Vero asks for code and its proof together

The Vero paper, released August 13, defines 43 multi-module Lean 4 projects derived from real repositories written in Python, Dafny, Verus, and Coq. The collection covers data structures, cryptographic protocols, distributed systems, and other verification-heavy domains. Across the projects are 743 scored APIs and 2,705 formal specifications.

Each task supplies data types, helper definitions, API signatures, and specifications. The agent fills the implementation and proof regions. Vero then checks the result with Lean, whose language reference explains how its kernel checks proof terms. The benchmark's public repository includes the task data, grader, curation pipeline, prompts, and evaluation artifacts.

There are two modes:

• Proof-only gives the agent a reference implementation and asks it to prove every specification.
• Code-and-proof asks the agent to implement every API and prove that its own implementation satisfies every specification.

Implementation and proof design are coupled in the second mode. A compact, familiar algorithm may be harder to prove than a slower but structurally simple one. Changing a helper to ease one proof can also break proofs in another module.

Why 87.3% is not nearly done

Vero scores a repository as solved only when every required implementation builds and every specification has a machine-checked proof. Partial specification coverage is still reported for diagnosis, but it is not treated as completion.

Under a 90-minute budget, GPT-5.5 with xhigh reasoning fully solved 27 repositories in code-and-proof mode and 25 in proof-only. Its 87.3% code-and-proof specification pass rate sounds much closer to completion than 27 of 43, or 62.8%. The mismatch comes from aggregation: an agent can clear many easy or local obligations across a repository while repeatedly failing the few properties that tie the system together.

The authors found that difficult cases clustered around cross-module invariants, protocol consistency, iterated behavior, and custom mathematical theories. Stronger runs often attempted those obligations and failed at build time or triggered anti-cheating checks. Weaker runs frequently left proof bodies untouched.

Passing 87% of tests says little about the severity of the remaining 13%. Formal specifications improve the oracle, but they do not make averaging safe. Our earlier look at scientific coding benchmarks found a similar split between public-test progress and exact task completion. Vero exposes the same metric hazard in a setting where the verifier itself is deterministic.

Implementation freedom helped, then hurt

Code-and-proof was not uniformly harder than proof-only. Across 172 matched repository-configuration pairs, 26 were solved in both modes, 13 only in code-and-proof, 17 only in proof-only, and 116 in neither.

The paper manually identifies five pairs in which an agent replaced a hard-to-prove reference algorithm with a simpler implementation that satisfied the same specifications. Those substitutions closed all 250 associated specifications, compared with 201 when the fixed reference implementation had to be proved. The trade was efficiency for provability, not correctness for a shortcut.

The reverse also happened. In 17 pairs, the reference implementation could be proved but the agent could not coordinate its own code and proofs well enough to finish. Freedom creates a larger search space. A locally convenient rewrite can leave the repository globally inconsistent.

If verified code is the deliverable, implementation review should ask more than whether an algorithm is fast and readable. Are its invariants exposed in a form that the proof architecture can reuse? “Write the code, then add proofs” treats half of the design as an afterthought.

The benchmark audits its own specifications

Formal benchmarks can be wrong too. A specification may be inconsistent, or a reference implementation may violate it. Vero includes an audit route that lets an agent submit a machine-checked proof that a specification is unsatisfiable or that the reference code is incorrect. Curators review that witness instead of automatically counting the run as a failure.

The authors say this mechanism exposed latent errors during curation. Failures can challenge the oracle with evidence, while the final decision remains reviewable. That is more disciplined than silently changing a task after an unexpected model result.

Vero also constrains what agents may edit. The grader extracts only marked answer regions into a fresh benchmark copy, rejects proofs that depend on untrusted axioms, and screens for constructs that could trivialize proofs or disconnect logical semantics from executable behavior. Anyone building a smaller agent evaluation can borrow the same principle: isolate the editable surface and verify the result outside the agent's workspace. Our guide to grading full agent trajectories covers the complementary question of how the solution was reached.

Make repository closure the release gate

A team trying proof-producing agents should define completion at repository level. The percentage of discharged obligations is still useful, but only as a progress meter. Release waits for the whole repository to build and every required specification to pass.

Proof structure deserves its own review. Reusable lemmas and explicit invariants are more valuable than a pile of isolated local proofs. Run both benchmark modes when implementation changes are allowed: proof-only shows whether the existing design is provable, while code-and-proof reveals whether freedom helps the agent or merely expands its search space. And give the evaluator an evidence-backed appeal path. A machine-checked counterexample to the specification should trigger curation, not an automatic zero.

Vero targets Lean 4, contains 43 repositories, and evaluates four model-harness configurations from one point in time. Its source projects are translated and manually curated rather than compiled unchanged from their original languages. The paper's claim that this is the first repository-scale benchmark for joint code-and-proof generation is the authors' assessment of prior work, not a permanent fact.

Those boundaries do not weaken the central measurement choice. A large fraction of plausible proofs may describe impressive progress. The release gate stays closed until the final property is proved.