Agentic Program Verification

TL;DR

Agentic Program Verification introduces AutoRocq, an autonomous LLM agent that collaborates with the Rocq prover to generate, refine, and certify proofs of real-world program properties. By combining context-aware tactic generation, a proof-tree representation, and a feedback loop that leverages prover responses and historical proof data, AutoRocq achieves end-to-end verification on SV-COMP benchmarks and Linux kernel modules, outperforming several baselines. The work demonstrates that explicit agency—deciding when and what context to fetch and how to adapt tactics—significantly boosts proof discovery and efficiency, enabling a generate-and-validate loop toward trusted automatic programming. This approach provides a practical path to scalable formal verification for AI-generated code and complex software, with potential to integrate with AI coding assistants for automated verification during development.

Abstract

Automatically generated code is gaining traction recently, owing to the prevalence of Large Language Models (LLMs). Further, the AlphaProof initiative has demonstrated the possibility of using AI for general mathematical reasoning. Reasoning about computer programs (software) can be accomplished via general mathematical reasoning; however, it tends to be more structured and richer in contexts. This forms an attractive proposition, since then AI agents can be used to reason about voluminous code that gets generated by AI. In this work, we present a first LLM agent, AutoRocq, for conducting program verification. Unlike past works, which rely on extensive training of LLMs on proof examples, our agent learns on-the-fly and improves the proof via an iterative refinement loop. The iterative improvement of the proof is achieved by the proof agent communicating with the Rocq (formerly Coq) theorem prover to get additional context and feedback. The final result of the iteration is a proof derivation checked by the Rocq theorem prover. In this way, our proof construction involves autonomous collaboration between the proof agent and the theorem prover. This autonomy facilitates the search for proofs and decision-making in deciding on the structure of the proof tree. Experimental evaluation on SV-COMP benchmarks and on Linux kernel modules shows promising efficacy in achieving automated program verification. As automation in code generation becomes more widespread, we posit that our proof agent can be potentially integrated with AI coding agents to achieve a generate and validate loop, thus moving closer to the vision of trusted automatic programming.

Figures (8)

• Figure 1: (a) Proof obligation wp_goal extracted from benchmark52_polynomial in SV-COMP svcomp and its proof generated by AutoRocq, with (b) the proof tree constructed during proving, where lemmas highlighted are retrieved from the global context autonomously by AutoRocq.
• Figure 2: Overview of AutoRocq, where components involving decision-making by LLMs are highlighted .
• Figure 3: Histogram of different complexity metrics: lemmas from SV-COMP programs (blue) vs. CoqGym (orange). Not a single lemma from CoqGym involves more than 100 terms or 7 hypotheses.
• Figure 4: [RQ.1] Lemmas proved by each tool on CoqGym and SV-COMP programs. On both benchmarks, AutoRocq is able to prove more lemmas, and has the most number of uniquely proved lemmas.
• Figure 5: [RQ.1] # of lemmas proved from SV-COMP programs: a breakdown by lemmas' complexity.

Theorems & Definitions (1)

• Definition : Proof Tree