A new benchmark says AI coding agents still can't reliably prove their own code is correct.
Researchers released Vero, a benchmark that asks AI agents to write both an implementation and a machine-checked mathematical proof that the implementation meets a specification, across 43 real-world, multi-module repositories drawn from Python, Dafny, Verus, and Coq codebases covering things like cryptographic protocols and distributed systems. Each task is recast as a Lean 4 repository with a fixed interface, a hand-curated specification, and a reference implementation, so an agent has to get the code and the proof to agree with each other rather than just producing one or the other. The benchmark also lets agents flag cases where a spec is impossible to satisfy or a reference implementation is wrong, which caught real errors during the benchmark's own construction. When the researchers ran top coding-agent setups with access to the Lean proof toolchain, the best one fully solved only 27 of the 43 repositories and closed zero proofs on the hardest ones.
Most prior verified-code demos tested single functions or asked agents to prove a spec against code someone else already wrote, which flatters agents on an easier problem than shipping a working system. Vero moves the target closer to actual software engineering, where an agent must keep design and proof decisions consistent across an entire codebase, and the failure rate here suggests that skill is nowhere near solved.
Formal verification has spent decades being the thing serious engineers agree is a good idea and mostly skip anyway, and Vero suggests AI won't remove that excuse any time soon.