Claude 是如何自动完成形式化验证的？从 Fuzz Harness 到 1.8 亿行 Rocq 证明的技术实现

原创

Qsec
Qsec

Qsec

2026年10月23日 15:27
上海

去阅读

Claude 是如何自动完成形式化验证的？从 Fuzz Harness 到 1.8 亿行 Rocq 证明的技术实现

2026 年 10 月 22 日，Anthropic 与 Theorem 发布了一项结果。Claude 为 123 个真实开源库生成汇编级形式化证明，合计约 1.8 亿行 Rocq 代码，由证明检查器验收。Anthropic 称这是首次大规模用 AI 验证生产软件。

传统形式化验证成本很高。seL4 内核实现花了两个人年，验证却花了二十个人年；这次公布的规模是 239 个 fuzz 入口、123 个库、数周完成。

正文沿自动验证流水线分五章：测试入口与规格、二进制语义、定理与 Proof Agent、zstd 真实证明链，以及验收机制、规模成因和边界。

图1：OSS Verify 从 fuzz 输入到 Rocq 验收的整体流水线

一、从测试入口到数学定理

从 fuzz 测试到数学规格

OSS-Fuzz 为开源项目持续运行模糊测试。一个 fuzz 目标（fuzz target）接收字节输入，调用被测库的某个入口，比如解析器。

⁠⁠⁠

intLLVMFuzzerTestOneInput(constuint8_t*data,size_t size);

fuzz 引擎不断生成半随机输入，崩溃即发现 bug；但输入空间无限，测试过的样本不能证明其他输入安全。

OSS Verify 将 fuzz 目标中的检查编码成规格，证明对所有输入都不会崩溃。检查必须写成 if (!cond) abort();，不能用 assert()，因为构建时的 NDEBUG 可能删掉断言。复杂 API 序列则可用 DSL 把输入文件解释为调用脚本，从而检查状态操作是否出错。

证明对象包含整个 fuzz 二进制，不止库代码，还包括启动代码、C 库、sanitizer 运行时和 fuzz 驱动。

二进制级验证的选择

传统形式化验证常先把 C 翻译成 Rocq 或 Lean，再证明翻译产物。OSS Verify 直接验证二进制，避免翻译错误或解释器偏差，证明对象就是用户实际运行的机器码。

目标架构是 RISC-V RV64GC，已有可复用的形式化语义基础。编译链固定为 clang 20.1.8、musl libc 和 lld，生成静态 riscv64 Linux 程序。

每个 fuzz 入口有四个构建，差异只在 sanitizer 编译标志。

sanitizer 构建是整个验证思路的支柱。内存错误这类最危险的 bug，在 sanitizer 构建里会变成一次可检测的崩溃，于是\"不崩溃\"的证明自动升级为\"内存安全\"的证明。

可复现编译是另一块基石。每个二进制的 SHA-256 被锁定进清单，证明只对锁定字节负责，构建必须做到两次独立构建产出逐字节相同的二进制。真实系统里 getenv() 返回 NULL、getpid() 返回 1，这些都是构建时的替换，目的只有一个，让程序行为只依赖输入文件，这是证明可写的前提。

二、二进制的数学语义建模

这一章回答前面抛出的问题，一个几十万条指令的真实程序，如何变成 Rocq 能理解和推理的数学对象。

从 ELF 到内存映像

第一步是 elf-snapshot 工具，它静态解析 ELF 的程序头表，取出每个 LOAD 段，输出一份内存映像（MemImage）。它不需要调试器、不需要模拟器，纯静态解析。init_pc 永远取 ELF 头里的 e_entry，内核 load_elf_binary 就是从这里接管控制流的。MemImage 记录三个东西，加载的段（地址、权限、字节内容）、入口 PC、程序头信息。整个映像有字节上限，默认 512 MiB，硬顶约 2 GiB，超过硬顶时 coqchk 无法检查，会被拒绝而不是截断。

程序状态与执行步骤

在 LPS（Linux Process Semantics，一个用 Rocq 写的 Linux 进程模型）里，一次执行的状态是一个机器状态，程序计数器、寄存器堆、内存。内存建模为\"地址到字节的部分函数\"（word -> option byte），没有映射的地址就是未映射内存，访问它会触发一次故障，而这正是\"崩溃\"的定义之一。指令执行的语义在 Riscv/Sem.v 里，系统调用语义按子系统组织在 LinuxProcessSem/Sys/ 下，每条指令和每个系统调用都有一条语义规则，描述在状态 S 下执行这一步可能到达哪些状态。

这里可以给出一个概念性的抽象，帮助理解，但不是 LPS 源码的原始定义。

S_{t+1} ∈ Step(S_t, E_t)

S_t 是 t 时刻的程序状态，E_t 是环境状态或环境在这一步做的选择，Step 描述下一步所有可能的状态变换。注意这是一个集合，执行是不确定的。read 可能返回任意非空前缀的可用字节，mmap 不带地址提示时可能返回任意空闲页对齐地址，LPS 允许 Linux 能给出的每个答案，证明必须覆盖每个答案。

这种\"关系式\"而非\"确定性函数\"的建模，正是后面所有推理的基石。Claude 不需要枚举所有输入和所有执行路径，那样不可能完成，它通过引理、抽象和归纳对一整组可能的执行行为建立数学结论。

unmodeled 的判定

这里有一个必须讲清的概念，unmodeled。LPS 描述的是受支持系统，稳定版 Linux 6.18.46（精确到内核 commit）加 QEMU 用户态模式，加上 RISC-V 规范。对模型没写规则的东西，比如一个没建模的系统调用，执行到那里就没有规则可用，这一步被标记为 unmodeled，而 unmodeled 在定理里算作一次错误。这样设计保证了 soundness（可靠性），模型宁可说\"我不管这个\"，也不假装知道。

LPS 的设计有三个优先级，依次是：

1. 1.

Sound（必须）。证明在受支持系统上为真，模型无法保证 sound 的地方就标 unmodeled。
2. 2.

Precise（目标）。模型不包含受支持系统给不出的行为。
3. 3.

Covered（目标）。模型没有 unmodeled 的漏洞。

前两条合起来是完备性，受支持系统上为真的命题，在模型里可证。第三条是理想目标，SCOPE.md 列出已知差距，这些差距直接决定证明的边界。

小黑在 LPS 规则轮上处理未建模调用

三、定理形态与证明构造

证明目标可以拆成三条定理；公开的 OSS Verify release 则将保证组合为 agrees 与 halts 两类命题。

三定理结构

目标是证明普通二进制不会崩溃。第一条定理先证明 ASan 版对所有小于 64 MiB 的输入都无故障、无 abort、无未建模行为。第二条定理证明 ASan 版与普通版行为等价，比较四类可观察结果：

• •

从 stdin 读入的字节；
* •

写到 stdout 和 stderr 的字节；
* •

退出码或杀死程序的信号；
* •

文件系统的最终状态。

对每个输入和每一对内存布局，两边产生相同的读写序列并以相同状态结束，才算行为等价；这个定义不比较性能。

但执行轨迹（trace）只记录可观察事件，不记录崩溃或死循环本身，因此等价关系可能把不同失败路径判成相同。第三条定理补上这一缺口，单独证明普通版本也不会崩溃。

图2：三定理结构及其安全结论

公开接口的 agrees 与 halts

公开的 OSS Verify release 没有单独发布这三条定理，而是组合成两个命题定义，写在每个 harness 的 Statements.v 里。以 zstd 的 fse\_read\_ncount 入口为例，其 asan_agrees 定义如下（真实文件）。

⁠⁠⁠

Definition asan_agrees :Prop:=  agrees_in Env.alloc_forced_only Budgets.Asan.lim_source Budgets.Asan.lim_target     Images.plain Images.asan.

agrees 要求普通版与 sanitizer 版都不进入错误状态，且输出与退出状态相同。halts 则保证预算内的每次执行都以允许状态（0 或 2）终止，不崩溃、不卡死、不失败断言、不触发 sanitizer，也不离开模型。预算均为前提，halts 为 16 GiB，agrees 的普通版为 2 GiB、sanitizer 版为 512 GiB，超出预算的输入不在命题范围内。

Shapes.v 中的 _is_lps 引理将公开命题定义对应到 LPS 定义，连接了证明接口与执行模型。

Agent 的任务输入

Agent 的具体编排并未公开，不能据此推测 prompt 或重试策略；公开仓库和证明文件能确认任务接口。

每项任务指定上游 commit、入口点、普通版与 sanitizer 二进制，以及以 Admitted. 标记待证定理的 statement 骨架。独立检查器只接受匹配该类型、且不引入许可清单外假设的证明。

Agent 的提交物是一个叫 AgentSubmission 的目录，其中 Proof.v 用真实证明替换掉部分 Admitted.。证明入口文件通常极短，zstd 的 asan\_agrees 证明只有四行。

⁠⁠⁠

From OssFuzzTheorems.zstd.fse_read_ncount Require Statements.From OssFuzzTheorems.Proofs.zstd.fse_read_ncount.lib Require Theorems.Theorem asan_agrees_holds :  OssFuzzTheorems.zstd.fse_read_ncount.Statements.asan_agrees.Proof.  exact OssFuzzTheorems.Proofs.zstd.fse_read_ncount.lib.Theorems.    strong_universal_error_free_fse_read_ncount_asan.Qed.

它只是引用了一个已经构造好的定理。真正的工作在辅助证明库里。

证明的拆解方式

一个入口点的库代码可能只有几百行 C，编译成约两千条 RISC-V 指令，但证明要覆盖整个进程，C 启动代码、C 库的分配器和 printf、ASan 自己的运行时、fuzz 驱动。每个证明今天都要从零重证这些，所以完整证明膨胀到约六十万行。

Agent 把证明拆成可处理的子问题，手段是建立分层抽象。

• •

程序规格抽象。为库的行为写数学规格，证明二进制满足它。zstd 的证明里，lib/Spec/FseHarness.v 先把 fuzz 数据的伪随机抽取函数形式化，再用归纳法证明其行为规格。
* •

辅助引理。把大的性质拆成可复用的小引理，同一文件里有 uint32Range_spec、int32Range_spec 这类引理。
* •

业务行为的规格定理。最终要证的是 roundtrip 性质，压缩表编码后解码能还原，fseB_round_trip 定理陈述了这件事的数学形式。
* •

指令级执行推理。这是和传统验证最不同的部分。证明必须逐条走过编译出的机器指令，使用 zstep、call 这类策略推进程序状态，用真实地址标识函数（如 PC_D_ENTRY : Z := 0x1366c）。

检查失败的迭代

可以把 Agent 与检查器的交互抽象成下面这个循环。它是一个工程抽象，不代表 Anthropic 的实际调度算法。

goal = load_theorem() proof = initial_proof() while not verified:     result = check_with_rocq(proof)     if result.success:         verified = True     else:         proof = revise_proof(goal, proof, result.diagnostics)

检查器返回诊断后，Agent 修改证明并再次提交。真实编排还包括多 Agent 并行、共享工作区和重试；公开资料显示，Agent 常先写一份更短的输出规格，再证明两个版本都满足它。规格中位数约 110 行，程序本身约 86 KB。

工具生成的分工

证明超过一半的内容由机器生成，包括指令编码表和查找表，来自 Claude 编写的工具。脚本处理量大、规则明确的展开工作；模型负责规格抽象、引理选择和证明结构等语义推理。

四、真实证明的完整链路

沿着 zstd 的 fse\_read\_ncount 入口，从 harness 源码逐层走到 Qed.。

图3：zstd fse\_read\_ncount 证明文件链路

第 0 层，harness 源码

fse_read_ncount.c 的 fuzz 目标测试 FSE normalized count 的 roundtrip，用 FSE_writeNCount 编码后由 FSE_readNCount 读回。断言检查写入长度、读取成功与消费字节数，以及 maxSymbolValue、tableLog 和计数值一致；失败通过 FUZZ_ASSERT 调用 abort。

第 1 层，命题（Statements.v）

Statements.v 定义待证命题，包括四个构建各自的 halts、三个 sanitizer 构建各自的 agrees，以及概率界和可判定性命题。命题通过 Shapes.v 与 Images 绑定到具体二进制。

第 2 层，证明入口（Proof.v）

前面已经给出，四行，引用库里的定理。

第 3 层，核心定理（Theorems.v）

Theorems.v 将目标关联到已构造的核心定理，下面是 ASan 版本的证明入口。

⁠⁠⁠

Theorem strong_universal_error_free_fse_read_ncount_asan :... strong_universal_error_free_T_scfg_budgets (mkSpuriousCfg false true true true true true)... lim_source lim_target (mkImage ...images.Plain.M.loaded_segments ...init_pc ...phdrs)(mkImage ...images.Asan.M.loaded_segments ...init_pc ...phdrs).Proof.  exact ...AsanW.AMain_final.base_asan_closed.Qed.

mkImage 包装普通版与 ASan 版映像，lim_source、lim_target 表示预算；定理将两份二进制在预算内无错误且行为一致写成 Rocq 命题。

第 4 层，业务规格（FseHarness.v）

FseHarness.v 里先建模伪随机抽取，再证明最终业务定理 fseB_round_trip。它的陈述（真实）。

⁠⁠⁠

Theorem fseB_round_trip pl n junk rt0 :  all_bytes pl ->0<= n ->let'(tl, msv, nc, data, dsz, bsz, rem):= fseA pl n in  all_bytes junk -> length rt0 =256%nat ->exists rt,    read_ncount rt0 255(data ++ junk)= Ok (rt, msv, tl, dsz)/\\ length rt =256%nat /\\(forall i,0<= i <= msv -> Znth i rt = Znth i nc)/\\(forall i, msv < i <=255-> Znth i rt =0).

该定理表明，给定输入 pl，fseA 算出计数和编码数据后，read_ncount 对任意尾随字节都能成功读取，消费长度为 dsz，解码数组长度为 256；合法范围内的结果与原计数相同，范围外为 0。

第 5 层，执行状态引理（RF\_fse\_h\_D.v）

RF_fse_h_D.v 用后置条件 phaseD_post 描述程序到达出口 PC 时的机器状态，并由 phaseD_proof 证明从入口 PC 0x1366c、寄存器和内存满足前置条件的状态可达该条件。证明以 zstep 逐指令推进，遇到 memcpy 时调用 rmemcpy_specZ，将机器级执行归约为高层规格。

各层的咬合

完整论证由执行引理、业务规格和核心定理组成。机器状态沿指令执行到目标函数，规格保证 roundtrip 正确，最终推出 strong_universal_error_free，再由 Proof.v 对应到 Statements.asan_agrees；oft check 用 wrapper 验证类型匹配。

五、验收、规模与边界

机器验收

Proof Agent 负责生成，Rocq Kernel 检查证明；构建锁定和公理审计将证明绑定到二进制、命题及允许的假设。

小黑把候选证明送入 Rocq 的类型检查槽

oft check 在固定镜像中运行，镜像包含 Rocq 9.2.0 和 LPS，不含证明自动化工具。它校验二进制哈希、从 ELF 重建映像、编译命题与证明，再生成 wrapper 将证明赋给指定 statement 的类型，并审计 Print Assumptions 输出。

wrapper 由 oft check 生成，pull request 不能替换。若提交证明了别的命题，类型检查会失败。

⁠⁠⁠

(* written by oft check; never supplied by a pull request *)Require OssFuzzTheorems.zstd.fse_read_ncount.Statements.Require OssFuzzTheorems.Proofs.zstd.fse_read_ncount.asan_agrees.Proof.Definition certified :  OssFuzzTheorems.zstd.fse_read_ncount.Statements.asan_agrees := OssFuzzTheorems.Proofs.zstd.fse_read_ncount.asan_agrees.Proof.asan_agrees_holds.Set Printing Fully Qualified.PrintAssumptions certified.

公理审计只接受 allowed-axioms.txt 中列出的少数基础公理；Axiom、Parameter 和 Admitted. 均不允许，oft lint 与 Print Assumptions 双重拦截。

CI 对每个 PR 检查改动项，并每周无缓存复检全部 statement 和证明；同时比较不同机型生成的 ELF 快照，重新下载并校验锁定哈希的发布资产。反例也会在运行器镜像中重跑。

信任基底包括 Rocq 内核、允许公理、LPS、快照与读取工具、wrapper 和 statement。Rocq 检查不能证明 LPS 与真实 Linux 完全一致；编译器、构建过程以及二进制与源码的关系也不在证明范围内，statement 只对 SHA-256 指定的字节负责。

规模的技术成因

数亿行证明主要来自三方面。

• •

每个入口都要重证 C 启动、C 库、ASan 运行时和 fuzz 驱动，目前缺少可复用的共享证明。
* •

逐指令推理要展开寄存器、整数转换和分支，证明因此冗长。形式化验证专家将现有证明评价为\"啰嗦\"；MachCSL 等 Agent 验证项目也遇到复杂度问题，扩展到更复杂程序仍依赖更好的模块化抽象。
* •

指令编码表等机械内容由 Claude 编写的工具生成，机器生成部分超过总量一半。

模型假设的取舍

LPS 的 SCOPE.md 列出模型假设。

• •

模型只支持 RV64GC、Sv48 地址空间和静态程序。
* •

栈上限为 8 MiB，源程序预算 16 GiB，目标程序预算 512 GiB。
* •

进程模型是单线程，不模拟调度、共享内存交错、子进程或信号处理器。
* •

文件系统不含目录树、符号链接和权限，只建模 /dev/null、/dev/urandom 等少数接口。

模型还假设没有其他进程改动相关文件或持有锁。

这些假设限定了证明边界。模型不固定 Linux 与 QEMU 的选择，系统调用和 mmap 布局可能在源、目标间不同；无地址提示的 mmap 可选任意空闲页；/dev/urandom 将随机字节视为共同输入，而 getrandom 每次独立选择。因此，对不同 API 的行为等价含义并不相同。

形式化验证不等于无 bug。证明针对静态 riscv64、单线程 musl 程序，不直接覆盖常见的 x86/ARM、glibc 动态链接环境；ASan 检测不到的内存错误、未建模代码和调用方误用也在范围之外。明确例外还包括关闭 leak 检测、没有 MemorySanitizer，以及输入上限 64 MiB。

公开证明只是宣称结果的子集。Anthropic 宣称覆盖 239 个入口、123 个库；公开仓库列出 60 个入口、25 个库，20,164 条 statements 中 138 条已证。公开部分可独立复验，未发布证明据称可能暴露尚未修补的 bug。

工程展望

Theorem 的路线图预测，验证速度约每两月翻倍；若共享库先被证明，依赖它们的大量程序也能复用这些结果。

回到三个技术问题。已有软件被转换成数学问题，靠的是把 fuzz 测试编码成规格、把编译产物锁定成内存映像、用 LPS 给出指令和系统调用的形式语义，再用三定理结构把\"无 bug\"拆成可验证的命题。Claude 完成大规模证明，靠的是规格抽象、辅助引理、指令级执行推理和工具生成的分工，模型管逻辑抽象，脚本管机械展开，两者合起来撑住数亿行。系统以可复现可检查的方式交付，靠的是 SHA-256 锁定、证明绑定 statement 类型、公理白名单和每周全量复验。

结论受 statement 和模型约束。被 SHA-256 锁定的二进制，仅在规定的架构、环境、输入上限和预算内满足相应性质。动态链接的 x86/ARM 环境、模型外系统调用、ASan 检不出的内存问题或调用方误用均不在范围内。用于生产前，工程团队仍需确认模型假设与实际部署相符。

参考

• •

Anthropic：LLMs are making formal software verification feasible at a much larger scale（2026-10-22）
* •

Theorem：OSS Verify 官方文档与三个开源仓库 oss-verify / oss-verify-proofs / rocq-linux-process-semantics（2026-10）
* •

Theorem：Bootstrapping the Verified Software Stack（2026-09-29）
* •

Google：OSS-Fuzz 持续模糊测试项目（2026）
* •

Rocq：Rocq Prover 9.2 官方发布（2026）