Lean 证明它没问题，结果 AI 还是挖出了漏洞：形式化验证没有失灵，只是边界露了出来

一场很有戏剧性的安全实验

“这个程序已经被证明是正确的。”——如果你是安全工程师，听到这句话，多半会先挑一下眉毛。

最近，开发者 Kiran 讲了一个非常有意思的故事：他把一个由 Lean 生态构建、并声称经过端到端形式化验证的 zlib 实现 lean-zip，交给 Claude、AFL++、AddressSanitizer、Valgrind 和 UBSan 去狠狠干一晚上。结果跑了超过 1.058 亿次模糊测试后，结论居然既让人安心，又让人背后一凉。

安心的是，lean-zip 那些真正被证明过的核心代码——压缩、解压、DEFLATE、Huffman、CRC32 这一套——没炸出典型的内存安全问题。没有堆溢出，没有 use-after-free，没有栈溢出，甚至连未定义行为都很干净。背后一凉的是，漏洞还是找到了，而且是个货真价实的堆缓冲区溢出，只不过它不在应用代码里，而在 Lean 4 的运行时里。

这件事之所以迷人，在于它像一部技术圈悬疑片：主角以为自己把房间里的门窗都焊死了，结果小偷是从地基里钻进来的。

形式化验证到底证明了什么，又没证明什么

先说清楚一个容易被误读的点：这不是“Lean 证明错了”，也不是“形式化验证是骗局”。相反，这个案例几乎是形式化验证最好的广告之一。

lean-zip 最核心的一条定理很直白：对任意小于 1GB 的字节数组，先压缩再解压，最后一定还原成原始数据。换句话说，在它声明的数学模型和证明范围内，压缩函数和解压函数互为逆操作。这种保证不是“测试看起来没问题”，而是用证明助手把正确性一层层推出来的。

问题在于，软件从来不是只有“算法”这一个层面。你证明了算法，不代表外围解析器、文件头读取、系统调用封装、底层运行时、内存分配器也都跟着自动无敌。Kiran 做实验时，特意把定理、文档和 C FFI 都剥掉，只保留纯 Lean 原生实现，再让 AI 在不知道“这玩意儿已经被证明过”的情况下去找错。这种设计很聪明，因为它避免了模型带着“权威崇拜”做无效审计。

最终找到的两个问题，也恰好落在“证明边界”之外。一个是 ZIP 档案解析器里未验证的代码路径，另一个更深：Lean 运行时里负责分配 ByteArray 的 C++ 函数 lean_alloc_sarray 存在整数溢出，导致超大容量申请时分配出一个极小的缓冲区，后续读取却仍按超大长度进行，直接造成堆溢出。

这很像早年 CompCert 的经典经验：被验证过的编译优化阶段很稳，真正容易出问题的，反而是没被验证的前端。验证不是魔法，它只是把“这里我有把握”这件事写得非常精确。问题也正出在这份精确上——只要边界外还有代码，风险就还在。

AI 时代，安全审计开始进入“穷举化”阶段

如果把这件事放到 2026 年的语境里看，它的意义又更大了一层。

过去几年，AI 在写代码这件事上争议不断，但在找漏洞这件事上，进步几乎是肉眼可见的。Kiran 在文中提到，业界已经开始担心 AI 代理的漏洞挖掘能力会把“发现 bug 的成本”压到极低。你未必相信每一家公司的宣传，但大方向已经非常明显：那些原本需要资深研究员几周、几个月追踪的复杂软件缺陷，正在越来越多地被自动化系统全天候、并行化地扫出来。

这对整个软件行业其实是个坏消息。因为现实世界里的大多数软件，并不是按“会被无限审查”这个标准写出来的。很多系统能跑十年，不是因为它们绝对健壮，而是因为过去没人有这么便宜、这么大规模的火力持续攻击它们。现在不同了。16 个并行 fuzzer，一晚上上亿次执行，这种审计强度已经不再是顶尖实验室的专属配置，而是在慢慢变成普通团队也够得着的能力。

于是，形式化验证忽然不再只是学术圈的浪漫理想，而有了很现实的工程价值：当攻击成本断崖式下降，防守方就不能再只靠“希望测试覆盖到了”。证明不是万能药，但它至少能把一部分最核心、最危险、最基础的错误，提前从可能性空间里直接删除掉。

换句话说，AI 正在把“软件质量”从一个差不多就行的问题，变成一个你必须更认真回答的问题。

真正让人后背发凉的，是“可信基座”也会出错

这次最刺眼的发现，其实不是 lean-zip 自身的拒绝服务漏洞，而是 Lean 运行时的堆溢出。

原因很简单：运行时属于 Trusted Computing Base，也就是“可信计算基座”。所有上层证明，都默认这层地板是结实的。可一旦这层木板腐了，上面的数学大厦再优雅，也会跟着一起晃。

触发条件并不玄学。研究者构造了一个只有 156 字节的 ZIP 文件，却在 ZIP64 头里填了一个接近 SIZE_MAX 的压缩大小。运行时在给 ByteArray 分配空间时，24 + n 这样的计算发生了整数回绕，本该申请天文数字大小的内存，最后只拿到二十多字节的小块。随后读取函数仍按超大长度去读，缓冲区自然被踩穿。更讽刺的是，最小复现代码只有短短几行，几乎像是给“所有版本都受影响”这件事配的黑色幽默注脚。

这类问题在系统软件史上并不罕见。很多“安全语言”并不是绝对安全，而是把大部分风险关进了运行时和编译器。一旦那一小块核心实现有 bug，影响面反而非常广。Rust、Go、Java 这些生态都绕不开类似讨论：语言层面再强，标准库、编译器后端、JIT、GC、FFI 边界，依旧是安全研究者最爱下手的地方。

所以这次事件真正提出的问题是：当我们越来越依赖证明、类型系统和安全语言时，谁来审计这些“证明成立的前提”？谁来验证验证器，谁来监督守门人？文章标题那句拉丁文——“谁来监督守望者”——放在这里，实在是再贴切不过。

这不是给形式化验证泼冷水，而是在帮它长大

我反而觉得，这条新闻最值得高兴的地方，是它没有把形式化验证神化，也没有把它打成笑话。

在 1 亿多次执行里，AI 没能在被验证的 Lean 应用代码中找到传统压缩库常见的内存安全漏洞。这件事本身已经非常了不起。想想 zlib、libarchive、各类 ZIP 解析器这些年积攒下来的 CVE 历史，你会更明白这个结果有多稀缺。很多老牌 C/C++ 压缩实现，最头疼的就是边界检查、长度字段、整数溢出、状态机错位。Lean 这类带依赖类型和良基递归约束的工具，把一整类 bug 在结构上就压掉了。

但另一面，它也诚实地告诉行业：形式化验证真正困难的，不只是证明一个算法，而是决定你究竟要证明到哪一层。你可以证明压缩-解压闭环正确，却没证明 ZIP 文件头来自恶意输入时该如何防御；你可以证明业务逻辑没有 bug，却仍然依赖一个用 C++ 写的运行时来分配内存。证明边界画在哪里，决定了安全边界画在哪里。

这对当下很热的“AI 自动生成 + 自动验证代码”路线也是提醒。未来我们可能会看到更多“AI 写代码、AI 证明代码、AI 再 fuzz 代码”的流水线，但别忘了，流水线并不会自动回答“系统边界在哪”这个问题。规范缺失的地方、没纳入证明的模块、默认可信的基础设施，仍然会成为攻击者最现实的突破口。

如果一定要给这件事下个新闻判断，我会说：它不是形式化验证的失败，而是形式化验证第一次以一种非常公众化、非常戏剧性的方式，证明了自己既强大，又不该被神话。真正成熟的工程体系，不该是“有了证明就万事大吉”，而应该是“证明、模糊测试、静态分析、运行时审计”一起上。数学负责减少错误，攻击模拟负责提醒我们哪里还没被数学照到。

这大概才是未来软件安全最像样的样子。