Vero: Can AI Agents Build Formally Verified Software Repositories?
Source: https://arxiv.org/abs/2608.13522
Authors: Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
Published: 2026-08-13
Categories: cs.LG, cs.AI, cs.LO, cs.PL, cs.SE
PDF: https://arxiv.org/pdf/2608.13522v1
Code: https://github.com/sunblaze-ucb/vero
中文导读
Vero 是第一个在仓库级别评测"实现 + 机器检查证明"联合合成的基准。动机：AI agent 写代码越来越多，但对生成代码的正确性没有任何保证；验证式代码生成（agent 同时产出实现与规格的形式化证明）是通往可信 AI 软件更强的路径。已有基准要么只针对单个函数，要么在给定实现下只评证明生成——agent 能否在真实多模块代码库中做出连贯的实现与证明决策，此前是开放问题。
Key Findings
- 基准构成：43 个多模块实例，源自 Python、Dafny、Verus、Coq 的真实仓库（密码学协议到分布式系统），统一整理为带预定 API 接口、人工整理形式规格与参考实现的 Lean 4 多模块仓库；支持 proof-only 与 code-and-proof 两种评测模式。
- 审计机制（benchmark reliability）：允许 agent 形式化地证明"所给规格不可满足"或"参考实现有错"，在整理阶段暴露并修正了潜在的代码与规格错误——用被测对象自身的形式化能力给基准查错。
- 前沿 agent 表现：给予 Lean 工具链访问的前沿 coding-agent 最强配置仅完全解出 43 例中的 27 例，且在最难仓库上没有闭合任何规格。
- 结论：仓库级验证式软件合成仍是当前 agent 的明显短板；基准、整理流水线与评测 harness 已开源。
Intake rationale
- Category: coding | Quality score: 4/5
- 把 verified code generation 从函数级推向仓库级，43 例/27 解的落差量化了 coding agent 在形式化证明上的真实边界；审计机制是基准设计上的新意。
Grounding
opencli arxiv paper 2608.13522 -f json（标题/作者/摘要/日期/分类均来自 arXiv 元数据）。