# AutoACSL: Synthesizing ACSL Specifications by Integrating LLMs with CPG-Based Static Analysis

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 26 references that are in the map.
- First posted on arXiv 18 Jun 2026.

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

- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation](https://mlsanity.com/paper/2405.02580/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Can ChatGPT support software verification?](https://mlsanity.com/paper/2311.02433/) (2023)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [Specify What? Enhancing Neural Specification Synthesis by Symbolic Methods](https://mlsanity.com/paper/2406.15540/) (2024)
- [A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs](https://mlsanity.com/paper/2512.24594/) (2025)
- [An experimental Study using ACSL and Frama-C to formulate and verify Low-Level Requirements from a DO-178C compliant Avionics Project](https://mlsanity.com/paper/1508.03894/) (2015)
- [Next Steps in LLM-Supported Java Verification](https://mlsanity.com/paper/2502.01573/) (2025)
- [AutoDeduct: A Tool for Automated Deductive Verification of C Code](https://mlsanity.com/paper/2501.10889/) (2025)
- [Seeking Specifications: The Case for Neuro-Symbolic Specification Synthesis](https://mlsanity.com/paper/2504.21061/) (2025)
- [SPEEDY: An Eclipse-based IDE for invariant inference](https://mlsanity.com/paper/1404.6605/) (2014)

## Abstract (arXiv)

Generating formal specifications for C programs remains a challenge in formal verification due to the manual effort, expertise, and semantic precision required. While recent advancements in large language models (LLMs) offer promise in automating specification synthesis, current approaches often lack semantic depth and produce unverifiable or incomplete contracts. To address these limitations, we introduce AutoACSL, a novel framework that integrates LLM prompting with semantic features extracted from Code Property Graphs (CPGs). AutoACSL performs static analyses to extract key semantic elements, including arithmetic operations, loop and recursion structures, and return value propagation, which are encoded into structured prompts. These prompts enable the LLM not only to generate normal behavioral specifications but also to include constraints that prevent inputs leading to runtime errors. AutoACSL employs a feedback-driven synthesis loop, where candidate specifications are verified using Frama-C/WP and refined iteratively until verification succeeds or a termination condition is met. Evaluated on 604 programs drawn from diverse datasets, AutoACSL achieves a 98% specification generation success ratio and a 96% full proof ratio when paired with Gemini-3. Compared to a code-only baseline, AutoACSL improves the full proof ratio by 24.7% to 51.7% across four LLMs (GPT-o4 Mini, GPT-5.2, Grok-4.1, and Gemini-3), demonstrating that integrating large language models with CPG-based static analysis substantially enhances both generation robustness and verification effectiveness for automated ACSL specification synthesis.