# Supporting Software Formal Verification with Large Language Models: An Experimental Study

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jul 2025.

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

- [AgentGuard: Runtime Verification of AI Agents](https://mlsanity.com/paper/2509.23864/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [Evaluating LLM-Generated ACSL Annotations for Formal Verification](https://mlsanity.com/paper/2602.13851/) (2026)
- [LLM-Driven Heuristic Synthesis for Industrial Process Control: Lessons from Hot Steel Rolling](https://mlsanity.com/paper/2603.20537/) (2026)
- [Neurosymbolic Auditing of Natural-Language Software Requirements](https://mlsanity.com/paper/2605.13817/) (2026)
- [Self-Spec Verifiable Code Generation](https://mlsanity.com/paper/2609.39568/) (2026)

## Abstract (arXiv)

Formal methods have been employed for requirements verification for a long time. However, it is difficult to automatically derive properties from natural language requirements. SpecVerify addresses this challenge by integrating large language models (LLMs) with formal verification tools, providing a more flexible mechanism for expressing requirements. This framework combines Claude 3.5 Sonnet with the ESBMC verifier to form an automated workflow. Evaluated on nine cyber-physical systems from Lockheed Martin, SpecVerify achieves 46.5% verification accuracy, comparable to NASA's CoCoSim, but with lower false positives. Our framework formulates assertions that extend beyond the expressive power of LTL and identifies falsifiable cases that are missed by more traditional methods. Counterexample analysis reveals CoCoSim's limitations stemming from model connection errors and numerical approximation issues. While SpecVerify advances verification automation, our comparative study of Claude, ChatGPT, and Llama shows that high-quality requirements documentation and human monitoring remain critical, as models occasionally misinterpret specifications. Our results demonstrate that LLMs can significantly reduce the barriers to formal verification, while highlighting the continued importance of human-machine collaboration in achieving optimal results.