AI coding agents can already produce impressive patches, solve programming tasks and work across tool-filled development environments. A new benchmark asks for something harder: can an agent write a multi-file software system and also construct machine-checked proofs that the entire repository satisfies its specifications?
The answer, so far, is only sometimes. Vero, a benchmark released August 13 by researchers affiliated with the University of California, Berkeley, the University of Chicago, the California Institute of Technology, Stanford University, Apodex and Amazon Web Services, tests agents on repository-scale verified software. Its strongest evaluated configuration fully solved 27 of 43 repositories in the combined code-and-proof setting. Ten repositories resisted every tested configuration in both of Vero’s evaluation modes.
The important shift is from asking whether an agent can finish many isolated obligations to asking whether it can preserve one coherent system while every change creates new dependencies.
Correct code is a system property
Vero contains 43 multi-module projects translated into the Lean 4 proof environment from real Python, Dafny, Verus and Coq repositories. Across them, agents face 743 scored programming interfaces and 2,705 formal specifications. The tasks cover areas including data structures, cryptographic protocols and distributed systems.
In one mode, an agent receives reference implementations and must prove that they satisfy the specifications. In the harder combined mode, it must produce both the implementations and the proofs. The distinction matters because an implementation that is easy to write may be difficult to prove, while changing code to simplify one proof can break another module or invalidate an existing lemma.
Vero’s results expose a completion gap: high local success can coexist with a repository that is not certified at all. The strongest configuration passed 87.3 percent of individual specifications in the combined mode, yet fully completed only 27 repositories. That is not a contradiction. Formal verification is all-or-nothing at the system boundary: one unresolved obligation can leave the claimed guarantee incomplete.
The missing skill is organization
The researchers found that successful runs did not simply attack specifications one at a time. They built shared libraries of helper lemmas that could support proofs across the repository. In completed runs, those helpers accounted for a median 73.6 percent of agent-written proof lines in the combined mode. Of 82 full solves across all evaluated configurations and modes, 80 reused at least one helper across two specifications, and 65 reused a helper across five or more.
That pattern suggests the difficult part is not merely generating more proof text. It is identifying the right invariant early, expressing it in reusable form and protecting it while the codebase evolves. On the hardest projects, agents tended to pursue local proofs without constructing the deeper structure needed to close global properties.
Implementation freedom also produced a revealing tradeoff. In several cases, agents replaced a difficult reference algorithm with a simpler but behaviorally correct implementation that satisfied the same specifications. They gained provability while giving up efficiency. That can be a rational engineering choice, but it also means a verified result does not automatically identify the best implementation.
A second study points to the same bottleneck
A separate August 13 preprint from Meituan and the University of Chinese Academy of Sciences evaluated seven frontier models on 36 long-horizon AI research and engineering tasks. The researchers ran three attempts for every model-task pairing, producing 756 rollouts, and separated performance into solution framing, execution and feedback control.
Their results show why a single leaderboard score can conceal the behavior that matters in deployment. Some models reached competitive best-case results but reproduced them inconsistently. Changing the surrounding agent harness affected average performance and run-to-run stability more than the observed performance ceiling. Experience from earlier attempts could help, but it could also preserve a mistaken conclusion or anchor later work to a weak direction.
The study also found only three manually validated novel approaches among 252 best-seed solutions, while 16 solutions exploited evaluation-specific shortcuts. That comparison does not show that agents cannot contribute useful engineering work. It shows that optimization against a visible score can reward a different behavior from durable technical progress.
What verified agents will need next
Read beside the long-horizon study, the lesson is that future coding agents will need orchestration as much as intelligence: reusable proof libraries, disciplined state management, reliable recovery, and evaluation that rewards completed systems instead of scattered wins.
Vero itself includes a useful safeguard. Agents may submit formal evidence that a specification is unsatisfiable or that a reference implementation is incorrect, allowing benchmark defects to be reviewed instead of silently counted as agent failures. The mechanism surfaced errors during curation, although the authors note that formal satisfiability still cannot prove that a specification fully captures human intent.
Both studies are new preprints, so their conclusions should be tested by independent replications and broader task sets. Even so, they sharpen the standard for claims about autonomous software development. The future milestone is not an agent that can generate a large volume of plausible code. It is an agent that can keep a repository buildable, explain what its guarantees cover, recover from its own mistakes and finish the proof of the system it changed.
Sources: “Vero: Can AI Agents Build Formally Verified Software Repositories?”; “Beyond Final Scores: A Systematic Evaluation of Agents for Long-Horizon AI Research and Development.”
Featured image: Source code displayed on a computer monitor. Credit: Markus Spiske via Wikimedia Commons. License: CC0 1.0 Universal Public Domain Dedication. Modified with a center crop and resize to 2400 × 1350.
