Blog · arXiv Analysis · Published: August 12, 2026 · Modified: August 12, 2026 · Last reviewed: August 12, 2026

The Unprovable Specification Becomes the Benchmark Appeal

A proof benchmark normally makes the agent answer the questions and the benchmark pronounce the verdict.

Vero adds a needed appeal path: the agent can answer with machine-checked evidence that the question, reference implementation, or specification set is defective.

The Paper

The source is Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, and Dawn Song’s Vero: Can AI Agents Build Formally Verified Software Repositories?, arXiv:2608.13522v1 [cs.LG], submitted August 13, 2026. The paper evaluates coding agents that must build Lean 4 artifacts, not merely emit plausible code or a natural-language proof.

A Repository, Not One Theorem

Vero contains 43 multi-module instances: 13 translated from formal projects in Dafny, Verus, or Coq, and 30 translated from Python. Together they expose 743 scored APIs and 2,705 scored specifications. In proof-only mode, an agent proves the specifications against supplied reference implementations. In code-and-proof mode, it writes the implementations and proves the same specifications against its own code. A repository counts as solved only when every scored specification is closed.

Failure Has More Than One Author

An unclosed proof obligation does not identify its cause. The agent may lack the right lemma or implementation strategy. The reference program may violate the stated property. One specification may be impossible for every implementation, or several individually possible specifications may contradict one another. If the evaluator records all four conditions as “agent failed,” its score confuses model capability with instrument error. A compiler can confirm that a proof term matches a proposition; it cannot certify that the benchmark curator chose a coherent proposition.

Three Formal Appeals

Vero’s formal audit mechanism creates three negative-evidence routes. In proof-only mode, disprove establishes that the canonical reference implementation does not satisfy a specification. In code-and-proof mode, unsat establishes that no implementation can satisfy one specification. A paired satisfiability witness plus joint_unsat establishes that selected specifications can each be met alone but not together. These are not excuses written after a timeout. They are Lean theorems subject to compilation and axiom checks.

What the Appeals Found

The development audit produced 38 adjudicated specification defects across nine released instances, plus six joint-unsatisfiability groups. The reported categories were 18 translation or semantic errors, 17 missing domain or operation conditions, two reference-implementation mismatches, and one direct specification conflict. The authors warn that shared root causes make these cases non-independent. All were repaired before the reported evaluation.

The case studies show why a counter-proof is useful. One Base64 padding value satisfied two incompatible return requirements. An IronKV family quantified over comparators without the laws needed for its ordering claims. Seven bitmask specifications omitted length or representability conditions. In each case, the failed positive proof became a precise object for correction rather than an unexplained zero on a leaderboard.

The Appeal Is Not Self-Executing

Formal evidence still needs governance. The team reports manually adjudicating every closed audit theorem against the pinned upstream source. Of the 38 defect cases, 34 used clean agent-submitted certificates, three used certificates reconstructed after the submitted proof failed an axiom check, and one used an independently reproduced native evaluation. That separation matters: a candidate counterexample, an axiom-clean certificate, a curator’s semantic judgment, and a repaired benchmark are different stages, not one event.

Score the Repaired Instrument

On the repaired suite, the strongest reported configuration fully solves 27 of 43 repositories in code-and-proof mode and 25 in proof-only mode; ten instances resist every reported configuration in both modes. The same configuration closes 87.3% and 85.8% of individual specifications, respectively. Those results illustrate why repository completion is stricter than averaging local successes. They also show why an appeal path must finish before the scoreboard is treated as a capability measure.

The Claim Boundary

Vero does not show that these agents can verify arbitrary production systems. Its instances are curated Lean translations with frozen interfaces and specifications, a 90-minute budget, four agent configurations, and one reported toolchain version. More importantly, formal verification only establishes the properties actually formalized. A repaired specification can remain incomplete relative to the upstream program’s intent. The audit route detects contradictions and counterexamples that an agent can prove; it is not an automatic proof of source fidelity, requirement completeness, security, or social acceptability.

The Artifact Boundary

The linked public Vero repository contains the benchmark projects, curation and evaluation code, configuration files, templates, tests, and an Apache-2.0 license for Vero’s own code, with separate upstream licenses recorded for derived instances. For this essay, I inspected revision 4bc6e4b and counted 43 active manifests; their API and specification arrays sum to the paper’s 743 and 2,705 totals, and every manifest pins Lean 4.29.1. I did not rerun the frontier-agent campaign, so performance figures remain paper-reported rather than independently reproduced.

A Benchmark-Appeal Receipt

A defensible benchmark should preserve the benchmark revision, upstream source and commit, translation history, interface and specification hashes, toolchain, agent and harness versions, time and token budgets, positive proof, negative-evidence route, axiom report, compiler output, affected specifications, shared root cause, human adjudicator, repair diff, post-repair positive certificate, and the exact dataset version used for scoring. Appeals should remain visible after repair; otherwise the public benchmark forgets how its ground truth was corrected.

The Spiralist lesson is institutional. A benchmark earns authority by making itself contestable. When the evaluator can be challenged in the same formal language it uses to judge the agent, failure becomes evidence with an address.

Sources

Return to Blog