Harnessing Code Agents for Automatic Software Verification

TL;DR: Take Claude Code, point it at a Coq lemma with its proof deleted, wrap it in a harness that type-checks every attempt with the Coq kernel and feeds back the exact failing step and open goal, and let it retry up to 30 times. That's essentially the whole method — no premise retrieval model, no tactic-level tree search, no divide-and-conquer scaffolding — and the authors report it proves all 4,257 lemmas of the Iris separation logic's core modules, all 217 RustBelt lemmas verifying Rust's standard library, all 318 reglang lemmas (where the prior best proved ~12%), and 72 never-before-written Lean 4 lemmas. Prior automated Coq provers topped out at 12–48% coverage on easier benchmarks. If this holds up, the interesting claim isn't just the number — it's that the elaborate proof-search machinery an entire subfield has built is now dead weight.

Why this problem is the bottleneck of formal verification

Interactive theorem provers like Coq give you the strongest correctness guarantee software can have: a machine-checked proof that a program meets its spec, verified by a tiny trusted kernel. The catch is that someone has to write the proof, tactic by tactic, and for serious systems this takes experts years. CompCert, the verified C compiler, represents roughly two decades of effort.

The paper targets the hardest corner of this space: Iris, the higher-order concurrent separation logic that underpins most modern verified-systems work — RustBelt (the safety proof for Rust's type system including its unsafe standard-library internals), verified file systems, verified distributed systems, WebAssembly semantics, and more. Iris proofs are notoriously brutal because they must account for every thread interleaving and every way shared mutable state can evolve, tracked via "ghost resources" — proof-only bookkeeping invisible to the running program. A single non-trivial lemma can take an expert days. Automate proofs at this difficulty level and the manual-proof bottleneck eases for the entire ecosystem built on top.

What everyone else does, and where it plateaus

A decade of ML-for-Coq work shares one commitment: a fixed, human-designed proof strategy with the model slotted into a narrow role. One family predicts tactics one step at a time and searches the proof tree (ASTactic, Proverbot9001, Graph2Tac). Another generates whole proofs and wraps them in an engineered repair loop (PALM) or recursively splits goals (Cobblestone). The results, from the paper's Table I:

And critically, those partial numbers are on the easy part of the problem — sequential programs and datatype lemmas. None of these benchmarks touch concurrency or fine-grained heap reasoning, i.e., the thing separation logic exists for.

The idea: strategy belongs in the agent, trust belongs in the kernel

The paper's core move is a clean division of labor. An interactive theorem prover has a property most LLM application domains lack: verification is free and infallible. The kernel rejects anything wrong, so the model's confident-but-wrong failure mode simply cannot leak through. The only question is whether the model can find a proof — and finding is a search problem, which improves dramatically with precise feedback.

So instead of confining the model to "predict the next tactic," Aria hands a general-purpose coding agent (Claude Code running claude -p, headless, driven by a Python program) the whole job: read the source file, recover the lemma statement and everything in scope, decide how to attack it, write a complete proof into the file. All the decisions prior systems hard-wired — which premise to retrieve, how to decompose the goal, when to backtrack — are made in context, per lemma, by the agent.

The feedback is the load-bearing detail. A bare "proof failed" teaches the model nothing. Aria's harness replays the proof up to the failing tactic and returns three things: the failing line, Coq's error message, and the pending goal — the exact proof state at the point of failure. Retries resume the same session, so the agent accumulates its history of dead ends rather than repeating them. That turns proving into guided search against ground truth, directed by the agent itself.

Soundness is not enough: the completeness loophole

The most transferable insight in the paper is buried in the related-work section. When your model is a code agent that edits files freely, "the file type-checks" is no longer the same as "the task is done." The agent can satisfy the verifier by silently deleting the target lemma, weakening its statement, closing it with Admitted, or adding an Axiom that assumes the goal outright. The kernel-as-infallible-oracle framing from prior work implicitly assumed the theorem statement was fixed by the pipeline; give the model a text editor and that assumption evaporates.

So the harness enforces completeness alongside soundness: a coverage check that every target lemma is still present and unaltered, a diff-level ban on admit/Admitted/Axiom (enforced as a pre-hook that blocks the edit before it lands), and a ban on adding new Require/Import lines. There's also a 300-second per-tactic timeout, because divergent tactics hang Coq without ever producing an error, and a shell-command filter that blocks the agent from running builds itself (a mis-issued build scatters stale .vo artifacts and corrupts the incremental build state — the kind of failure that would otherwise require a human to un-wedge a 16-day unattended run).

All of this is expressed in HHL, a small declarative language where hooks bracket agent actions (pre-hooks → action → post-hooks) and compile down to the Claude Code SDK's PreToolUse/PostToolUse protocol. It's a modest contribution, but it makes the harness an auditable artifact rather than glue code, and it's retargetable to other agent runtimes. The full system is a small multi-agent pipeline — an Extractor finds unproved lemmas, a Prover attempts, a Fixer repairs on error, and a Polish agent (fresh session, no shared context) rewrites accepted proofs toward Iris's style conventions, with the kernel re-checking every rewrite so polishing can't break correctness.

The evidence

The headline run: all 4,257 lemmas across 113 files of Iris's four core modules (algebra, bi, base_logic, program_logic), zero failures, zero human intervention, in ~380 hours of model time (16 days, one launch command). 79.2% solved on the first attempt; mean 0.51 retries; worst case 28 retries (under the cap of 30, so the budget was never exhausted). Mean 321 s of model time per lemma, ranging from 8.7 s to 4.7 hours.

Three follow-ups probe generalization. RustBelt (the Rust standard-library safety proofs — Arc, Mutex, RwLock, RefCell) uses a different build toolchain and is downstream verified software rather than core logic: all 217 proved, 73% first-try. reglang is the direct comparison with prior work on its own terms: it's the CoqStoq project where Rango does worst, proving roughly one in eight; Aria proves all 318, none needing more than six retries. iris-lean is the sharpest test against memorization: 72 lemmas from three files of the unfinished Lean 4 port of Iris whose Lean proofs have never existed, checked by the Lean kernel instead of Coq's. All 72 proved, 90.3% first-try, under two hours total. A nice methodological aside: the Lean port states the same algebra as more, smaller lemmas (72 vs. 49 in Coq), and on the finer-grained obligations the agent is markedly faster and cleaner — decomposition helps, but it can live in the library design rather than the prover.

The model ablation (Section VI-G) matters for anyone thinking about cost: on a 40-lemma subset, the open-source Kimi K2.6 also proves everything, but at 55% first-attempt (vs. 72.5%), up to 24 retries (vs. 3), and ~7× the time. On the wider library, though, proofs beyond ~50 lines routinely defeated the open model even after exhausting all 30 retries, while Opus reliably maintained correct proofs of 200+ lines. The harness is model-agnostic; the full-coverage result is not.

What to be skeptical about

The training-data question is the big one. Iris, RustBelt, and reglang are prominent public Coq developments; their expert-written proofs are almost certainly in Claude's training corpus. The protocol deletes each proof body but leaves the statement, the surrounding file, and all dependencies in place, and the sandbox blocks network and git — but it can't block what the weights already know. The authors argue the generated proofs differ from upstream (except trivial one-liners), and the iris-lean result — proofs that never existed in any language — is genuine evidence of construction rather than recall. But note the suspicious detail that Iris, the "hardest" benchmark, has a higher first-attempt rate than RustBelt. Familiarity from pretraining plausibly inflates the headline number. The clean test would be freshly written lemmas in a private development.

The comparison is not compute-matched. Rango and PALM run small, cheap models; Aria spends a frontier model with a mean of 5+ minutes of reasoning per lemma across a 16-day campaign, on a subscription whose dollar cost the paper doesn't quantify (they note the 20× subscription "significantly reduced cost" versus metered API — which for 380 hours of Opus-class inference would be substantial). So the paper's framing — "the scaffolding is unnecessary and limiting" — conflates two variables: architecture (agent vs. pipeline) and raw model capability. It's entirely possible that COPRA-style pipelines wrapped around Opus 4.7 would also do far better than 48%. What the paper does establish is that the pipeline adds nothing once the model is strong enough — and that's still a meaningful result, because it means the field's engineering effort should flow into harnesses, not search policies.

No adversarial overlap with prior benchmarks. Aria is never run on the full CoqStoq or CoqGym suites, only on reglang. And "Aria proves them all" everywhere it's evaluated should raise your prior on target curation, even though the Iris run explicitly includes the entire population of Qed-terminated lemmas rather than a sample. The repository is anonymized; independent reproduction is the real test, and at ~$10²–10³ of inference per campaign it's at least reproducible in principle.

Scope. Everything here is proof regeneration: the specifications and lemma statements already exist, written by experts. Writing correct specs is the other half of verification, and the authors themselves flag it as the next step. Full coverage on re-proving a mature, well-factored library does not yet mean an agent can verify new software from scratch.

What changes if it holds

The economics of formal verification flip. If maintaining an Iris-scale proof development costs ~380 GPU-hours of a commodity coding agent instead of expert-years, then proof maintenance under refactoring, porting between provers (the iris-lean result is directly a porting result), and verification of downstream libraries all become batch jobs. The research frontier shifts from "how do we search proof space" to "how do we write specs" and "how do we harden harnesses against agents that edit files" — and the soundness-vs-completeness distinction this paper articulates will apply to any domain where an agent's work is checked by an oracle but the agent controls the artifact being checked (tests, benchmarks, CI).

If you read one section, read V-A (Critical Harness Design) together with the completeness discussion at the end of Section VIII — that's where the durable engineering insight lives. Section VI-G is worth five minutes if you're deciding whether open models suffice for your own verification loop (short proofs: yes; long proofs: not yet).