Preprint
Aug 2026
Vero: Can AI Agents Build Formally Verified Software Repositories?
Vero is introduced, the first benchmark to evaluate joint implementation and proof synthesis at the repository level and an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation.
Zhe Ye, Hantao Lou, Yuechun Sun et al.
· 0 citations