一周 1.8 亿行证明：一件小事的量变

2026 年 10 月，Anthropic 的 Frontier Red Team 与初创公司 Theorem 发布了一项工作：用 Claude 对 123 个真实开源库（来自 Google OSS-Fuzz 项目）在 RISC-V 汇编层证明安全属性——对任意小于 64MB 的输入、建模的 Linux 内存布局，程序不会触发内存错误或断言失败。数周之内，Claude 产出了约 1.8 亿行 Rocq 证明代码，覆盖 239 个入口点；单个证明平均约 60 万行，对应中位数 1.8 万条 RISC-V 指令的二进制。

这件事在 Hacker News 上拿了 436 分，但它的分量远不止一个热帖。把它放进软件工程五十年的历史坐标里看，这是一条被反复验证的曲线的又一个陡峭拐点：形式化验证的成本，正在从"人年"坍缩到"token"。

软件正确性：五十年的概率游戏

先回到问题的原点。软件工业对"正确性"的承诺，本质上一直是概率性的：

  • 测试是抽样。你跑一万个用例，只能说明这一万个输入没问题，不能说明第一万零一个没问题。
  • Fuzzing 是暴力抽样。OSS-Fuzz 对开源项目做持续随机输入轰炸，累计执行了数万亿次运行，确实挖出了成千上万的 bug——但抽样永远是抽样，Go 的 fuzzer 跑一百年也"证明"不了任何东西。
  • 形式化验证是另一条路：把程序翻译成数学模型，用定理证明它永远不违反某条规则。它给出的是全称量词级别的保证——对所有输入，而不只是测过的输入。

这条路的代价是出了名的。经典案例是 seL4 微内核：实现花了 2 人年，形式化验证花了 20 人年。因此几十年来，验证只属于 Airbus 航电、seL4 这类极端任务关键场景，普通项目连想都不用想。工业界的现实是：Linux 内核这种被测试覆盖到牙齿的软件，近年仍一次性披露上千个漏洞。

LLM 补上了最贵的那块拼图

形式化验证的瓶颈从来不在于理论——Rocq（原 Coq）的内核检查器几十年前就有了，而且极小、极可靠。瓶颈在于写证明太贵：证明的规模通常是代码的几十倍，且需要极小众的专家技能。

这恰恰是 LLM 的甜区。Anthropic 的流水线值得拆开看：

  1. Spec 从哪来？ “程序正确"对大多数软件很难定义（什么叫一个文本编辑器"正确”？）。他们的取巧之处是：把项目已有的 fuzz 测试套件自动转成规约——“这个测试对任意输入都不崩溃”。规约来源问题被工程化绕开了。
  2. 在哪个层面证明？ 不是源码，而是编译后的 RISC-V 汇编，配合 Theorem 形式化的 RISC-V 指令语义和 Linux 进程语义。这意味着证明直接锚定在最终执行的产物上，绕过了"编译器是否可信"的经典争论。
  3. 谁写证明？ Claude 全自主生成证明，Rocq 内核机械检查。证不出来，意味着代码可能真有 bug——失败本身即信号。
  4. 闭环。 证明过程中 Claude 顺手修复了数百个 bug，其中不少是数万亿次 fuzz 运行都没撞出来的存量缺陷：某流行 PDF 阅读器一周内被发现相当于过去一整年报告量的安全 bug；还有一个潜伏了十年以上的逻辑错误被揪出。

注意这里的分工：LLM 负责"不可靠但便宜"的证明生成，定理证明器内核负责"绝对可靠"的检查。 这是一个聪明的架构——它没有让 AI “相信"自己写的代码是对的，而是让 AI 承担体力活，把最终的裁判权交给几万行经过数十年审查的内核代码。幻觉在这个体系里没有生存空间：证明检查不过就是不过。

它不是银弹：诚实地列出边界

这项工作离"软件没有 bug"还很远，Anthropic 自己也列得很清楚：

  • 条件苛刻：单线程、静态链接、固定内存预算、RISC-V + Linux、输入 <64MB。真实部署中这些库跑在 x86/ARM 上、多线程、动态链接。
  • 规约是窄的：“不崩溃"只是内存安全，不是功能正确。一个会返回错误结果的程序也能通过这个证明。
  • 成本仍高：单个证明要烧掉数亿 token，Anthropic 没有公布总账单。但趋势乐观：Opus 5.5 用比 Opus 5 少 40% 的 token 解出了一半的证明。
  • 语义基础是人工的：Theorem 的 RISC-V/Linux 形式语义是人写的，这是证明的信任根之一。

但"有边界的保证"恰恰是工程的正道。测试给的是"没发现 bug”，验证给的是"在这些假设下没有这类 bug”——后者是可以写进合同和合规框架的东西。

为什么说这是范式的起点而不是终点

我认为这条新闻真正值得记住的，是三个二阶推论：

其一，AI 写代码的信任问题有了出路。 “AI 生成的代码谁敢用"是过去两年所有技术管理者的心病。当模型能为自己生成的代码附带机器可检查的正确性证明时，代码 review 的经济学被改写了：人不审代码，人审规约。“AI 证明给自己看"听上去循环，但因为有 Rocq 内核这个外置的、确定性的裁判，这个循环是健康的。Anthropic 同期上线的 OSS Scanner（为关键开源项目做持续 Claude 漏洞扫描，此前已在 25 个项目里发现 493 个问题）正在把同一能力常态化为公共服务——研究到产品的转化周期被压缩到了周。

其二，攻防不对称正在被矫枉过正地修复。 前沿模型已经能链式利用看似无害的 bug 组合成漏洞利用。当防御方也能用同样的模型做全称量词级的验证时，安全竞赛从"谁先发现"变成了"谁能穷尽”。Theorem 的路线图已经指向 glibc、OpenSSL、cURL 这些真正的基础设施——如果未来依赖树的根节点带证明，供应链安全的图景会完全不同。

其三，证明会成为可复用的资产。 1.8 亿行证明已经部分开源在 GitHub（oss-verify-proofs），连同 RISC-V/OS 语义。证明的复用和跨代码库改编会摊薄成本——这是"证明库"这个概念第一次有实际意义。可以想象未来的包管理器里，依赖项旁边标注的不只是版本号，还有"已验证：内存安全，RISC-V，单线程”。

判断

我的预测是：三年内，“带形式化证明的 CI” 会成为安全关键开源项目的标配，就像十年前 fuzzing 进入 CI 一样。 触发条件已经齐备：证明成本随模型能力指数下降（一代模型 40% 的 token 节省）、规约生成被工程化、语义基础开始标准化、证明资产可以复用。剩下的只是工程扩散的常规节奏。

更远一点看，这件事的哲学意义在于：软件工程终于拥有了从"经验学科"走向"数学学科"的量产工具。Knuth 那句 “Beware of bugs in the above code; I have only proved it correct, not tried it” 玩笑般流传了五十年——because proving it correct 从来不是人手能批量做的事。现在，它是了。

问题从"AI 能不能编程"变成了"AI 能不能证明它写的程序是安全的"。这一周，答案向前跳了一大步。

参考：