# Harnessing Code Agents for Automatic Software Verification arXiv: https://arxiv.org/abs/2607.06341 ยท HTML: https://mlsanity.com/paper/2607.06341/ ## Key facts - Cited by 1 papers in the map (data through 14 Oct 2026). - Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. - Builds on 22 of its 63 references that are in the map. - First posted on arXiv 7 Jul 2026. ## Placed in - LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/) ## Builds on (most cited first, 22 of 22) - [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022) - [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023) - [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020) - [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022) - [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024) - [RepairAgent: An Autonomous, LLM-Based Agent for Program Repair](https://mlsanity.com/paper/2403.17134/) (2024) - [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022) - [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023) - [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019) - [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022) - [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023) - [Generating Correctness Proofs with Neural Networks](https://mlsanity.com/paper/1907.07794/) (2019) - [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024) - [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020) - [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024) - [Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming](https://mlsanity.com/paper/2405.01787/) (2024) - [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024) - [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024) - [Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)](https://mlsanity.com/paper/2309.03046/) (2023) - [Compositional Non-Interference for Fine-Grained Concurrent Programs](https://mlsanity.com/paper/1910.00905/) (2019) - [Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement](https://mlsanity.com/paper/2109.07863/) (2021) - [Cryptis: Cryptographic Reasoning in Separation Logic](https://mlsanity.com/paper/2502.21156/) (2025) ## Built on by (most cited first, 1 of 1) - [FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification](https://mlsanity.com/paper/2610.00885/) (2026) ## Abstract (arXiv) Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.