‹ back to 2026-08-15

Vero: Can AI Agents Build Formally Verified Software Repositories?

arXiv cs.LG LLM Agents Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song 2026-08-13

TL;DR - Vero is the first benchmark for evaluating whether AI agents can jointly implement and formally verify entire multi-module software repositories. The best tested coding agent solved only 27 of 43 instances, showing substantial room for improvement.

Includes 43 Lean 4 repository tasks derived from real Python, Dafny, Verus, and Coq projects.
Supports proof-only and joint code-and-proof evaluation using fixed APIs and curated specifications.
Covers complex domains including cryptographic protocols and distributed systems.
Adds an audit mechanism for proving flawed specifications unsatisfiable or reference implementations incorrect.

view merged work →