Evaluating LLM-Generated ACSL Annotations for Formal Verification
Not on the map. Why?
Abstract (arXiv)
Formal specifications are crucial for building verifiable and dependable software systems, yet generating accurate and verifiable specifications for real-world C programs remains challenging. This paper presents an empirical evaluation of automated ACSL annotation generation strategies for C programs, comparing a rule-based Python script, Frama-C's RTE plugin, and three large language models (DeepSeek-V3.2, GPT-5.2, and OLMo 3.1 32B Instruct). The study focuses on one-shot annotation generation, assessing how these approaches perform when directly applied to verification tasks. Using a filtered subset of the CASP benchmark, we evaluate generated annotations through Frama-C's WP plugin with multiple SMT solvers, analyzing proof success rates, solver timeouts, and internal processing time. Our results show that rule-based approaches remain more reliable for verification success, while LLM-based methods exhibit more variable performance. These findings highlight both the current limitations and the potential of LLMs as complementary tools for automated specification generation.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 13 of its 20 references that are in the map. First posted on arXiv 14 Feb 2026.
Builds on
13 of 20 references.
References · 13
- 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
- 2024Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verificationcited by 58
- 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
- 2023Finding Inductive Loop Invariants using Large Language Modelscited by 36
- 2024AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMscited by 31
- 2024Proof Automation with Large Language Modelscited by 22
- 2025RvLLM: LLM Runtime Verification with Domain Knowledgecited by 17
- 2024VeCoGen: Automating Generation of Formally Verified C Code with Large Language Modelscited by 10
- 2024Specify What? Enhancing Neural Specification Synthesis by Symbolic Methodscited by 6
- 2025SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Modelscited by 6
- 2025Supporting Software Formal Verification with Large Language Models: An Experimental Studycited by 6
- 2024Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFastcited by 5
1 more
Built on by
Citing papers per year: 2026: 1.
1 paper.