Signal Vero: Can AI Agents Build Formally Verified Software Repositories?

Summary

AI agents are increasingly used for programming, yet there is no guarantee that the code they generate is actually correct. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, is presented as a more solid path toward trustworthy AI software than unverified generation. The paper notes that existing benchmarks in this area either focus on individual functions or evaluate only narrow slices of a codebase, rather than covering whole, formally verified software repositories. To address this gap, Vero is introduced with the aim of testing whether AI agents can actually build and maintain entire formally verified repositories. As a result, Vero extends verified code generation from isolated functions to realistic, repository-scale software engineering.