在软件工程领域，形式化验证长期被视为确保代码正确性的终极手段，但其高昂的人力成本限制了大规模应用。UC Berkeley 等机构的研究者近日发布 Vero 基准，试图探索 AI 智能体能否承担这一重任，在仓库级规模下同时完成实现代码与数学证明的编写。

Vero 被定位为首个聚焦仓库级场景的验证基准，其设计核心在于模拟真实开发环境中的多文件、多模块交互。基准包含 43 个基于 Lean 4 证明助手构建的实例，每个实例均涉及多个相互依赖的模块，总计包含 743 个用于评分的应用程序接口（API）以及 2705 条形式化规范。

与现有基准不同，Vero 要求智能体不仅生成可运行的代码，还需为每个函数提供经过验证的数学证明，确保实现与规范严格一致。这意味着智能体必须同时掌握编程逻辑与定理证明能力，并在跨模块的复杂依赖关系中保持一致性。

研究团队表示，Vero 的评估体系覆盖了从基本函数到复杂数据结构的多种场景，能够有效区分智能体在验证任务上的细微能力差异。初步实验显示，当前主流 AI 模型在该基准上的表现仍有显著提升空间，尤其在处理多步骤证明策略和模块间接口约束时存在明显短板。

该基准的发布为 AI 辅助软件工程提供了新的评测维度，或将推动智能体从简单的代码生成向可验证、高可靠性的软件开发方向演进。对于依赖严格安全标准的行业，如航空航天、金融系统和自动驾驶，Vero 所衡量的能力可能成为未来 AI 工具选型的重要参考。