Claude 给 123 个开源库写“数学证明”：RISC-V 汇编级形式化验证，1.8 亿行 Rocq 几乎零人工复核

Anthropic 这篇研究博客的开篇第一句，就带着一种少见的紧迫感："Most software is riddled with bugs, which AI can now easily find and exploit."（大多数软件都充满 bug，而 AI 现在能轻易地找到并利用它们。）

这不是危言耸听。就在同一周，一个 OpenAI 模型协助找出了 PHP2Shell 漏洞；Anthropic 自己刚让 Claude 给 OpenSSH 等 25 个开源项目做了"缩圈"（删掉不需要的代码，缩小攻击面）。AI 找 bug 的能力正在指数级上升，而传统的防御——测试、fuzzing、代码审计——本质上都是"抽查"：你永远不知道还有多少 bug 躲在没测到的角落里。

10 月 22 日，Anthropic 扔出了一颗更大的炸弹。他们和形式化验证创业公司 Theorem 合作，让 Claude 干了一件以前只有顶尖专家团队花几年才能干的事：给 123 个真实世界的开源库，写出了"数学证明"——在 RISC-V 汇编指令级，证明它们永远不会崩溃。用 Anthropic 自己的定性："据我们所知，这是第一次大规模用 AI 对生产软件做汇编级的形式化验证。"

注意这个措辞的份量。"形式化验证"（formal verification）不是"测得更狠"，而是换了一套游戏规则：不再是"跑一万个输入都没崩，所以大概没 bug"，而是"数学上证明了，对所有可能的输入，都不可能崩"。AI 安全，第一次从"找 bug"升级到了"证明无 bug"。

它是怎么做到的：把 fuzz 测试翻译成定理

整个 pipeline 的设计非常漂亮，值得拆开看：

第一步：找现成的"规约"。形式化验证最难的一步，是先说清楚"正确"是什么意思——给程序写数学规约（specification）。Anthropic 取了个巧：直接用 Google OSS-Fuzz 项目里现成的 fuzz 测试。OSS-Fuzz 从 2016 年开始给开源 C/C++ 项目做持续 fuzz 测试，每个测试都有一个入口点（entry point），规则很简单：任何让程序崩溃的输入，就是开发者在乎的 bug。Anthropic 把这条规则翻译成形式化规约："这个测试，对任何小于 64MB 的输入，永远不会崩溃。"

第二步：在机器码上证明。库和它的 fuzz 测试被编译成 RISC-V 可执行文件（带 AddressSanitizer 插桩，内存访问违规就会崩）。Theorem 提供的 RISC-V 指令语义和 Linux 进程语义，加上"不崩溃"这个性质，机械地生成证明题目。Claude 负责写证明——用 Rocq（前身叫 Coq）这个证明助手语言。

第三步：机器检查。Rocq 的证明检查器（kernel）逐行验证证明是否成立。这一步是纯机械的：通过就是通过，不通过就是不通过，不需要人类"相信"任何论证。

几个数字感受一下规模：239 个入口点、123 个库、几周时间、约 1.8 亿行 Rocq 证明。一个典型的证明约 60 万行，对应的二进制中位数是 1.8 万条 RISC-V 指令。也就是说，证明是代码的 30 多倍大——这正是形式化验证历史上贵得离谱的原因。

而最关键的一句是 Anthropic 反复强调的：这 1.8 亿行里，几乎一行都不需要人工 review。因为检查器是机械的，你需要信任的东西只有四样：RISC-V 的形式化模型、Linux 进程的形式化模型、被证明的定理陈述本身、Rocq 检查器本身。就这四样。剩下的 1.8 亿行，对错由机器判定。

为什么这事以前做不到：seL4 的 20 人年

要理解这次突破的份量，得先知道形式化验证过去有多贵。Anthropic 在博客里举了业界最著名的例子：seL4 微内核——写代码用了 2 个人年，形式化验证用了 20 个人年。证明工作量是写代码的 10 倍，需要的是全球稀缺的专家。

这就是为什么形式化验证过去只出现在"不容有失"的地方：空客的航电代码、军用系统、密码学库。普通开源项目？想都别想——谁出得起 20 人年去证明一个 JSON 解析器？

LLM 改变的是成本结构，不是原理。Claude 证明的这 123 个库，恰恰是"普通开源项目"：cJSON、libexpat、各种解压缩库、图片解码器——全是你每天都在用、但没人会花 20 人年去证明的东西。Anthropic 的论点是：当写证明的成本从"专家年"降到"token 账单"，形式化验证就能从"镇国重器"变成"常规工具"，就像当年的静态类型和单元测试一样，从"可选"变成"标配"。

成本还在继续下降。Anthropic 做了个对照实验：36 个小型验证任务，Opus 5.5 完成一半任务只用了 Opus 5 约 60% 的 token（省 40%）。而且证明可以复用——让多个 agent 在共享工作区里互相抄作业（证明里大量重复的是 C 运行时和 ASan 初始化代码），token 消耗再降 17%，还有两个任务是单干做不出来、抄作业做出来的。这很像 Mathlib（Lean 的数学库）当年的生长方式：证明越积越多，后人站在前人肩膀上。

诚实限定："被证明了"不等于"没 bug"

Anthropic 专门用了一整节讲 limitations，这种诚实值得尊重，也值得每个读者读完再激动。核心就一句："Formally verified" does not mean "bug-free."（"形式化验证过"不等于"没有 bug"。）

证明的保证，是有严格边界的：它假设程序是单线程、静态链接、有固定内存预算、跑在 RISC-V CPU 的 Linux 上。而现实世界里，这些库绝大多数跑在 x86 或 ARM 上，动态链接 glibc。RISC-V 上证明了不崩，不代表你服务器上的 x86 版本不崩——中间隔着指令集语义和 libc 实现的差异。

另外，证明只覆盖了"内存安全 + 不触发断言"这个性质。ASan 检测不到的内存安全问题、业务逻辑错误（比如算错了但没崩），都不在保证范围内。而且 123 个库并没有每个入口点都被证明——只证明了 239 个 fuzz 入口。

但 Anthropic 的回应也很漂亮：这些限定恰恰告诉你"剩下的 bug 可能藏在哪"——要么在四个信任基里（RISC-V/Linux 语义模型、定理陈述、检查器），要么在证明范围之外。把"不知道哪里有 bug"的无限问题，收敛成"加固四个信任基"的有限问题，这本身就是巨大的进步。加固信任基的成本，被所有用了这些证明的项目分摊——证明一次，全生态受益。

副产品比主产品还值钱：几百个"万亿次测试都没发现"的 bug

这项研究最有戏剧性的部分，不是那 1.8 亿行证明，而是写证明的过程中顺手挖出来的几百个 bug。

逻辑是这样的：Claude 写证明时如果卡住了，往往意味着代码里真有个 bug——因为"证明所有输入都不崩"这件事，在有 bug 的代码上是不可能完成的。Anthropic 允许 Claude 直接修掉它找到的 bug（修完重新生成规约、重新证明），结果挖出了一堆 fuzzing 跑了万亿次都没发现的东西：

• 一个解压缩库里的计数器下溢，导致越界写——但只在约 20MB、且有某种极罕见布局的输入下触发。Fuzzer 的输入通常上限 1MB，且靠代码覆盖率引导，永远走不到这个角落。
• 一个图片解码器的越界读，需要 64MB 输入 + 超过 2GB 内存。Fuzzer 的资源预算根本够不着。
• CVE-2026-56132（libexpat）：需要深度嵌套输入才能触发，被 Claude"重新发现"了一遍。
• 还有一类更狠的：根本不崩溃的逻辑 bug。比如某个库有个"限制应用只能加载特定文件"的安全功能，Claude 在证明内存安全时顺手发现这个功能"并不总是生效"——fuzzing 永远发现不了，因为它不触发崩溃。

另外两个实验更说明问题：Anthropic 让 Claude 给 Linux 内核的 zlib 实现写了 RFC 1950 的形式化规约并证明（x86 二进制级），顺手发现了几个"不可利用的边角 bug"；在一个 PDF 阅读器的验证尝试中，一周发现的安全 bug 数量，相当于平时一年的报告量；还有一个潜伏了十多年的逻辑 bug，被揪了出来。

这段的潜台词很值得品味：fuzzing 是"抽查"，证明是"普查"。抽查再努力，也有抽不到的角落；普查一遍，所有角落无所遁形。Anthropic 的数据第一次量化了这两者的差距：万亿次测试 vs 一次证明。

和《Claude 给 OpenSSH 缩圈》的划界：两种安全范式

还记得 cycle87 那篇《Claude 给 OpenSSH 等 25 个开源项目缩圈》吗？那篇讲的是 Anthropic 让 Claude 给知名开源项目删除不需要的代码——攻击面缩减（attack surface reduction）。这篇讲的是形式化验证。两者都是"Claude 搞开源安全"，但范式完全不同，一句话划界：

缩圈是"做减法"：把可能藏 bug 的代码删掉，让攻击者无处下手。这篇是"做保证"：代码留着，但数学上证明它不会崩。

前者的哲学是"代码越少越安全"——删掉用不到的协议、关掉默认开启的功能，bug 自然跟着消失。后者的哲学是"你不需要删，只要能证明"。一个是从外部缩小战场，一个是从内部确立秩序。

有意思的是，这两种范式在 Anthropic 手里是组合拳：先缩圈（把没用的代码删了，证明对象变小），再验证（对剩下的核心代码做证明，成本更低）。博客里虽然没明说，但逻辑上这两件事是互相成就的——要证明的代码越少，证明越便宜。对开源维护者来说，现实路径可能是：先用缩圈把项目瘦身，再用形式化验证给核心路径上"数学保险"。

为什么"证明"比"测试"更适合开源生态：依赖的幂律

这项研究还有一层容易被忽略的战略意义，藏在 Anthropic 的一句话里："Dependencies follow a power law: proving even a small set of shared libraries makes a huge swath of software feasible to prove."（依赖服从幂律：证明一小部分共享库，就能让一大片软件变得可证明。）

想想你的应用依赖了多少开源库：直接依赖几十个，传递依赖几百个。每个库的作者都"测过"，但测试是不传递的——A 库测过 + B 库测过，不等于 A+B 测过。组合爆炸让"全测一遍"永远不可能。这就是现代软件供应链的真相：我们站在几百个"大概率没问题"的库搭成的塔上，心里其实没底。

证明的美妙之处在于它是可组合的。一个库被证明了"内存安全"，所有依赖它的上层代码，自动继承这部分保证，不需要重新证明。而依赖是幂律分布的：glibc、OpenSSL、zlib、libexpat 这几个"地基层"库，被几百万个项目依赖。Theorem 的路线图（验证整个 Nix 生态，从 glibc、OpenSSL、cURL 开始）打的正是这个算盘：先证明地基，再一层层往上盖。这和 Mathlib 的生长逻辑一模一样：先证明基础定理，后人直接引用。

所以 123 个库这个数字，别只看"多"，要看"准"——它们全是 OSS-Fuzz 里的高频基础库。证明它们的性价比是最高的：一次证明，几十万个下游项目间接受益。这也是为什么 Anthropic 说"形式化验证会从外挂变成内置"：未来的包管理器，可能会像今天显示"下载量"和"许可证"一样，显示"已验证"的徽章。

攻防天平的第一次倾斜：防守方的新武器

回到开篇那句"AI 能轻易找到并利用 bug"。过去两年，AI 在安全领域一直是"攻"大于"守"：找漏洞的 agent 越来越强，修漏洞的还是人。上周 PHP2Shell 的例子就是缩影——AI 帮着找到了漏洞，然后人类熬夜打补丁。攻防两端，AI 的加持是不对称的。

形式化验证是第一次给防守方发了不对称武器。攻击者的优势在于"只需要找到一个 bug"，防守者的劣势在于"要堵住所有 bug"——而证明恰恰是"堵住所有 bug"的数学工具。当 Claude 能证明"这个入口对所有输入都不崩"，攻击者在这一层的 fuzzing 就彻底失业了：不是"更难找到 bug"，是"这一类 bug 被数学注销了"。

当然，军备竞赛不会停止。Anthropic 自己也承认：证明只覆盖了内存安全和断言，逻辑漏洞、配置错误、供应链投毒都不在范围内。攻击者会转向证明覆盖不到的地方。但这恰恰是进步的形态：把"低级错误"用数学方法批量消灭，让攻防双方都去卷更高级的问题。就像内存安全语言（Rust）消灭了一大类内存 bug 之后，漏洞研究转向了逻辑漏洞——不是终点，但是水位上涨。

对独立开发者来说，这一层的意义更直接：你引入的每一个开源依赖，未来都可能带着"已证明"的标签。你不需要懂 Rocq，不需要会写规约——你只需要会看那个徽章，就像今天你会看"周下载量"和"最近更新时间"一样。形式化验证的民主化，最终表现形式可能就是这么朴素：npm install 之前，多看一眼。

对开发者的实际意义：免费 pipeline 已经开了

这篇研究不是纯学术秀肌肉，它的"产品化"动作很实在：

第一，Theorem 开了 OSS Verify 计划，给符合条件的开源项目免费跑这套 pipeline。接入方式是提 PR（加 project.yaml、Dockerfile、build.sh），Theorem 按类似 OSS-Fuzz 的标准评审，优先覆盖"用得广的关键基础设施"。维护者最后拿到的是：Rocq 检查器验证过的"你的 fuzz 目标在 64MB 以下输入永不崩溃"的证明；过程中发现的 bug 会私下邮件披露，没有公开期限。路线图更激进：验证整个 Nix 生态，包括 glibc、OpenSSL、cURL——也就是现代软件栈的地基。

第二，发布了 Claude skill，帮助开发者自己上手验证代码。Anthropic 在博客结尾直接喊话："We encourage all developers to explore formal verification with LLMs — especially those who previously tried it with less capable models and found it didn't work."（我们鼓励所有开发者用 LLM 探索形式化验证——尤其是那些以前用能力不足的模型试过、觉得行不通的人。）

第三，证明和语义模型开源了。部分证明、RISC-V 和 OS 语义、没证出来的 fuzz 目标的规约，都放到了 GitHub 上。任何人都可以独立验证——这就是"证明"相对"论文"的优势：你不需要相信 Anthropic 的论证，你只需要跑一遍检查器。

对 vibe coding 的读者来说，还有一层意味深长的：AI 写的代码，正在被 AI 证明是对的。我们担心"AI 生成的代码有没有 bug"，Anthropic 的回答是：让另一个（更严谨的）AI 流程去证明它。写代码的 agent 和写证明的 agent，一个负责快，一个负责对——这可能是未来软件工程的标准分工。

结语：安全的"确定性"第一次有了价格标签

软件安全历史上，"确定性"一直是奢侈品。测试只能给"大概率没问题"，fuzzing 给"跑了很多遍没问题"，只有形式化验证给"数学上不可能有问题"——但贵到只有空客和军方用得起。

Anthropic 这次做的，是第一次给"确定性"标了个普通人付得起的价格：几周、token 账单、123 个库。它不完美（RISC-V 假设、只证了内存安全、只覆盖了部分入口），但它把一条路走通了：从"专家手工证明"到"LLM 规模化证明"，从"镇国重器"到"开源基础设施标配"。

Anthropic 在结尾写道：形式化验证会像静态类型和测试框架一样，从"外挂"变成"内置"。这句话的潜台词是：未来的 CI pipeline 里，"跑测试"和"跑证明"会是并列的两步——前者告诉你"这次改动没把已知功能搞坏"，后者告诉你"这次改动不可能引入某类 bug"。当证明的成本降到和 fuzzing 一个量级，不做证明的项目，就像今天不写测试的项目一样，会显得不专业。

从"找 bug"到"证无 bug"，差的不只是技术，是整个安全观的升级。而这一次，升级的按钮是 AI 自己按下的。

一手来源：Anthropic 官方研究博客《LLMs are making formal software verification feasible at a much larger scale》，发布于 2026-10-22（页面标注 Published: 2026-10-22T00:00:00.000Z，Updated: 2026-10-23T17:10:27.000Z）；交叉印证：Unite.AI 同日独立报道《Anthropic Says Claude Proved Security Properties Across 123 Libraries》（2026-10-22），以及 siliconnoon、AI Weekly 的同步分析。题图为芯片裸片显微实拍（Hackaday RISC-V 项目），意在呼应"汇编指令级"这一核心事实。