Vero：AI Agents 能否构建经过形式化验证的软件仓库？

AI agents 越来越多地被用于编程，但无法对生成代码的正确性提供任何保证。经过验证的代码生成，即由 agent 同时生成实现及其规格说明的机器检验证明，为实现可信的 AI 生成软件提供了一条更强的路径。该方向上的现有基准要么专注于单个函数，要么仅在提供实现的情况下评估证明生成。agents 能否在真实的多模块代码库中做出连贯的实现和证明选择，仍然是一个未解问题。为弥合这一差距，我们引入 Vero，这是首个在仓库级别评估联合实现与证明合成的基准。Vero 包含 43 个多模块实例，来源于横跨 Python、Dafny、Verus 和 Coq 的真实世界仓库，并覆盖从密码协议到分布式系统的多样化领域。每个实例由一个多模块 Lean 4 仓库组成，包含预先确定的 API 接口、人工整理的形式化规格说明以及参考实现，支持仅证明和代码加证明两种评估模式。为提高基准的可靠性，Vero 还包含一种审计机制，允许 agents 形式化证明所提供规格说明的不可满足性或参考代码的不正确性，从而在整理过程中暴露并纠正潜在的代码和规格说明错误。我们评估了可访问 Lean 工具链的前沿 coding-agent 配置。最强的 agent 仅完全解决了 43 个实例中的 27 个，并且在最难的仓库上没有完成任何规格说明。Vero 为衡量仓库规模的经过验证的软件合成进展提供了一个具体测试平台，而当前 agents 在这方面仍有不足。我们在 https://github.com/sunblaze-ucb/vero 发布了该基准、整理流水线和评估工具。