Vero：首个仓库级实现与证明联合合成基准，最强 Agent 仅解出 43 个实例中的 27 个

研究者提出 Vero，首个在仓库层面评估实现与形式化证明联合合成的基准，用于衡量 AI Agent 能否构建经过机器校验的软件。Vero 包含 43 个多模块实例，取自 Python、Dafny、Verus 和 Coq 的真实仓库，覆盖密码协议到分布式系统等领域，每个实例由带预定 API 接口的 Lean 4 多模块仓库、人工整理的形式化规格和参考实现组成，支持仅证明与代码加证明两种评测模式。基准还引入审计机制，允许 Agent 形式化证明给定规格不可满足或参考代码有误，从而在整理阶段暴露并修正潜在的代码与规格错误。在可访问 Lean 工具链的前沿编码 Agent 配置下，最强 Agent 仅完整解出 43 个实例中的 27 个，在最难的仓库上未能闭合任何规格。作者开源了基准、整理流程与评测框架。