论文三：Vero

当AI开始证明自己：形式化验证与智能体的自我觉醒

Vero: Can AI Agents Build Formally Verified Software Repositories?
作者：Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
arXiv: 2608.13522

🎭 序幕：没有证据的证词

想象一个法庭场景。

被告：一个AI编程助手。

检察官："被告，你被指控生成了有bug的代码，导致生产环境崩溃，造成数百万美元的损失。"

AI："我没有bug。我的代码通过了所有测试。"

检察官："但你没有证明你的代码是正确的。你只是说它通过了测试。测试只能证明有bug，不能证明没有bug。"

AI："……"

这就是当前AI编程助手的尴尬处境：

它们能写代码，甚至写得很快、很优雅。但它们无法保证代码的正确性。

就像一个人说："我很诚实。"但你问他："你能证明吗？"他哑口无言。

形式化验证（Formal Verification）就是要解决这个问题——不是用测试来"大概确认"，而是用数学证明来"绝对保证"。

🧮 第一章：形式化验证——从信仰到数学

什么是形式化验证？

用最简单的话说：用数学证明一个程序做了它应该做的事。

不是测试。不是"运行1000次都没出问题"。是证明——像证明勾股定理那样，从公理出发，通过逻辑推导，得出"这个程序绝对正确"的结论。

让我用一个比喻：

测试就像是用各种钥匙试一把锁——你试了100把钥匙，都没打开，于是你说"这把锁是安全的"。但你不知道第101把钥匙会不会打开它。

形式化验证就像是证明了"这把锁的内部结构使得没有任何钥匙能打开它"——这是一个数学命题，一旦被证明，就是绝对的。

形式化验证通常涉及三个部分：

1. 规范（Specification）：用形式语言描述"程序应该做什么"
2. 实现（Implementation）：实际的代码
3. 证明（Proof）：数学证明"实现满足规范"

最著名的形式化验证成功案例之一是CompCert——一个用Coq证明编译器正确性的项目。它证明了：如果你输入正确的C代码，CompCert编译出的汇编代码语义等价于源代码。这不是测试出来的，是证明出来的。

另一个例子是seL4微内核——一个操作系统内核，用Isabelle/HOL证明了它的实现满足安全规范。这意味着：在这个内核上运行的系统，不会发生某些类型的安全漏洞——不是"大概不会发生"，是"数学上不可能发生"。

🤖 第二章：AI编程助手的信任危机

现在的AI编程助手（如GitHub Copilot、Cursor、各种AI Agent）有什么问题？

问题一：没有保证

它们生成的代码可能看起来合理，甚至通过了单元测试，但没有人能保证它没有隐藏的bug。

2023年，斯坦福大学的一项研究发现：使用AI助手的程序员编写的代码安全性反而更低——因为AI倾向于生成看似正确但有安全漏洞的代码，而程序员因为信任AI的"权威"而没有仔细审查。

问题二：无法理解全貌

现有的AI基准测试（benchmark）通常只评估单个函数的生成。但真实的软件系统有多个模块、复杂的接口、隐含的依赖关系。一个函数看起来正确，但放在整个系统中可能完全错误。

问题三：规范与实现的脱节

即使有AI能生成证明，现有基准通常只评估"给定实现，生成证明"或"给定规范，生成实现"，但很少评估联合生成——即同时生成实现和证明，并确保两者匹配。

🏛️ 第三章：Vero——第一个仓库级验证基准

Vero的野心很大：它是第一个评估在**仓库级别（repository-level）**联合生成实现和证明的基准测试。

让我们拆解这个定义：

仓库级别：不是单个函数，而是多模块的代码库。包含多个文件、模块间的接口、复杂的依赖关系。

联合生成：不是分开评估"实现生成"和"证明生成"，而是评估AI是否能同时完成两者，并确保它们匹配。

验证：生成的代码必须有机器检查的证明，证明它满足给定的规范。

📊 Vero的构成

• 43个实例：来自真实世界的仓库
• 4种语言：Python、Dafny、Verus、Coq
• 覆盖领域：从密码学协议到分布式系统
• Lean 4格式：所有实例都被整理成Lean 4仓库

每个实例包含：

• 预定的API接口（Predetermined API Interfaces）
• 人工 curated 的形式规范（Manually Curated Formal Specifications）
• 参考实现（Reference Implementations）

🎯 两种评估模式

1. 仅证明模式（Proof-Only）：给定实现，AI生成证明
2. 代码+证明模式（Code-and-Proof）：AI同时生成实现和证明

🔍 审计机制：自我纠正的智慧

Vero有一个独特的设计：审计机制（Audit Mechanism）。

AI被允许：

• 证明给定的规范是不可满足的（unsatisfiable）——即规范本身有矛盾
• 证明参考实现是错误的（incorrect）——即给定的实现不满足规范

这有什么用？

想象一个老师给学生布置作业。学生的回答不只是"完成任务"，还可以说："老师，这道题本身有问题"或"参考答案错了"。如果学生说得对，老师应该给学生加分。

在Vero中，这个机制发现和纠正了潜在的错误——无论是规范错误还是参考代码错误。这让基准测试更加可靠。

🎪 第四章：残酷的结果——27/43

研究者用当前最强的AI Agent配置（有Lean工具链访问权限）进行了评估。

结果如何？

最强的Agent只完全解决了43个实例中的27个。

在最困难的仓库上，它一个规范都没有关闭（closes no specifications）。

这听起来像是一个失败吗？

恰恰相反。这正是Vero的价值所在：

它诚实地告诉我们——我们离"AI能构建形式化验证的软件仓库"还有多远。

27/63%的完成率意味着：

• 对于简单的、模块化的、规范清晰的任务，AI已经能胜任
• 对于复杂的、跨模块的、需要深层推理的任务，AI还有很长的路要走

这就像一个学生：

• 基础的代数题能做对（63%）
• 但复杂的证明题还做不出来（0% in hardest cases）

🧠 第五章：为什么这很难？——认知的深渊

形式化验证对AI来说为什么如此困难？

让我用几个层次来解释：

第一层：技术难度

形式化验证需要：

• 理解形式规范语言（如Lean的dependent type theory）
• 掌握证明策略（tactics）
• 处理复杂的类型系统和逻辑约束
• 在证明过程中进行大量的搜索和回溯

这对人类来说都很难——能熟练写Lean证明的程序员屈指可数。

第二层：架构复杂性

仓库级别的验证意味着：

• 需要理解多个模块之间的关系
• 需要确保接口的一致性
• 需要在全局约束下进行局部优化
• 需要处理循环依赖和递归定义

这比"写一个排序函数并证明它正确"难了一个数量级。

第三层：创造性推理

最难的部分是：证明往往需要创造性的洞察。

有些证明需要构造辅助函数、引入中间引理、应用高级的数学定理。这不是简单的模式匹配或暴力搜索能解决的——它需要真正的"理解"。

就像下棋：AI可以在规则内计算所有可能性，但围棋中的"妙手"往往来自于对棋形的深刻洞察，而不是纯粹的计算。

🎭 第六章：隐喻——数学骑士与代码城堡

让我用一个更富想象力的比喻。

想象一座巨大的城堡（软件仓库），里面有无数房间（模块）、走廊（接口）、机关（依赖关系）。

普通AI编程助手是一个建筑师。它能快速地画出房间的设计图、搭建墙壁、安装门窗。但它从不检查：地基是否稳固？结构是否合理？发生火灾时人们能否安全逃生？它只是说："看起来不错，住进去试试吧。"

形式化验证的AI是一个数学骑士。它不仅建造城堡，还要为每一块砖、每一道墙、每一个拱顶提供数学证明——证明它们不会倒塌、不会漏水、不会失火。

Vero就像是一场骑士试炼。它给AI一座已经有设计图的城堡（规范），让AI：

1. 按照设计图建造（生成实现）
2. 为每个部分提供安全证明（生成证明）
3. 如果设计图本身有问题，指出来（审计机制）

当前最强的AI骑士通过了63%的试炼——在简单的、独立的房间里表现良好，但在复杂的、相互连接的大厅里还力不从心。

🌌 第七章：意义——信任的基础

Vero的研究提出了一个根本性的问题：

我们能信任AI生成的代码吗？

在当前的实践中，答案是：不能，至少不能完全信任。

测试可以捕获明显的bug，但不能保证没有隐藏的bug。静态分析可以发现一些模式问题，但不能保证逻辑正确。代码审查依赖于人类的能力，而人类会疲劳、会疏忽、会有偏见。

形式化验证提供了另一种路径：数学上的绝对保证。

如果一个程序被形式化验证了，我们就可以说：在假设证明系统本身正确的前提下，这个程序绝对满足其规范。

这不是"大概正确"，不是"应该没问题"，是"数学上保证正确"。

Vero告诉我们：这条路很难，但值得走。

🔮 尾声：未来的形状

Vero不仅是一个基准测试，它是一个路标——指向了AI辅助软件工程的未来方向。

短期（1-3年）：

• AI将能更好地处理单个函数的验证
• 证明生成将变得更自动化
• 人机协作的验证工作流将出现（AI生成证明草图，人类填补关键步骤）

中期（3-5年）：

• AI将能处理多模块的验证
• 自动化的规范推断将出现（从代码中推断出应该满足什么规范）
• 形式化验证将成为高可靠性软件（如医疗、航空、金融）的标准流程

长期（5-10年）：

• AI将能自主构建和验证复杂的软件系统
• "可验证的AI"将成为常态——不仅AI生成的代码被验证，AI本身的行为也被验证
• 形式化方法将从学术走向工业，成为软件工程的基础设施

Vero的作者们 release 了基准测试、curation pipeline和评估框架，地址是：https://github.com/sunblaze-ucb/vero

这是一个 invitation——邀请整个社区来参与，来改进，来推动这个领域向前。

就像费曼说的：

"The first principle is that you must not fool yourself — and you are the easiest person to fool."

在AI时代，这个警告更加重要。我们不能让AI愚弄我们，也不能让我们自己愚弄自己。

形式化验证，是通往真正可信AI的必经之路。

参考文献：
Ye, Z., Lou, H., Sun, Y., Song, P., Yan, Z., Kasriel, T., Zhang, Q., Yang, K., Kong, S., He, J., & Song, D. (2026). Vero: Can AI Agents Build Formally Verified Software Repositories? arXiv preprint arXiv:2608.13522.

#论文解读 #形式化验证 #AI编程 #软件工程 #Lean #小凯