# Evaluating LLM-Generated ACSL Annotations for Formal Verification

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

## Key facts

- Cited by 1 papers 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 (most cited first, 13 of 13)

- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024)
- [RvLLM: LLM Runtime Verification with Domain Knowledge](https://mlsanity.com/paper/2505.18585/) (2025)
- [VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models](https://mlsanity.com/paper/2411.19275/) (2024)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [SV-LLM: An Agentic Approach for SoC Security Verification using Large Language Models](https://mlsanity.com/paper/2506.20415/) (2025)
- [Supporting Software Formal Verification with Large Language Models: An Experimental Study](https://mlsanity.com/paper/2507.04857/) (2025)
- [Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast](https://mlsanity.com/paper/2411.02318/) (2024)
- [Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects](https://mlsanity.com/paper/2507.14330/) (2025)

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

- [Partial Contracts Suffice: Sound, LLM-Inferred Regression Verification](https://mlsanity.com/paper/2607.10291/) (2026)

## 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.