# Intent-aligned Formal Specification Synthesis via Traceable Refinement

arXiv: https://arxiv.org/abs/2604.10392 · HTML: https://mlsanity.com/paper/2604.10392/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 42 references that are in the map.
- First posted on arXiv 12 Apr 2026.

## Builds on (most cited first, 29 of 29)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [FireAct: Toward Language Agent Fine-tuning](https://mlsanity.com/paper/2310.05915/) (2023)
- [Arcee's MergeKit: A Toolkit for Merging Large Language Models](https://mlsanity.com/paper/2403.13257/) (2024)
- [RedCode: Risky Code Execution and Generation Benchmark for Code Agents](https://mlsanity.com/paper/2411.07781/) (2024)
- [Inference-Aware Fine-Tuning for Best-of-N Sampling in Large Language Models](https://mlsanity.com/paper/2412.15287/) (2024)
- [BOND: Aligning LLMs with Best-of-N Distillation](https://mlsanity.com/paper/2407.14622/) (2024)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [LM-Cocktail: Resilient Tuning of Language Models via Model Merging](https://mlsanity.com/paper/2311.13534/) (2023)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Towards Understanding the Characteristics of Code Generation Errors Made by Large Language Models](https://mlsanity.com/paper/2406.08731/) (2024)
- [CLEVER: A Curated Benchmark for Formally Verified Code Generation](https://mlsanity.com/paper/2505.13938/) (2025)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [MergeME: Model Merging Techniques for Homogeneous and Heterogeneous MoEs](https://mlsanity.com/paper/2502.00997/) (2025)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [AutoSpec: Automated Generation of Neural Network Specifications](https://mlsanity.com/paper/2409.10897/) (2024)

## Built on by (most cited first, 2 of 2)

- [Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation](https://mlsanity.com/paper/2610.10604/) (2026)
- [Passing Tests, Missing Semantics: Evidence of Interpretive Lock-In in Plan-Based DataFrame Code Generation](https://mlsanity.com/paper/2610.15797/) (2026)

## Abstract (arXiv)

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.