Vero: Can AI Agents Build Formally Verified Software Repositories?

AI agents cannot yet reliably generate formally verified code at scale: When evaluated on Vero's 43 real-world multi-module repositories, frontier coding agents failed to produce correct implementations with machine-checked proofs, indicating that current AI systems lack the capability to ensure correctness guarantees across complex codebases—a critical requirement for trustworthy AI-generated software.

Formal verification requires coherent decision-making across entire systems: The benchmark reveals that generating verified code is fundamentally different from generating individual functions; agents must make consistent implementation and proof choices across multiple interconnected modules, a challenge that existing benchmarks have not adequately tested until now.

Specification and reference code errors are common in verification benchmarks: Vero's audit mechanism—which allows agents to formally prove when specifications are unsatisfiable or reference implementations are incorrect—surfaced and corrected latent errors in the benchmark itself, suggesting that previous verification benchmarks may contain undetected flaws that undermine their reliability.

Formal verification offers a path toward genuinely trustworthy AI code generation: Unlike traditional code generation that relies on testing, verified code generation produces machine-checked mathematical proofs of correctness, providing stronger guarantees about AI-generated software safety and reliability for high-stakes applications like cryptographic protocols and distributed systems.

Bridging the gap between AI capabilities and formal verification remains an open challenge: The paper establishes that while AI agents show promise in programming tasks, the jump to generating formally verified multi-module repositories represents a significant unsolved problem requiring future research and development.