LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation
On the map: LLM agents and tool use → Software engineering coding agents
Abstract (arXiv)
Formal specification is essential for rigorous program verification, yet writing correct specifications remains costly and difficult to automate. Although large language models (LLMs) and agents have shown promising progress, their true capabilities and failure modes remain unclear. We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs. We introduce LiveFMBench, a continuously evolving benchmark of 630 ACSL (ANSI/ISO C Specification Language)-annotated C programs, including 360 newly collected cases designed to mitigate data leakage. Using this benchmark, we evaluate direct prompting with different sampling sizes, reasoning-enabled (thinking mode) inference, the agentic pipeline, and perform a fine-grained failure analysis. Experimental results reveal that naive evaluation substantially overestimates performance because models under direct prompting may exhibit unfaithful behaviors, such as deceiving automated provers or ignoring code-context constraints; after excluding such cases, the true specification generation accuracy drops by approximately 20%. We further find that both increased sampling and thinking mode significantly improve success rates, with smaller models benefiting more from thinking mode. Agentic pipelines are particularly effective under low sampling budgets and on harder datasets. Failure analysis further shows that incorrect loop invariants are the dominant error type, while agentic pipelines notably reduce assertion errors. These results expose fundamental limitations in current LLM-based approaches and suggest they remain far from replacing human-authored formal specifications. We release LiveFMBench at https://huggingface.co/datasets/fm-universe/Live-FM-Bench and all evaluation artifacts to support future research.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use. Builds on 32 of its 56 references that are in the map. First posted on arXiv 2 May 2026.
Builds on
32 of 56 references.
References · 32
- 2021Evaluating Large Language Models Trained on Codecited by 8,053
- 2021Program Synthesis with Large Language Modelscited by 3,509
- 2024Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameterscited by 1,928
- 2024Qwen2.5-Coder Technical Reportcited by 1,151
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
- 2022UniXcoder: Unified Cross-Modal Pre-training for Code Representationcited by 355
- 2023Using an LLM to Help With Code Understandingcited by 222
- 2025Qwen2.5-1M Technical Reportcited by 158
- 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
- 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
- 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
- 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
20 more
- 2024A Survey on LLM-based Code Generation for Low-Resource and Domain-Specific Programming Languagescited by 65
- 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
- 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
- 2024SpecGen: Automated Generation of Formal Program Specifications via Large Language Modelscited by 51
- 2025What to Retrieve for Effective Retrieval-Augmented Code Generation? An Empirical Study and Beyondcited by 22
- 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
- 2024What You Need is What You Get: Theory of Mind for an LLM-Based Code Understanding Assistantcited by 8
- 2024SpecEval: Evaluating Code Comprehension in Large Language Models via Program Specificationscited by 8
- 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8
- 2025Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMscited by 8
- 2024Leveraging Large Language Models to Boost Dafny's Developers Productivitycited by 7
- 2025VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Codecited by 7
- 2025Local Success Does Not Compose: Benchmarking Large Language Models for Compositional Formal Verificationcited by 6
- 2025A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programscited by 6
- 2018Deductive Verification of Unmodified Linux Kernel Library Functionscited by 5
- 2015An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Projectcited by 4
- 2025Retrieval-Augmented TLAPS Proof Generation with Large Language Modelscited by 2
- 2014Dafny: Statically Verifying Functional Correctnesscited by 1
- 2025DiffLiB: High-fidelity differentiable modeling of lithium-ion batteries and efficient gradient-based parameter identificationcited by 1
- 2025Towards Language Model Guided TLA+ Proof Automationcited by 1
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2026P3: Joint Program-and-Proof Planning for Verified Code Generation
- 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
- 2026Automating Formal Verification with Agent-Guided Tree Search
- 2026Agentic Separation Logic Specification Synthesis
- 2026Beyond Type-checking: Towards Holistic Evaluation of Formal Specification Generation
- 2026Intent-aligned Formal Specification Synthesis via Traceable Refinement
- 2026TDD-Agent: Test-Driven Reasoning for Code Generation
- 2026SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs?