Automatically generated code is gaining traction recently owing to 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 such general mathematical reasoning, however, it tends to be more structured. The structure of the program can be used to structure the proof as well as its intermediate lemmas.

In this work, we present a first LLM agent 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 Rocq (formerly Coq) theorem prover to get additional context. 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, as well as on Linux kernel modules, shows promising efficacy in achieving agentic 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, thereby moving closer to the vision of trusted automatic programming.