Adnan KhanAdnanProduct & AI
San Francisco Bay Area
Get in touch

Source note3 min read

Harnessing Code Agents for Automatic Software Verification

Source

arXiv

arxiv.org/abs/2607.06341v1

Read the source

Source

Plain-Language Brief

The authors propose a new method for automatic software verification using large language models (LLMs) in the form of 'code agents'. Instead of wireting a fixed proof strategy, they allow the code agent to choose its own approach, which results in full coverage with no failures or Coq expert intervention. The harness around the agent ensures each proof is sound, complete, and terminating. The method was evaluated on three dimensions: core logic, comparison with prior LLM provers, and generality.

What the Document Says

  • The authors propose a method for automatic software verification using large language models (LLMs).
  • They introduce a code agent approach where the agent chooses its own strategy for proof generation.
  • The harness around the agent ensures each proof is sound, complete, and terminating.
  • On Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4257 lemmas of four core modules and 217 lemmas verifying Rust's standard libraries fully automatically.
  • On reglang, where prior provers manage barely one in eight, Aria proves all 318 theorems.
  • On iris-lean, an unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas.
  • The method does not require a fixed proof strategy and achieves full coverage with no failures or Coq expert intervention.

Key Concepts Mentioned

  • automatic software verification
  • large language models
  • code agents
  • proof generation
  • soundness
  • completeness
  • termination
  • Iris
  • reglang
  • iris-lean

Claims Made by the Document

  • The proposed method achieves full coverage with no failures and no Coq expert intervention.
  • On Iris, the state-of-the-art separation logic, Aria proves all targeted lemmas fully automatically.

Evidence Used

  • The authors demonstrate the effectiveness of their approach through evaluations on various logics and theorem proving benchmarks.
  • Results show that Aria achieves full coverage on Iris, reglang, and iris-lean.

Methods / Approach

UNKNOWN

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

Raw Abstract / Excerpt

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.