第 01 章：引言

Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross

大多数软件都存在大量漏洞，而 AI 现在可以轻松发现 并利用 这些漏洞。抵御网络攻击的常规防御措施已不再足够：我们需要能够证明代码没有漏洞的方法。软件形式化验证可以提供这种保证，但过去往往需要专家耗费数年时间，因此对大多数实际项目来说并不现实。然而，在与 Theorem 的合作中，我们表明情况已经改变：LLM 现在可以大规模生成形式化证明，从而支持包含经证明的安全保证的软件开发新工作流。我们使用 Claude，在 100 多个实际使用的开源软件库中，于汇编代码层面（RISC-V）证明了安全属性。据我们所知，这是首次大规模利用 AI 在汇编代码层面对生产软件进行形式化验证。 在编写证明的过程中，Claude 还发现了一些多年来一直未被检测出的漏洞，尽管这些软件已经过数万亿次测试运行 。随着模型能力持续提升，我们预计形式化验证将成为安全软件开发不可或缺的一部分。

引言

即使是经过大量测试的成熟软件也存在漏洞，而 LLM 越来越擅长 发现这些漏洞。Linux 内核是当今经过最充分测试的软件之一，部署在全球数十亿台设备上，最近却披露了超过 1,000 个漏洞 。随着前沿模型越来越善于将看似无害的漏洞串联起来 形成严重的攻击手段，我们需要能够在这些漏洞被实际利用之前发现并修复它们的技术。

理想情况下，这类技术能够发现并修补_所有漏洞，_然后提供某种证明，表明已没有其他漏洞可供发现。_形式化验证_就是实现这一目标的一种方法。在形式化验证中，开发者将代码转换为数学模型，然后尝试证明它始终遵循一组预先定义的安全规则。如果无法证明这一点，就意味着代码中可能存在违反规则的漏洞，而证明失败的具体情况会暗示漏洞可能是什么。重复这一过程（每次都消除失败的原因）最终将得到证明，表明代码中不存在任何会违反这些规则的漏洞。

然而，形式化验证并不容易。证明的篇幅可能是原始代码的许多倍，编写证明需要付出大量努力，还需要一套冷门且高度专业化的技能。例如，实现 seL4 操作系统内核花费了两人年，而对其进行形式化验证 则花费了 20 人年。因此，形式化验证过去只在真正的任务关键型应用中才具有可行性，例如 Airbus 的航空电子设备代码 。

但 LLM 正在让这一过程容易得多。前沿模型现在可以完全自主地为实际软件生成正确性证明。为了展示这一点，我们让 Claude 证明 123 个开源库中有用的安全属性，包括证明其中一些可执行构件在特定条件下_绝不会_崩溃。具体来说，Claude 证明了在某些假设下（即程序作为单线程静态二进制文件，在使用 Linux 操作系统的 RISC-V1 CPU 上运行，且具有固定的内存预算），对于小于 64 MB 的每一种输入，以及模型涵盖的每一种 Linux 操作系统（OS）响应和内存布局，这些程序都将正常退出，不会触发内存安全错误或断言失败。这距离修复_所有_可能的漏洞仍然很远，但确实让我们比以往更接近这一目标，并为实现该目标提供了一条路线图。

我们正在发布这些证明的一个子集 以及 RISC-V 和操作系统的语义定义 ，以便任何人都能验证和复用它们。我们在这个项目中的合作伙伴 Theorem 也提供为其他开源项目 运行同一流程的服务，并正在发布一项 Claude 技能 ，帮助开发者开始验证自己的代码。

形式化验证是一个广泛的领域，包含多种方法。下文还介绍了我们使用其他形式化验证方法加速其他安全或软件开发任务的初步探索，例如评估 zlib 压缩算法的安全性、证明用 Rust 编写的 Python 解释器在行为上等价，以及根除关键软件中长期存在的漏洞。

形式化验证的前景令人期待。随着模型越来越智能，编写证明的成本正在下降。此外，随着越来越多的代码被形式化，以及实现安全保证的方法日益标准化，在不同代码库之间复用或修改证明的能力将分摊相关成本。我们鼓励所有开发者探索使用 LLM 进行形式化验证，_尤其是_那些之前尝试过能力较弱的模型却发现行不通的开发者。

在本文余下部分，我们将更详细地介绍我们的形式化验证实验。

将测试转化为证明

要证明一段软件是正确的，我们首先必须说明“正确”究竟意味着什么。正确性由_规格说明_（spec）定义。对于某些程序，有一种明确的方式来形式化描述程序的预期行为。例如，PNG 解码器接收一串字节，并（遵循 RFC 2083 ）将这些字节解码为对应的图像。但对于大多数程序，事情并没有这么简单。文本编辑器或网页浏览器的“正确”意味着什么？获得全面且没有歧义的规格说明十分困难，这是大规模验证软件的一大障碍。

为了解决我们希望证明的开源库代码所面临的这一问题，我们采用的方法是：利用一个通用模型来描述在 Linux 上执行任意经 RISC-V 编译的二进制文件意味着什么，并将“这个测试套件始终通过”这一规则编码进去，从而自动把它们已有的、可编译的测试套件转换为规格说明。过去，证明这类规格说明是难以实现的，因为要编写一个证明，涵盖数万条汇编指令在任意输入下所有可能的行为与交互并对其进行论证，本身就极其复杂（由此产生的证明也往往极其庞大）。这正是当今 LLM 能够发挥作用的地方：处理数百万行代码以实现一个定义明确的目标，是 LLM 极其擅长的任务。

在这个项目中，我们从_模糊测试_入手。在这类测试中，开发者在代码中编写一个接收输入的_入口点_2 ，使任何导致崩溃的输入都对应作者关心的漏洞。接着，作为测试引擎的_模糊测试器_会在入口点生成海量半随机和变异的输入，尝试找出漏洞（如图 1 所示）。模糊测试器运行的时间越长，就能发现越多漏洞。但这本质上是一个暴力穷举的过程，无论尝试多少种输入，都无法保证覆盖每一条可能的代码路径。

模糊测试通过让海量生成的输入经过同一个入口点，找出会导致崩溃的输入。 输入有无穷多种，因此搜索永远无法穷尽。

为了找出模糊测试本可发现的所有漏洞，我们将模糊测试转化为一个针对编译后的 RISC-V 指令定义的规格说明。该规格说明指出，对于小于 64 MB 的_任何_输入，模糊测试都不会崩溃。3 如果 Claude 能证明这一规格说明，那么在 RISC-V 上进行该模糊测试就变得多余了：对该入口点进行模糊测试将永远找不到任何漏洞。

我们在 Google 的 OSS-Fuzz 计划中对数百个项目进行了这项工作。该计划为符合条件的开源项目提供持续的模糊测试。OSS-Fuzz 包含数千个由开发者编写的入口点，通过触发崩溃来查找代码属性遭到破坏的情况（例如，断言失败时）。OSS-Fuzz 会自动为 C 和 C++ 程序插入 AddressSanitizer4 （ASan）检测代码，使它们在内存被不当访问时崩溃（这是软件漏洞的主要原因之一 ）。内存安全等广泛适用的规约适用于几乎所有软件。

开源库及其现有模糊测试被编译成 RISC-V 可执行文件。这个可执行文件、Theorem 的 RISC-V 和操作系统形式语义，以及所要求的无崩溃属性，共同通过机械化过程生成证明必须满足的规约。Claude 编写证明；Rocq 内核根据规约检查证明。绿色标记表示已证明的部分，前提是受信任组件正确无误。

在几周时间里，Claude 成功修复了它发现的错误，并证明了 123 个不同的 OSS-Fuzz 库中共有 239 个入口点在任何输入下（最高 64 MB）都不会崩溃。这些证明针对编译后的 RISC-V 指令（即可执行二进制文件），总计约 180 million 行 Rocq 代码；一个典型证明约有 600,000 行，为长度中位数为 18,000 条 RISC-V 指令的二进制文件提供安全保证。这些证明的构建方式是，使用 Theorem 的 RISC-V 指令语义和 Linux 进程语义，将 RISC-V 汇编代码转换为数学模型。这意味着，这些证明目前假设程序以单线程静态二进制文件的形式，在使用 Linux 操作系统的 RISC-V CPU 上运行，且内存预算固定。扩大这些证明的适用范围完全可行，只需为更多汇编架构和其他操作系统的进程制定标准化语义。有关 Claude 编写的证明，请参阅一位专家的看法 。

针对所有输入的形式化无崩溃证明，排除了从入口点可达的任何路径上发生任何崩溃的可能性。在反复完善证明的过程中，Claude 还可以发现并修复任何仍然可达、会导致崩溃的错误。

尽管证明代码的数量十分庞大，但几乎没有一行需要人工审查。Rocq 证明检查器确保该证明正确满足规约。因此，开发者只需要信任以下产物：

  • RISC-V 和 Linux 进程的形式化模型；
  • 已证明的确切定理陈述；
  • Rocq 证明检查器本身。5

这并不意味着这些库没有错误。它意味着，任何仍然存在的错误，要么位于上面列出的产物中，要么超出了 Claude 证明的范围。加固这些仍可能存在错误的受信任组件（Rocq、RISC-V 和 Linux 语义）并非易事，但比起调试大规模证明所覆盖的每一行代码，这项任务要容易处理得多——尤其是因为这种方法可以保护任意数量的项目，而无需增加受信任组件的规模。

我们欢迎对证明进行独立验证，也鼓励大家改进我们的方法。为此，我们将发布为本项目制作的、尚未公开的受信任组件（见上文）；Claude 为无需修补的模糊测试编写的完整 Rocq 证明；以及我们未能证明的其他模糊测试的规约。

发现并修复错误

上文中，我们展示了如何将许多开源库中由开发者编写的测试（模糊测试）转化为规约，再由 Claude 证明这些测试始终能够通过，有时需要先修补它发现的剩余错误。正因如此，尝试证明这些规约的过程发现了数百个错误。

Claude 在尝试证明数百个入口点的过程中发现了大量错误。为了确保 Claude 不必每次遇到错误时都停下来等待人工处理，我们让 Claude 自行修复发现的错误：它修补代码后，系统会根据修补后的代码重新生成规约，然后 Claude 继续证明这个新规约。6

我们发现的许多错误，模糊测试工具恐怕永远也找不到。模糊测试工具会对小规模输入进行变异，通常上限为 1 MB ，并且通常依靠代码覆盖率来引导它们寻找错误。在证明某个库的入口点时，Claude 在该库自带的一份解压器代码中发现了一个计数器下溢错误，该错误会导致越界写入，但只有在输入约为 20 MB 且具有一种罕见的特定布局时才会发生。其他错误包括：图像解码器中的一次越界读取，需要 64 MB 的输入和超过 2 GB 的内存才能触发；另一个库中的一次越界读取，需要通过同一文件的两个句柄进行特定顺序的调用才能触发；以及在 libexpat 中重新发现了 CVE-2026-56132，该漏洞需要深度嵌套的输入才能触发。Claude 还发现了一些完全不会导致崩溃的逻辑错误。例如，在证明某个库的内存安全性时，它注意到一个用于限制应用程序可加载哪些文件的功能并不总是生效。

这个项目的最终目标是证明，编译为 RISC-V 的模糊测试中已不存在尚待发现的崩溃。然而，上述错误表明，无论是否实现这一目标，这个过程还有另一个好处：即使只是尝试进行这一过程，也能发现需要修复的真实错误。

证明内存安全以外的属性

证明一个模糊测试中已没有更多待发现的崩溃，其意义比听起来更重大。现实代码中的模糊测试通常会检查有意义的高层属性是否遭到破坏，例如编码解码往返一致性、幂等性、代数定律、差分测试、自洽性或与参考实现的等价性。例如，LZO 压缩算法的一个模糊测试会断言，如果先压缩输入再解压，结果应与原始输入相同。如果该属性不成立，程序就会崩溃——因此，证明测试永远不会崩溃，就等同于证明该属性本身。

即使开发者没有直接指定这些属性，也可能出现这种情况。例如，为了完成对 cpp-httplib 的 OSS-Fuzz 证明，Claude 必须排除 std::set 析构函数中递归过深导致栈溢出的可能性。这个递归深度受树的最大深度限制，因此 Claude 必须证明（而且是在机器代码层面！）libc++ 的红黑树再平衡算法经过了正确优化，能够将树的深度限制在对数级别。

其他形式化验证案例研究

形式化验证是一个广阔的领域。上面从模糊测试到证明的例子，展示了大语言模型如何通过将证明直接应用于机器代码，让形式化验证得到更广泛的应用。

我们还通过其他方式将大语言模型与形式化验证结合，并取得了成功。例如，我们让 Claude 为定义 zlib 压缩文件格式的技术文档 RFC 1950 编写一份形式化规约。然后，我们让 Claude 证明 Linux 内核中的 zlib 实现正确地实现了该规约。与上面的例子一样，Claude 在二进制层面证明了这一属性；区别在于，这次 Claude 使用由它生成（并经过充分测试）的 x86 指令集架构形式语义，直接证明了编译为 x86 的二进制文件，而不是 RISC-V 二进制文件。7 随后，我们对另外六个广泛使用的库重复了这一过程。在此期间，我们在边界情况下发现了一些轻微的（不可利用的）错误，目前正在向上游报告。我们从这项工作中得出两个结论：(1) 这些经过极充分测试的代码库已经几乎完全正确；(2) 可以证明真实现有代码库的端到端正确性属性。

在另一项实验中，我们让 Claude 用 Rust 为 Python 的一个大型子集开发解释器，并证明它遵循一篇学术论文中描述的 CPython 语义，证明过程使用了 Rust 验证工具 Verus。随后，我们通过运行超过 1.7 百万个随机生成的 Python 程序，实际检验了该解释器与 CPython 行为的一致性。在 99.95% 的测试中，两者行为完全一致；其余测试中的差异都是已知的边界情况，并不令人意外。

我们还尝试对简单的安全属性进行形式化验证，从而发现了几个广泛使用的关键应用程序中的问题。其中，我们发现了一个此前未知的逻辑缺陷，它已经潜伏了十多年。在验证一款广泛使用的 PDF 阅读器时，我们在一周内发现的安全缺陷数量，相当于通常一年内收到的报告数量。

有关其中部分工作的更多细节，请参阅附录 。

这只是开始

LLM 辅助形式化验证的一个主要局限是，生成证明可能需要消耗数亿个 token。如果我们的目标是让整个软件生态系统都能使用这些方法，成本效率就至关重要。幸运的是，我们有充分的理由期待效率会有所提升。

更新的模型需要更少的 token

我们从真实的 OSS-Fuzz 代码中 构建了 36 个小型验证任务。Opus 5.5 完成其中一半任务的证明，所需 token 比 Opus 5 少约 40%。随着模型接受长时间验证任务的训练，我们预计这一趋势会持续下去。

Opus 5.5 完成证明的速度快于早期模型。 在给定 token 预算下，由单个智能体完成证明的 36 个形式化验证任务所占比例。每个任务都由单个智能体进行三次独立尝试，每次预算为 5M 个 token；首次尝试完成证明时，该任务即计为已证明。

证明可以复用

当智能体各自工作时，它们往往会重复做大量工作。证明和软件一样，都是由更小的证明递归构建而成的，而且证明越小，通常就越容易复用。为了衡量这一点的影响，我们让智能体在证明各自目标的过程中，可以相互复制证明。有了这个共享工作区，智能体所需的 token 比独立工作时减少了 17%，有些智能体甚至在此前独立尝试失败后成功完成了证明。

一个共享工作区中的 36 个证明，按完成顺序排列。 弧线连接共享同一个未修改文件的任意两个证明；条形表示编写每个证明所消耗的 token，黑线表示智能体独立完成同一任务的平均成本。在已完成的 34 个证明中，有 30 个任务的独立工作平均成本更高（独立工作的智能体未能完成其中两个证明）。

在 OSS-Fuzz 证明工作中，我们也观察到了同样的现象，而且规模更大。证明的大部分内容涉及每个程序都包含的代码（尤其是 C 运行时和 AddressSanitizer 的初始化），因此差异很大的程序最终可能有大量重叠的证明。智能体团队利用了这一点：复制另一个团队已经完成的证明，然后将其调整为适用于自己的程序（图 6）。

智能体复制已有证明，并将其调整为适用于每个新程序。 每列按字节占比展示一个程序的完整证明。色块代表证明的各个部分，每个色块显示有多少内容保持完全一致、经过轻微编辑（同一文件，大小变化不超过 2%）、经过更多编辑或为新编写。共享部分几乎没有新增代码。

证明的这种可复用性，使得 Lean 中的共享形式化数学库 Mathlib 发展到拥有近 300,000 条定理 ，由超过 700 名贡献者提交：每个新证明都建立在已有成果之上。在 OSS-Fuzz 工作过程中，我们也积累了类似的证明成果，并在本次发布中包含了其中一部分（我们不会发布可能暴露开源软件中尚未修复的缺陷的证明）。

从这些初步实验迈向更大规模的应用时，我们需要一套策略来验证数量庞大的_现有_软件，首先从最关键的依赖项着手。正如我们所展示的，通过使用通用规格并在二进制层面开展工作，可以大规模实现这一目标，无需用另一种语言重写整个代码库。

这种方法也有助于以软件包为单位复用证明，这意味着每个依赖项只需验证一次。依赖关系遵循幂律：即使只证明一小组共享库，也能让大量软件的证明变得可行。更多细节请参阅 Theorem 的路线图 ，其中介绍了验证整个 Nix 生态系统的计划，包括 glibc、OpenSSL 和 cURL 等关键基础设施。

局限性

在实践中，形式化验证有时能够证明的代码安全性，可能不如我们希望的那么全面。

“经过形式化验证”不等于“没有缺陷”。 Claude 可以编写证明，表明编译后程序的行为符合形式化规格的要求（该证明由外部证明检查器验证）。但是，证明检查器无法告诉你规格是否符合现实。要符合现实，规格就必须正确涵盖和建模被验证程序所运行的真实机器的各个方面，包括 CPU 和操作系统。当经过验证的代码中出现缺陷时，原因在于规格或对机器语义的假设与现实存在差异。好在这也意味着我们知道应该_去哪里_寻找剩余缺陷，以及如何设计系统，尽量缩小那些仍可能存在缺陷的空白。下面介绍这些情况如何影响我们的证明，以及未来可以如何弥补这些空白。

真实机器的某些行为没有被模型描述。 我们的证明针对的是与 musl libc 链接的单线程静态 RISC-V 二进制程序。然而，大多数人在 x86 或 ARM 上运行这些库，并将它们与 glibc 动态链接。为了弥补这一差距，我们需要更接近实际部署系统的系统模型。例如，朝这个方向迈出的一步是为 x86 生成准确的语义。

所证明的论断可能没有涵盖我们关心的一切。 我们证明了 Google OSS-Fuzz 中许多模糊测试入口点对于任何小于 64 MB 的输入都不会触发崩溃，包括 ASan 检测到的崩溃。不过，ASan 无法检测所有内存安全缺陷，而且我们没有验证每个库的所有入口点。即使验证了所有入口点，也无法覆盖整个库（尤其是存在死代码时）。此外，真实程序可能会错误使用库，导致_调用方_发生内存损坏。为了弥补这一差距，我们需要为每个公共函数规定调用方必须遵守的要求，调用方也必须严格遵守这些要求。

我们预计，随着我们对如何利用 LLM 进行形式化方法的了解不断加深，以及模型持续改进，这些局限将变得可以解决，我们也将能够验证所依赖代码中大得多的比例。

结论

发展趋势很明确：形式化验证在过去只有在安全性要求最高的代码中，由专家针对特定需求精心构建保障时才切实可行；而不久之后，对于几乎所有生产软件，它都将变得像今天的模糊测试一样实用。就像静态类型、测试框架和其他正确性工具一样，验证将从“后加上去”逐渐成熟为“内置功能”，推动这一变化的不仅有 LLM，还有语言设计和开发工作流方面的创新。

在当今世界，LLM 正在自动扫描并发现越来越多的代码漏洞，因此我们必须采用能够_保证_代码安全属性的流程。由 LLM 扩展规模的形式化验证是一种很有前景的方法，有望在过去无法企及的范围和规模上获得这些保证。我们鼓励其他人开展实验，让我们共同建设这样一个世界：稳健的软件得到广泛普及，软件缺陷则成为人们充分了解、能够迅速解决的罕见现象。

阅读完整附录。

脚注

01RISC-V 是一种处理器设计，与 x86 或 ARM 类似，它定义了软件编译后所使用的汇编指令（芯片执行的基本命令）。

02入口点是代码的一个入口，由代码作者提供用于测试。任何导致入口点崩溃的输入都表明存在作者关心的缺陷。

03要增加这个数值，只需要人稍费一点力气，修改参数并重新生成规格说明，然后让 Claude 重新证明该命题。

04AddressSanitizer 是一种编译器工具，它会在程序中加入检查，使缓冲区溢出、释放后使用等内存错误在运行时一发生就被检测并报告。

05严格来说，这也意味着我们必须信任 Rocq 证明检查器所依赖的硬件、操作系统和 OCaml 编译器。

06请注意，这仍然留下了奖励黑客行为的空间。奖励黑客行为是指 AI 模型找到一条捷径，虽然在形式上达到了给定的目标，却没有完成真正的意图，就像学生靠背答案而不是学习知识来通过考试。在这里，Claude 可以把程序重写成一个显然永远不会崩溃的程序，从而让任何定理都能得到证明。为了防止这种情况，我们对任何补丁都予以扣分；如果能证明补丁改变了哪些输入的行为，以及受影响的输入有多少、是否足够少，我们则给予额外加分。我们还记录并审查了补丁，检查是否存在这些问题。

07我们认为，Claude 能够完全自主地生成一套 ISA 的形式语义，本身也是另一个有趣的发现。虽然我们无法确定这套语义本身是完美的，但实际测试表明，逐步执行这套语义可以在 Linux 内核之上启动 Ubuntu 用户空间。生成这套语义的过程还发现了官方参考文档中的数百处错误，以及硬件本身数量较少的一些缺陷。