Vero: Can AI Agents Build Formally Verified Software Repositories?

Vero 将原本分散在 Python、Dafny、Verus、Coq 的 43 个真实多模块实例重写为 Lean 4 仓库，提供 API、规范和参考实现，并设置 proof-only 与 code-plus-proof 两条赛道。审计不默认题目正确：它能证明部分规范不可满足或参考实现有错；最佳 agent 完成 27/43，却没有系统关闭最难仓库。基准因此同时测定理证明、实现和跨文件依赖管理，也避免把有缺陷的 oracle 当作不可质疑的真值。