Claude 形式化验证实战：不用重写代码，把 OSS-Fuzz 的模糊测试换成汇编级证明

一、规格只有一句话，但它是全集量词#

目标定得很克制，也正因如此才可能做到。被验证的性质是「No crash」：对于任何小于 64MB 的输入，程序都不会崩溃。前提条件写得很明确——被测对象是单线程、静态链接、使用 musl libc 的 RISC-V 二进制，在 Linux 上运行，内存预算固定。

注意这里的量词是「任何输入」。模糊测试能覆盖的是「我试过的那些输入」，形式化证明覆盖的是「所有满足前置条件的输入」。前者是采样，后者是全覆盖——这就是为什么一个需要 64MB 输入加 2GB 内存才能触发的越界读，模糊测试几乎不可能命中，而证明能指出它存在。

规模给人的直观感受是这样：约 1.8 亿行 Rocq 证明，单个典型证明约 60 万行；而它证明的那个中位二进制，只有约 1.8 万条 RISC-V 指令。证明与代码的比例是几千比一，这个数字解释了为什么这件事以前没人做得起来。

二、信任基座：不要把它读成「AI 说证明对了」#

形式化验证的价值全部取决于你最小必须相信什么。这次的设计里，需要信任的东西被压缩到四类，而且都写在开源仓库里：

1. Rocq 内核，包括它的字节码机器（vm_compute）以及 toolchain/allowed-axioms.txt 里列出的公理白名单；
2. LPS（Linux Process Semantics），即以 release.yaml 指定的那个 commit 为准的 RISC-V + Linux 进程语义模型；
3. 把 ELF 变成 LPS 内存镜像的工具链：LPS 的 elf-snapshot，以及 rocq-read-file 0.0.2（一个在编译期把镜像字节读进 Rocq 的 OCaml 插件）；
4. oft check 本身：它生成的包装器和它对 Print Assumptions 输出的解读。

关键设计在最开头那段话里：他们没有把待验证的 C 代码翻译成别的语言再验证，也没有重写被测程序。验证的对象就是机器码。这个选择换来的好处很实在——你不需要先相信一个「编译器保留语义」的翻译过程，墙上的裂缝少了一条。

证明也不是「跑个 AI 看它说 OK」。oft check 的流程是硬的：先按 SHA-256 校验每个二进制、构建内存镜像与定理陈述、编译每条证明，再编译一个把证明的定理赋予陈述类型的包装器，最后读取 Print Assumptions 的输出，拒绝任何不在允许清单里的假设。CI 里 push 到 main 会全量检查一遍，每周还会带缓存地再跑一次全量。也就是说，任何人都能重新检查这份证明，而不是只能相信一份报告。

三、它真的找出了 bug，而且找到的是模糊测试找不到的那类#

下面是官方列出的具体战果，我挑几个最能说明问题的：

• 一个解压器里的计数器下溢，最终导致越界写，触发条件是约 20MB 的输入；
• 一个解压器里的越界读，需要 64MB 输入 + 2GB 内存才够触发——这类条件组合基本落在模糊测试的盲区里；
• 一个需要跨两个句柄的特定调用序列才能触发的越界读，同样属于「路径长、概率低」的类型；
• 重新发现了 CVE-2026-56132（libexpat，需要深层嵌套输入），也就是一个已经被记录在案的漏洞；
• 一个逻辑 bug：某个文件限制功能并不总是被强制执行。这类问题既不是内存安全，也不一定会让进程崩溃，模糊测试天然抓不到。

还有两个跨越「只查内存安全」边界的例子值得一提。其一是 cpp-httplib：为了证明它，Claude 得先证明 libc++ 的红黑树深度在对数级别有界——而且是在机器码层面证明的。其二是官方把 RFC 1950 zlib 规范本身写成了 Rocq，然后证明 Linux 内核里的 zlib 在 x86 二进制层面确实实现了这份规范（连 x86 的语义也是 Claude 生成的）；官方称这个过程在官方参考文档里找出了数百处错误，还捎带发现了几个硬件层面的问题。

另外两组数字放在一起看很有意思：一个用 Verus 写的 Rust 版 Python 解释器，证明它在 170 万个随机程序上与参考实现行为一致的比例是 99.95%；而一个 PDF 阅读器项目，在一周内找到的安全漏洞数量相当于它通常一年收到的量。

四、成本才是这条路线真正的变量#

形式化验证的瓶颈从来不是「能不能做」，而是「单位成本」。这次公布里有两组关于效率的数字：

• 对同样的 36 个小型验证任务，Opus 5.5 比 Opus 5 少用约 40% 的 token；
• 让多个智能体共享同一个工作区，token 用量再降约 17%。

还有一条容易被忽略的工程决策：他们对「打补丁式」的提交扣分，对能证明「哪些输入的行为因此改变」的提交给额外加分。这是在训练/提示层面压制 reward hacking——如果只奖励「证明通过」，模型最省事的做法是去改规格或者绕过难点；把「改了什么、影响集合是什么」显式地变成得分项，模型才被迫去说清楚自己的改动。

累计投入也要说实话：据官方附录，全流程写下的 Rocq 证明总量约 10 亿行，而最终站住的是约 1.8 亿行。也就是说，八成的证明工作是失败的尝试。这个比例比任何宣传语都更能说明这项工作的性质——它不是「AI 一次写对」，而是「AI 把试错成本压到了人力做不到的量级」。

五、你现在可以自己检查一份证明#

这是这篇最实用的部分。已开源的仓库有三个：theorem-labs/oss-verify-proofs（证明本体）、theorem-labs/rocq-linux-process-semantics（LPS）、theorem-labs/oss-verify（流程与工具链）。官方 README 给出的检查命令可以照抄（依赖 Docker、zstd、带 PyYAML 的 Python 3）：

git clone https://github.com/theorem-labs/oss-verify-proofs && cd oss-verify-proofs
./oft fetch coturn                     # 拉取项目二进制，每个都按 SHA-256 校验
python3 -m pip install --require-hashes --target "$HOME/oft-pydeps" -r tools/oft/requirements.txt

docker run --rm --network none -u "$(id -u):$(id -g)" -e HOME=/tmp -e PYTHONPATH=/pydeps \
  -v "$HOME/oft-pydeps:/pydeps:ro" -v "$PWD:/work" -w /work \
  ghcr.io/theorem-labs/oss-fuzz-theorems-checker@sha256:cc9ae43a9f4b0dd59d7c8d30727d36e039bfe72a2a9f9c4a99c68e413037e902 \
  ./oft check coturn/FuzzStunClient --parts statements,proofs

两个实战提醒：镜像不含 PyYAML，所以要把依赖目录挂进去；资源上，16 核检查一份证明最多可能吃到 20 GiB 内存，因为它是「一个核编一个文件」，核越多内存越要加，用 docker run --cpuset-cpus 限制核数就行。想加项目，官方还放了一个 Claude Code 技能（.claude/skills/add-project/SKILL.md），思路是给它一个 OSS-Fuzz 项目名，在 Docker 里跑几轮。

六、用一个二十行的 Z3 例子体会「把测试写成规格」#

真正的管线是 Rocq 加 RISC-V 内存模型，重到不适合在博客里跑。但它的思想可以用 Z3 二十行体会到：把一个「崩溃检查」写成规格，然后让求解器去反驳它。

模型很简单：一个 8 字节缓冲区，解析器要读表头给的偏移量处的两个字节，要求 buf[off] 和 buf[off+1] 都不越界。

from z3 import BitVec, BitVecVal, Solver, UGE, ULT, unsat

BW, BUFLEN = 32, BitVecVal(8, 32)

def check(guard_kind):
    s = Solver()
    off = BitVec("off", BW)
    s.add(UGE(off, BitVecVal(0, BW)))
    s.add(ULT(off, BitVecVal(16, BW)))       # 偏移量是外部输入，先限个范围

    guard = {
        "safe":       off + 2 <= BUFLEN,     # 读两个字节，就检查两个字节
        "off_by_one": off + 1 <= BUFLEN,     # 只算了 buf[off]，漏了 buf[off+1]
        "loose":      off <= BUFLEN,         # 常见写法：拿 <= 长度当上界
    }[guard_kind]
    s.add(guard)
    s.add(UGE(off + 1, BUFLEN))              # crash 条件：第二个字节落在缓冲区外

    r = s.check()
    if r == unsat:
        return "UNSAT → 证明通过：不存在任何越界输入", None
    return "SAT → 存在反例，证明失败", s.model()[off].as_long()

for kind in ("safe", "off_by_one", "loose"):
    verdict, ce = check(kind)
    print(f"{kind:<11}{verdict}" + (f"，反例 off = {ce}" if ce is not None else ""))

实测输出（我在本机跑的，Z3 版本 5.3.1.0）：

safe       UNSAT → 证明通过：不存在任何越界输入
off_by_one SAT → 存在反例，证明失败，反例 off = 7
loose      SAT → 存在反例，证明失败，反例 off = 8

怎么读这三个结果：safe 的 UNSAT 意思是，在 off ∈ [0,16) 这个范围内不存在任何能让第二个字节越界的输入——这已经是一句全覆盖的断言了，不是「我试了 16 次都没崩」。off_by_one 和 loose 返回 SAT，附带具体反例：off_by_one 给的是 off = 7（7+1 <= 8 通过检查，但读 buf[8] 越界），loose 给的是 off = 8。SAT 附带的反例就是 bug 的最小复现，可以直接写成测试用例。

我也把「跑穷举测试」的结果放在一起对照：同样把 off 从 0 到 15 全跑一遍，off_by_one 和 loose 都能发现首个越界值 off = 7，safe 则一个都发现不了。在这个 8 字节玩具例子上一遍全跑就能覆盖，所以两者看不出差距——但当输入是 64MB 的缓冲区、路径是几万条指令的调用序列时，「跑一遍」就不再是选项了。

这里我踩了一个值得写下来的坑。 第一版我把不变量写成 need < length，而 need 在这个模型里恒等于 length，于是整个约束集合不可满足——求解器干脆利落地返回了 UNSAT。但那是空证明：规格自相矛盾，什么都证明不了。这正是形式化验证里最危险的失效模式，也是官方为什么把「精确的定理陈述」明确列进信任基座的原因。写规格比写代码更容易骗自己。

还有一个会改变成本曲线的事实：证明可以复用。因为所有证明都建立在同一套 RISC-V + Linux 进程语义之上，某个程序里已经证过的辅助定理（比如某种解析循环的不变量、某种内存布局的性质），往往能被另一个程序直接引用，不用从头再证一遍。官方把这列为「证明可复用」，含义很直接：单位成本会随着证明库变大而下降。这也是这条路线和「每换一个项目就把符号执行从头跑一遍」在结构上最大的差别——前者攒的是资产，后者每次都在重复劳动。

七、别过度解读：官方自己标出的局限#

这段是官方文档里写的，逐条照抄要点：

• 证明「不崩溃」不等于证明「没有 bug」。官方明确说不希望这些证明被理解为「代码已被证明无 bug」；
• ASan 检测不到所有内存安全 bug，未初始化的读取就是一类典型；
• 有些情况下断言会在坏访问之后才失败，导致过近似（over-approximation）——也就是说证明为真的性质，未必是运行时最紧的那条；
• 他们没有验证所有入口点。这一点在读新闻时特别容易混淆：博客口径是 123 个库 / 239 个入口点，而已发布的证明仓库里写着 60 个入口点 / 25 个库。这两个数不矛盾，是「做过的工作量」和「通过检查并公开的证明」两回事，但媒体把两者混着写的时候，读者会以为 123 个库的证明都能下载下来。

总结#

这次发布最值得记住的不是某组数字，而是方法上的三个可复用点。

一是验证对象直接取机器码：不重写、不翻译，少掉一整条需要信任的链路，也让「证明」能覆盖真实发布的那个二进制。二是信任基座被显式列出并开源可检：Rocq 内核 + LPS 语义 + ELF 转换工具 + oft check，外加一份公理白名单；Print Assumptions 拒绝白名单外的假设，CI 每次 push 全量复检。三是把成本量化下来：约 1.8 亿行证明、单证约 60 万行、中位二进制约 1.8 万条指令、全流程写下约 10 亿行、模型换代 token 少约 40%。

对我们这些维护自己基础设施的人，最实际的收益是两条：「证明能像测试一样被复跑」这件事已经成立了（./oft check coturn/FuzzStunClient 就是一条命令），以及规格比代码更需要被审查（我那个空证明的坑就是明证）。如果这条路线继续降价，五年后回头看，「只跑 fuzzing 就等于做了内存安全」很可能会像「只跑单元测试就说系统没有并发 bug」一样，显得太乐观了。