知识卡片：Vero——AI 智能体能否构建形式化验证的软件仓库？

英文标题：Vero: Can AI Agents Build Formally Verified Software Repositories?
英文关键词：Verified Code Generation; AI Agents; Repository-Level Benchmark; Formal Verification; Lean 4; Proof Synthesis

一句话结论

Vero 是首个在“仓库级”评估 AI 智能体联合生成代码实现与机器可检查形式化证明的基准。最强配置的智能体仅完整解决 43 个实例中的 27 个，在最难仓库上未闭合任何规范（closes no specifications）；这说明当前智能体距离仓库级可验证软件综合仍有明显差距。

事件概述或研究问题

AI 智能体越来越多地被用于编程，但其生成的代码没有正确性保证。论文提出“验证式代码生成”路线：智能体同时输出实现和满足规范、可由机器检查的证明。现有基准要么只针对单个函数，要么在给定实现的前提下只评估证明生成；尚不清楚智能体能否在真实的多模块代码库中做出连贯的实现与证明选择。Vero 旨在填补这一空白。

方法/产品要点

Vero 是一个基准测试，包含 43 个多模块实例；实例源自真实软件仓库，来源生态涉及 Python、Dafny、Verus、Coq，领域从密码协议到分布式系统。
每个实例以多模块 Lean 4 仓库形式组织，包含预先确定的 API 接口、人工整理的形式化规范，以及参考实现。
支持两种评估模式：仅证明（proof-only）和“代码+证明”（code-and-proof）。
设置审计机制：允许智能体正式证明给定规范不可满足，或参考实现不正确，从而在基准整理过程中暴露并修正潜在代码与规范错误。
评测对象为可访问 Lean 工具链的前沿编码智能体配置；基准、整理流程与评估框架已开源。

主要结果或产业意义

最强智能体配置完整解决 43 个实例中的 27 个；在难度最高的仓库上，未完成任何规范证明。
这表明仓库级“代码+证明”联合生成仍是未解决问题；Vero 为衡量该方向进展提供了具体测试平台。
产业意义在于：Vero 把“AI 生成代码 + 机器可检查证明”作为可评测目标，为需要强正确性保证的软件自动化提供了一条可衡量的前进方向；但当前结果说明距离实用仍有差距。

为什么重要

Vero 将可信 AI 生成软件的评测从“单函数”提升到“多模块仓库”层面，且要求智能体同时负责实现和证明，而不是在给定实现后只做证明。这是一个从“AI 写代码”到“AI 保证代码正确”的关键评测步骤。

与既有脉络的关系

已有相关卡片分别涉及 AI 智能体做开放式研究、技能库建设和 IoT 漏洞利用。Vero 的增量在于：它聚焦形式化验证，把“智能体生成的软件是否可证明正确”作为核心问题，与 SkillCenter 的技能检索、VEXAIoT 的漏洞利用和开放式研究的科学问题提出均不重复；同时延续了“AI 智能体能承担复杂工程任务但尚未达到可靠自主”的总体判断。

局限与不确定性

摘要未披露所测前沿智能体的具体模型名称、配置细节、计算成本与实验方差，待核实。
真实仓库到 Lean 4 实例的转换保真度、人工整理规范的具体过程、审计机制的触发频率等细节，摘要未展开，待核实。
Vero 的得分与真实生产环境中的软件验证能力之间的关系，摘要未说明，待核实。

可用于图书/PPT/简报的角度

数字钩子：最强 AI 智能体在仓库级验证代码生成上只完成 27/43，说明“生成代码”和“证明代码正确”之间的差距。
故事线：AI 写代码 → AI 为代码写证明 → AI 在多模块仓库中同时完成两者。
方法论角度：用“真实仓库来源 + 多模块 Lean 4 + 双评估模式 + 审计机制”构造一项更接近实际软件工程的 AI 能力基准。
可信 AI 角度：形式化验证可以被视为给 AI 软件“上保险”，但 Vero 显示当前保险还远未普及。

原始材料

英文标题：Vero: Can AI Agents Build Formally Verified Software Repositories?
来源：https://arxiv.org/abs/2608.13522v1
PDF：https://arxiv.org/pdf/2608.13522v1
arXiv ID：2608.13522v1
作者：Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
发布/更新：2026-08-13
主要分类：cs.LG；其他分类：cs.AI, cs.LO, cs.PL, cs.SE