Intent-aligned Formal Specification Synthesis via Traceable Refinement

ArXi:2604.10392v1 Announce Type: cross Large language models are increasingly used to generate code from natural language, but ensuring correctness remains challenging. Formal verification offers a principled way to obtain such guarantees by proving that a program satisfies a formal specification. However, specifications are frequently missing in real-world codebases, and writing high-quality specifications remains expensive and expertise-intensive.