Harnessing Code Agents for Automatic Software Verification

• URL: http://arxiv.org/abs/2607.06341v1
• Date: Tue, 07 Jul 2026 14:39:59 GMT
• Title: Harnessing Code Agents for Automatic Software Verification
• Abstract summary: Large language models (LLMs) promise to generate proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system.<n>We show that imposing such a strategy is unnecessary and limiting.<n>Handing the whole lemma to a general code agent, free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective.
• Score: 0.47154736035631406
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study [0.20415910628419062]
  Large language models (LLMs) can generate text that resembles a mathematical proof, but resemblance does not establish correctness.<n>Coq bases its rules on the Calculus of Inductive Constructions, a logical framework that defines which proof steps the system may accept.<n>This pilot study evaluated six open-weight LLMs on the same 100 theorems from CoqStoq, a benchmark derived from real Coq projects.
  arXiv  Detail & Related papers  (2026-08-05T21:29:12Z)
• Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs [21.65389718022749]
  We present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution.<n>Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model.<n>Experiments show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost.
  arXiv  Detail & Related papers  (2026-06-16T14:33:15Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems [100.24694338574402]
  We present Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof.<n>IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents.<n>IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.
  arXiv  Detail & Related papers  (2026-05-22T00:05:36Z)
• Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning [20.336209492846752]
  Formal verification guarantees proof validity but not formalization faithfulness.<n>We investigate whether frontier models exploit this gap when generating Lean 4 proofs.<n>We find no evidence of systematic gaming in unified generation.
  arXiv  Detail & Related papers  (2026-04-21T13:37:49Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline.<n>The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed.<n>Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions.
  arXiv  Detail & Related papers  (2026-04-20T22:02:57Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Eigen-1: Adaptive Multi-Agent Refinement with Monitor-Based RAG for Scientific Reasoning [53.45095336430027]
  We develop a unified framework that combines implicit retrieval and structured collaboration.<n>On Humanity's Last Exam (HLE) Bio/Chem Gold, our framework achieves 48.3% accuracy.<n>Results on SuperGPQA and TRQA confirm robustness across domains.
  arXiv  Detail & Related papers  (2025-09-25T14:05:55Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  We present APOLLO (Automated PrOof repair viaLLM and Lean cOllaboration), a model-agnostic agentic framework for automated theorem proving.<n>A set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean, isolate failing sub-lemmas, utilize automated solvers, and invoke an LLM on each remaining goal.<n>Our results demonstrate that targeted, compiler-guided repair of LLM outputs yields dramatic gains in both efficiency and correctness.
  arXiv  Detail & Related papers  (2025-05-09T03:38:31Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  Large language models (LLMs) are increasingly integrated into real-world personalized applications.<n>The valuable and often proprietary nature of the knowledge bases used in RAG introduces the risk of unauthorized usage by adversaries.<n>Existing methods that can be generalized as watermarking techniques to protect these knowledge bases typically involve poisoning or backdoor attacks.<n>We propose name for harmless' copyright protection of knowledge bases.
  arXiv  Detail & Related papers  (2025-02-10T09:15:56Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  Two lines of approaches are adopted for complex reasoning with LLMs.<n>One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps.<n>The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers.<n>We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
  arXiv  Detail & Related papers  (2023-11-16T11:26:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.