Vero：首个仓库级代码与证明联合生成基准

AI 智能体被广泛用于辅助编程，但目前对生成代码的正确性几乎没有保证。来自多所机构的研究团队在 arXiv 发布了 Vero 基准，首次将「代码实现」与「机器可校验的形式化证明」放在仓库级别进行联合评估，填补了该方向长期缺乏系统性测试工具的空白。

基准设计：覆盖多语言、多领域

Vero 共收录 43 个多模块实例，源自真实的开源仓库，覆盖 Python、Dafny、Verus 与 Coq 四类语言，涉及密码协议、分布式系统等多样化领域。每个实例以一个多模块的 Lean 4 仓库形式给出，包含预先确定好的 API 接口、人工撰写的形式化规约以及参考实现。基准同时支持「仅证明」与「代码加证明」两种评估模式，使研究者可以分别衡量智能体在仅有规约和同时给出参考实现条件下的能力差异。

审计机制：纠正潜在的代码与规范错误

为提升基准的可靠性，Vero 引入了一项审计机制，允许智能体对给出的规约不可满足或参考实现存在错误等形式进行形式化证明。这一设计的目的是在数据整理过程中暴露并修正潜在的代码与规约错误，从而降低因基准本身缺陷而导致的评估偏差。

实验结果：最强智能体仅完整解决 27 个实例

研究团队使用接入 Lean 工具链的前沿编程智能体配置进行了评测。结果显示，即使是最强的智能体配置，也只能在 43 个实例中完整解决 27 个；而在难度最高的若干仓库上，没有任何智能体能够闭合全部规约。这一结果表明，当前 AI 智能体在仓库规模上同时进行实现与证明的能力仍然有限，距离真正可靠的「经形式化验证的软件合成」仍有相当距离。

开源与意义

Vero 的基准数据、整理流程与评测框架已随论文一同开源，为后续衡量「仓库级可信软件合成」的进展提供了具体测试平台。对关注 AI 编程智能体安全性与可信度的研究者而言，Vero 既是一个新的度量工具，也明确指出了当前能力的天花板所在。