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

A new method using a general language model code agent and a verification harness proves all targeted lemmas in Iris, Rust's standard libraries, and unfinished Lean 4 port of Iris, achieving full coverage without any failures or Coq expert intervention.

What the Document Says

  • A method using a general language model code agent (e.g., Claude Code) is shown to be simpler and more effective for automatic software verification than traditional methods.
  • The new approach achieves full coverage, proving every targeted lemma without failures or Coq expert intervention.
  • The paper evaluates the harness plus code agent on three dimensions: core logic, comparison with prior LLM provers, and generality.
  • In core logic, Aria proves all 4,257 lemmas of Iris's four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically.
  • Compared to prior LLM provers, Aria proves all 318 lemmas on reglang where prior provers managed barely one in eight.
  • On iris-lean (the unfinished Lean 4 port of Iris), the method proves 72 not-yet-ported lemmas, demonstrating its generality.

Key Concepts Mentioned

  • automatic software verification
  • large language models
  • code agent
  • formal verification
  • theorem provers
  • Iris
  • Rust's standard libraries
  • reglang
  • iris-lean

Claims Made by the Document

  • Imposing a fixed, human-designed proof strategy is unnecessary and limiting.
  • A general LLM code agent can prove every targeted lemma with no failures or Coq expert intervention.
  • The new harness plus code agent proves all targeted lemmas in Iris, Rust's standard libraries, and iris-lean.

Evidence Used

  • Results from evaluating the harness plus code agent on various lemmas and standards.
  • Statements about the proofs demanded by interactive theorem provers such as Coq and the limitations of existing approaches.

Methods / Approach

  • using a general language model code agent (e.g., Claude Code) in a verification harness that keeps proofs sound, complete, and terminating

Limitations Stated by the Authors

  • The paper doesn't provide information on the limitations of the method other than what is implied by comparisons with prior LLM provers.

Limitations Noted by the Agent

Agent interpretation — not from the source.

  • UNKNOWN - The text does not explicitly state any limitations of the method for the agent.
  • The method may have limitations in terms of scalability and applicability to other programming languages or logic systems beyond those tested.

Open Questions

  • What are the specific hard constraints that keep each proof sound, complete, and terminating?
  • How does the method handle complex and non-trivial software verification problems?
  • What is the scalability of the method for larger and more complex programs?

Notes for Future Q&A

May include interpretation. Labeled where it does.

  • The paper focuses on the results of the new approach but does not delve into the details of the method, leaving open questions about the specific constraints, applicability, and scalability.
  • Further research could investigate the internal workings of the verification harness and the general language model code agent for a better understanding of their capabilities.

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.