A. 证明对象与三条要求
主研究的对象是单线程、静态链接的 RISC-V/Linux 二进制文件。静态链接是把程序依赖的库代码一起编入同一个可执行文件；这里使用 musl，而不是许多日常部署采用的 glibc。公开仓记录的构建工具是 clang 20.1.8，证明检查使用 Rocq 9.2.0。证明针对这些具体文件，不会自动覆盖其他编译结果。
每个入口有不带检测工具的普通版，以及加入 ASan 的版本。附录列出了需要证明的三条要求：ASan 版不崩溃，普通版与 ASan 版行为等价，普通版自身也不崩溃。这些要求针对小于 64 MiB 的输入，并覆盖所有内存布局；博客正文将输入上限写作 64 MB，本文正文沿用博客写法。
这里的“行为等价”只比较规定的外部可观察结果，不要求程序执行的每一步都一样。附录列出的观测项是：
- 从标准输入读取的字节。
- 写入标准输出和标准错误的字节。
- 程序的退出码，或结束它的信号。
- 文件系统的最终状态。
比较还要求读写事件的顺序相同。这个定义不包含性能。一次崩溃可能让读写记录停住，无声的无限循环也可能如此，因此行为等价本身不足以排除普通版崩溃，必须另证普通版不崩溃。
公开仓还包含部分入口的 UndefinedBehaviorSanitizer（UBSan）证明，它用于检测某些未定义行为，不能把这些结果扩大到主研究全部入口。普通版的内存预算，在 ASan 相关陈述中为 2 GiB，在 UBSan 陈述中为 16 GiB。普通版超出预算的输入不在保证内。
这些要求在 LPS 中表达。LPS 是 Linux 进程运行 RISC-V 文件的数学模型，README 明说它不完整，也包含未自行检查的假设。模型与实际 Linux 不同的地方，可能使证明不适用。博客列出的信任前提之外，还需信任检查程序所依赖的硬件、操作系统和 OCaml 编译器。
项目早期，模型为证明两个版本输出一致，通常先归纳一个更短的中间规格，再证明两个版本都满足它。这些中间规格的中位长度约 110 行，程序代码大小的中位数是 86 KB，证明覆盖了其中由测试入口执行到的约 20–50%。这是证明过程中组织推理的方式，不是允许模型自由改变研究最终目标。
B. 其他 bug 与验证实验
除正文中的解压器案例外，还有一个库在通过同一文件的两个句柄、按特定顺序调用时，会读取不该读取的内存。文件句柄是程序用来访问已打开文件的标识。Claude 还发现了一个图像解码器的越界读取，需要 64 MB 输入并消耗超过 2 GB 内存才会触发；它重新发现了 libexpat 中的 CVE-2026-56132，触发条件是深度嵌套的输入。另一个库限制应用能够加载哪些文件的功能并非总被执行，这是不会引发崩溃的逻辑 bug。发现它不等于“不崩溃”要求已经证明这项访问限制正确。
正文第 4 节的 LZO 例子还有两处细节。一是测试代码只断言两步成功、字节数相同，没有直接用断言逐字比较内容；“压缩器与解压器正确往返”是附录作者对证明所需推理的说明，不能据此写成“代码直接检查了内容完全一致”。二是在二进制里，每条断言都是一个跳到中止处理的分支，证明在这些分支的确切地址上逐个推演，表明它们永远不会被走到。
p11-kit 管理对智能卡和加密硬件的访问。它的配置解析代码在识别 PEM 数据块时，通过断言检查数据块不会超出输入缓冲区的范围，证明也覆盖了这项检查。cpp-httplib 的案例则需要排除递归过深撑爆调用栈：Claude 为此证明 libc++ 的红黑树重新平衡算法能够保持对数级深度。红黑树是一种树状数据结构，这里对树深度的约束用于排除相关递归过深造成的栈溢出。
另一项实验不是从“不崩溃”出发。团队让 Claude 为定义 zlib 压缩文件格式的 RFC 1950 写出要求，再证明 Linux 内核中的 zlib 实现符合它。对象是 x86 二进制文件，所用的指令执行语义由 Claude 生成并经过大量测试。团队把过程扩展到约六个其他常用库，发现了一些不可利用的小 bug，正在向上游报告。原文从中得出两点：这些测试极其充分的代码库本来就已经几乎完全正确；对真实存在的代码库证明端到端的正确性是做得到的。
关于这套 x86 语义，原文称，逐步按其执行规则运行能够启动 Linux 内核上的 Ubuntu 用户空间；生成语义时还发现了官方参考文档中的数百处错误，以及较少量的硬件 bug。作者同时说明，经验测试不能保证语义本身完美。
Python 实验让 Claude 用 Rust 编写一个支持 Python 较大子集的解释器，并用适合 Rust 的验证工具 Verus 检查。它实现了 17 层，证明的要求是：只要解释器返回结果，结果就符合选定的数学语义。这并不保证程序终止，也不等于已经证明与 CPython 完全等价。
团队另外运行超过 170 万个随机程序，其中 99.95% 的行为与 CPython 一致，其余差异是已知边界情况。这个一致性结果来自测试。为了比较测试和证明，团队在早期版本注入 7 个 bug，其中 5 个躲过随机测试，7 个全让证明失败。
原文还报告，在一个未点名的关键应用中发现了存在十多年的逻辑 bug；验证一个未点名的常用 PDF 阅读器时，一周发现的安全 bug 数量，相当于通常一年报告的数量。
C. 证明规模与缩小版实验
完整程序的证明要覆盖公共运行部分，因此证明规模与库自身大小并不成简单的比例关系。典型入口背后的库代码编译后约有 2,000 条指令，完整二进制的指令数中位数则约为 18,000 条，两者不是同一个统计口径。附录用 cJSON 和 fftw3 展示了这种差别。
真实 OSS-Fuzz 工作中也观察到团队复制已有证明，再适配不同程序；原文没有给出这些真实任务对应的整体节省幅度。
D. 公开统计与外部意见补充
公开仓 v2026.10.0 的统计包含不同层级。它为 1,381 个 OSS-Fuzz 项目建立目录，其中 427 个能构建；5,290 个测试中，2,148 个有陈述。一个入口可以产生不同编译版本和不同种类的陈述，陈述数不等于入口数，也不等于库数。
该版本共有 20,164 条陈述：138 已证，229 形式模型未覆盖而卡住，19,797 未解决，0 已知为假。138 统计的是已证陈述，对应有证明的 60 个入口、25 个库。229 条受阻的原因是 LPS 尚未描述需要的系统功能，不是这里已经测得 AI 证明能力不足；0 已知为假也不是其余要求都已获证明。
Anthropic 公布了 RISC-V 与操作系统的形式化语义、项目新建而此前未公开的可信组件、不需要补丁的完整证明，以及其他未能完成证明的测试要求。Theorem 是 2025 年 Y Combinator 春季批次孵化的公司，自称 AI 与程序语言研究实验室，两位联合创始人都在原文作者名单里。原文链接了它的一份路线图，计划按依赖关系逐步验证整个 Nix 软件生态，其中包括 glibc、OpenSSL、cURL 这些关键基础设施。原文的思路是：在二进制层面用通用的要求工作，不必用另一种语言重写整个代码库；证明可以按软件包复用，每个依赖只需验证一次；依赖关系服从幂律，证明一小批共享库，就能让一大片软件变得可以证明。
Wallach 把这项工作和 Kaashoek、Zeldovich 此前用 agent 验证 xv6 操作系统的技术报告作了对比（Zeldovich 两边都署名）：那次是先精心设计一套逻辑（MachCSL），再借大模型用它做验证；这次的自动化程度高得多，agent 自己想出了逻辑，一群 agent 自发地共享思路和技巧，帮助证明推进。他还指出，这些库本来就在 OSS-Fuzz 里，测试入口早已定义好，而任何基于性质的测试都可以改写成定理交给证明检查器。
Wallach 提到的工具包括 Rust 生态中的 Verus、Aeneas，以及支持相关验证方式的 C 工具 Frama-C。他建议把函数调用前需要满足的条件、调用后应保证的结果写回源代码，用这些工具支持后续开发。
他仍希望保留一直到机器码的证明，并近似转述了形式化验证研究者的看法：如果编译器本身已经被证明正确，从中提取关于其输出正确性的证明就更直接；编译器未经证明时，这件事更难。他把对 gcc 或 clang 投入模型算力列为建议，而不是已经完成的研究结果。
