Formal verification changes what counts as done

Tests exercise examples selected by their authors. A formal specification states a property, and Lean's kernel checks a proof for every input covered by that property. The result is not universal correctness. It covers only the behavior expressed in the specification, within the proof's model and assumptions.

Vero's released suite has 43 instances translated from projects originally written in Python, Dafny, Verus, and Coq. They contain 743 scored APIs and 2,705 specifications, covering work such as data structures, numerical utilities, cryptographic protocols, and consensus.

Every instance freezes the shared types, API signatures, and specifications. Proof-only mode supplies a reference implementation. Code-and-proof mode withholds the implementation bodies, so the agent chooses an implementation and proves that its code satisfies the same interface.

Each run gets file-system, build, and Lean toolchain access for 90 minutes. The paper tested four coding-agent configurations in both modes. The strongest reported setup, GPT-5.5 at xhigh reasoning with Codex, completed 27 repositories in code-and-proof mode and 25 in proof-only mode. Ten repositories were not fully solved by any tested configuration in either mode.

The grader rebuilds what the agent claims

Vero does not trust the working directory left by the agent. It extracts content from permitted edit slots, inserts that content into a fresh project rendered from the benchmark source, and rebuilds it. The grader checks proof dependencies against an axiom allowlist. Rule-based and model-based screens reject declarations or typeclass instances that make the obligations trivial.

A green result in a dirty checkout can depend on an altered fixture, a hidden helper, or state the agent did not create. Reconstructing the submission from frozen material makes the evidence survive outside that working directory. Ordinary agent CI can use the same pattern even when the checks are tests rather than proofs.

Our RepoComplianceBench review found that agents often comply with requests to add work while overlooking instructions to stop or ask for a human. Vero moves its stop condition into the grader: all specifications must close, the clean project must build, and only allowed proof dependencies may remain.

Completed repositories rely on shared lemmas

The successful runs did not treat all 2,705 specifications as isolated proof holes. Across 82 full-solve runs, helper theorems make up a median 73.6% of proof lines in code-and-proof mode and 71.6% in proof-only.

Reuse is widespread. At least one helper supports two or more specifications in 80 of those 82 runs. In 65, a helper supports at least five.

Deeper chains were less reliable. Specifications with no helper passed at 83.9% in code-and-proof mode, but the rate fell to 50.6% at a helper-chain depth of four or more. Proof-only went from 80.1% to 39.1%.

Repository verification therefore needs more than local proof search. The agent has to identify invariants and build a reusable library soon enough for later obligations to share it. Successful local proofs can still leave duplicate lemmas, incompatible definitions, and a dependency structure that cannot be repaired before the deadline.

Provable code may be poor production code

Code-and-proof mode lets the agent replace a difficult reference algorithm with something simpler that satisfies the formal contract. The paper reports five instance-agent pairs across three repositories where this helped. Those runs closed all 250 specifications, compared with 201 in matched proof-only runs against fixed reference implementations.

Some replacements gave up asymptotic efficiency. The specifications required behavior, not a particular performance profile. A proof can establish its stated contract while saying nothing about latency, memory use, side channels, operational failures, or maintainability unless those properties are modeled.

Seventeen matched pairs were full solves in proof-only mode but not in code-and-proof. According to the trajectory analysis, agents often chose an implementation early and kept extending the proof attempt until time ran out instead of changing the definition.

Vero lets an agent challenge the benchmark

Curators can make formal mistakes. Vero accepts machine-checked negative evidence that a reference implementation violates a specification, one specification is impossible, or a set of specifications is jointly inconsistent. A confirmed witness sends the instance back for review. The authors say every confirmed defect was repaired before the reported evaluation.

This route gives the benchmark a precise response to an impossible task. It does not prove that every remaining instance is correct, but it separates a hard proof from a formally demonstrated curation error.

Auditing a reported run

The paper and evaluation tutorial expose the harness. A reproducibility review should check six things:

1. Use full-repository solves as the outcome and per-specification coverage for diagnosis.
2. Confirm that grading reconstructs a clean project from frozen source.
3. Inspect the axiom policy and the rejection rules for trivial proofs.
4. List performance and operational properties that the specifications do not model.
5. Report the harness, model setting, budget, benchmark commit, and mode together.
6. Read the unsolved repositories and formal defect witnesses as closely as the ranking.

Vero's own code is Apache-2.0. Three active benchmark translations retain their copyleft upstream licenses. The public benchmark inventory pins the source revision used for every Lean translation.

The 87.3% figure describes progress through individual obligations. The 16 unfinished repositories describe what could not yet be certified as a complete artifact.