Intent-aligned Formal Specification Synthesis via Traceable Refinement
For developers and verification engineers, this reduces the expertise and cost of writing formal specifications, but the approach is incremental, combining known techniques (LLMs, traceability, repair) in a new pipeline.
VeriSpecGen synthesizes intent-aligned formal specifications in Lean from natural language via traceable refinement, achieving 86.6% on VERINA SpecGen task with Claude Opus 4.5, improving over baselines by up to 31.8 points. Training on generated trajectories improves specification synthesis by 62-106% and transfers to general reasoning.
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. We present VeriSpecGen, a traceable refinement framework that synthesizes intent-aligned specifications in Lean through requirement-level attribution and localized repair. VeriSpecGen decomposes natural language into atomic requirements and generates requirement-targeted tests with explicit traceability maps to validate generated specifications. When validation fails, traceability maps attribute failures to specific requirements, enabling targeted clause-level repairs. VeriSpecGen achieve 86.6% on VERINA SpecGen task using Claude Opus 4.5, improving over baselines by up to 31.8 points across different model families and scales. Beyond inference-time gains, we generate 343K training examples from VeriSpecGen refinement trajectories and demonstrate that training on these trajectories substantially improves specification synthesis by 62-106% relative and transfers gains to general reasoning abilities.