Claude 给 123 个开源库写了形式化证明：在汇编层证明「永不崩溃」，还挖出跑了万亿次测试都没发现的 bug

软件行业有一个心照不宣的事实：测试只能证明 bug 存在，不能证明 bug 不存在。一个库跑了万亿次模糊测试没崩，不代表第一万亿零一次不会崩。真正能给出「不会崩」这份保证的，是形式化验证——把代码翻译成数学模型，证明它永远满足某组安全规则。问题是这件事过去太贵了：seL4 内核写了 2 人年，验证它花了 20 人年。

一分钟速览

• Anthropic 与 Theorem 合作，用 Claude 在 RISC-V 汇编层为 123 个真实开源库证明了安全属性。
• 证明内容：对任何小于 64MB 的输入、任何建模的 Linux 响应与内存布局，程序都会正常退出，不触发内存安全错误或断言失败。
• 这是已知首次大规模用 AI 把形式化验证应用到生产软件的汇编层。
• 写证明的过程中，Claude 发现了此前逃过数万亿次测试运行的 bug。
• Anthropic 公开了部分证明以及 RISC-V 与操作系统语义，Theorem 发布了一个 Claude skill 帮开发者上手。

把模糊测试变成一条定理

这项工作的巧妙之处不在「让模型写证明」，而在「让模型知道要证明什么」。形式化验证最大的障碍往往不是证明本身，而是规格说明：一个文本编辑器怎样才算「正确」？一个浏览器呢？规格写不清楚，证明就无从谈起。

Anthropic 的做法是把已有的模糊测试套件转成规格。模糊测试的逻辑是：给程序入口喂大量半随机输入，谁崩了谁就是 bug。团队把「这个模糊测试永不崩溃」编码成一条针对编译后 RISC-V 指令的规格，再配上一套通用的 Linux 执行模型。于是原本只能靠穷举逼近的目标，变成了一条可以被证明的命题：对任何小于 64MB 的输入，程序都不会崩。

如果证明成立，这个入口上的模糊测试就变得多余——因为穷举永远找不到反例。这就是从「测试」到「证明」的跨跃：前者是采样，后者是全称量化。

为什么是汇编层

选择在汇编层做证明，而不是在 C 源码层，是个有分量的决定。源码层的证明依赖编译器的正确性假设：你证明的是「这段 C 代码正确」，但用户跑的是编译器生成的机器码。编译器优化、未定义行为、内联汇编，都可能让源码证明与最终产物脱节。直接在 RISC-V 汇编上证明，等于把编译器也纳入了信任边界之内。

代价是难度陡增。汇编指令数量庞大、状态空间复杂，证明规模往往是原代码的数倍。这正是 LLM 的用武之地：在数百万行代码里朝着一个明确定义的目标推进，是模型擅长而人类疲惫的工作。

它到底证明了什么，没证明什么

需要把边界说清楚。这次证明的是「程序在特定假设下不会崩溃」：单线程静态二进制、固定内存预算、RISC-V CPU、Linux 系统、输入小于 64MB。它证明的是内存安全与断言不会失败，不是「程序功能正确」，更不是「没有逻辑漏洞」。

但这已经比过去实用得多。内存安全错误长期是软件漏洞的主要来源，OSS-Fuzz 生态里大量项目跑的就是 AddressSanitizer——一旦非法访问内存就崩溃。把这些模糊测试目标转成「永不崩溃」的定理并证明成立，等于把一整类漏洞从可能性里划掉。

Anthropic 也提到在探索其他形式化方法：评估 zlib 压缩算法的安全性、证明一个用 Rust 写的 Python 解释器行为等价、清除关键软件里的陈年 bug。这些是不同方向的尝试，不是同一套流水线的复制。

成本曲线在往下走

这项研究最值得关注的不是「AI 能写证明」，而是成本结构的变化。证明成本由两部分组成：写证明的人力，和可复用的基础设施。模型变强，第一部分在降；语义模型、证明库、跨代码库的复用，让第二部分被摊薄。Anthropic 的判断是，随着更多代码被形式化、方法标准化，证明可以在代码库之间迁移和修改，单位成本会持续下降。

这会改变形式化验证的适用边界。过去它只出现在空客航电、内核这类「出错就死人」的场景，因为只有这些场景付得起 20 人年。当成本降到「一个团队一个季度」的量级，数据库、加密库、解析器、协议实现这些「出错就泄密」的组件就会进入名单。

对开发者的实际建议

Anthropic 在文末说了一句很实在的话：鼓励所有开发者尝试用 LLM 做形式化验证，尤其是那些以前试过、因为模型不够强而放弃的人。这句话指向一个具体动作——如果你手上有一个跑了很多年模糊测试的关键库，现在是重新评估形式化验证成本的时点。

但也有必要保持克制。形式化验证证明的是「符合规格」，规格写错了，证明再漂亮也没用；假设变了（多线程、动态内存、不同架构），证明就失效。它是安全工程的一层，不是替代品。真正成熟的做法，是把证明当作持续集成的一部分：代码改了，证明重新跑，规格和实现一起演进。

从行业角度看，这件事和英伟达开源 OpenShell 时的思路是同一条线：当智能体开始自己写代码、自己改策略，人类需要的不是更多的测试，而是可机器检查的保证。形式化验证从学术象牙塔走向工程流水线，可能比模型再涨几分更能改变软件的质量基线。