Preprint Open access
Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
When generating verifiable code, natural language requirements are mapped to machine checked code using LLMs and agentic workflows. A crucial component of this pipeline is specification generation (SpecGen), which produces a formal contract against which an agent can prove implementation correctness. Proof generation c …