Berkeley's Vero Benchmark: Only 27 of 43 Repos Fully Solved

Berkeley's RDI lab has released a new benchmark called Vero. It asks AI agents to do two things at once, at the scale of an entire codebase: implement every required API and prove that each given specification holds, while keeping the code, the proofs, and the build consistent throughout. Earlier formal-verification benchmarks mostly stopped at a single theorem or a single function; a repository-level benchmark is a first.

The test set consists of 43 multi-module Lean 4 projects, ported from existing code written in Python, Dafny, Verus, and Coq, covering 743 APIs and 2,705 formal specifications in total. The evaluation runs in two modes: in proof-only mode, agents are given a reference implementation and only need to write the proofs; in code-and-proof mode, agents must write the implementation themselves and then prove it satisfies the specification.

The scoreboard

Number of fully solved instances (out of 43) under a 90-minute budget:

The gap between the first and third rows is worth looking at closely: with the same GPT-5.5 and the same Codex, simply turning the reasoning setting from medium up to xhigh takes the code-and-proof score from 2 to 27. On this kind of task, the marginal return on reasoning budget is nowhere near saturated.

The hard part isn't any single proof

The top row hides another pair of numbers. GPT-5.5 (xhigh) passes 87.3% of individual specifications in code-and-proof mode and 85.8% in proof-only mode, but once the bar becomes "the entire instance is fully done," that drops to 27/43 and 25/43. The researchers' conclusion is blunt: proving any single specification is no longer the hard part — keeping an entire proof repository consistent is.

The gap between those two numbers has real engineering consequences. An 87% pass rate on individual specs means that, on a project with dozens of specs, almost every project will end up with a handful still stuck. And formal verification is all-or-nothing: if even one specification isn't proven, the whole repository fails to build, and everything proven correctly earlier earns no partial credit. That's a completely different situation from a project that passes 87% of its unit tests and still ships.

Another detail concerns what the proof code is actually made of. Across the runs that were fully solved, auxiliary lemmas made up a median of 73.6% of the proof code. In other words, three-quarters of what the agents wrote existed purely as scaffolding to prop up the main proof. That ratio suggests today's models are taking a breadth-first approach — brute-forcing their way through with piles of lemmas — rather than finding a clean proof structure.

Picking your own algorithm: helped five times, hurt seventeen

Code-and-proof mode gives agents one extra degree of freedom: since they write the implementation themselves, they can choose an algorithm that's easier to prove. The researchers measured the net effect of that freedom in paired comparisons: switching algorithms led to success in 5 cases, but caused failure in 17.

That 5-to-17 split says a lot. In theory, the freedom to choose your own implementation should only ever help — worst case, you just copy the reference implementation. In practice, models frequently picked an implementation they judged clever, which turned out to be much harder to prove, and then got stuck in it for the full 90 minutes. Writing code and knowing which code is easy to prove are two different skills, and current agents only have the first one.

The leaderboard leaves one more note: of the 43 instances, 10 were never solved by any configuration, in either mode. Those instances mark the current hard ceiling of the field's methods, and they're exactly where the next round of work should focus.

For people building AI coding tools, Vero's value isn't the leaderboard ranking — it's that "repository-level consistency," a quality that could previously only be judged by feel, has been turned into a measurable metric. Benchmarks like SWE-bench test whether a model can fix one bug correctly; Vero tests whether it can hold up under the full set of constraints of an entire engineering project. The two are not the same order of difficulty.

Sources: Berkeley RDI Lab public blog, CocoLoop; benchmark scale, fully-solved counts for both modes, per-spec pass rates, auxiliary-lemma share, and paired-comparison statistics have all been checked against the public report.