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

大多数软件都布满漏洞，而 AI 现在可以轻易找到并利用这些漏洞。针对网络攻击的标准防御措施已不再足够：我们需要能够证明代码没有漏洞的方法。形式化软件验证可以提供这种保证，但历史上它需要专家投入数年努力，因此对大多数现实项目而言并不切实际。然而，在与 Theorem 的合作中，我们表明情况已不再如此：LLM 现在可以大规模生成形式化证明，从而支持包含经过证明的安全保证的新软件开发工作流。使用 Claude，我们在 100 多个现实世界开源软件库中，在汇编代码层面（RISC-V）证明了安全属性。据我们所知，这是首次大规模尝试使用 AI 在汇编代码层面将形式化验证应用于生产软件。在编写证明的过程中，Claude 还发现了多年来尽管经过数万亿次测试运行仍未被检测到的漏洞。随着模型能力持续提升，我们预计形式化验证将成为安全软件开发的重要组成部分。

引言

即使是成熟且经过大量测试的软件也包含漏洞，而 LLM 越来越擅长发现它们。Linux 内核——当今经过最充分测试的软件之一，部署在全球数十亿台设备上——最近披露了 1000 多个漏洞。随着前沿模型越来越有能力将看似无害的漏洞串联成严重利用，我们需要能够在这些漏洞被野外利用之前检测并修复它们的技术。

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

然而，形式化验证并不容易。证明可能比原始代码大许多倍，编写证明需要大量努力以及小众且高度专业化的技能组合。例如，实现 seL4 操作系统内核用了两个人年，但对其进行形式化验证用了 20 个人年。因此，形式化验证仅在真正关键任务应用中才具有实用性，例如空客的航空电子代码。

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

我们正在发布这些证明的一个子集，以便任何人都可以验证和重用它们，同时发布 RISC-V 和 OS 语义。我们在该项目中的合作方 Theorem 也提出为其他开源项目运行相同的流水线，并正在发布一个 Claude 技能，以帮助开发者开始验证自己的代码。

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

形式化验证的前景十分广阔。随着模型变得越来越智能，编写证明的成本正在下降。此外，随着更多代码被形式化，以及实现安全保障的方法变得更加标准化，跨代码库复用或修改证明的能力将分摊成本。我们鼓励所有开发者探索使用 LLM 进行形式化验证——尤其是那些此前用能力较弱的模型尝试过并发现行不通的人。

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

将测试转化为证明

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

为了处理我们试图证明的开源库中的代码，我们采取的方法是：自动将其已有的可编译测试套件转换为一个规范，具体做法是编码“该测试套件始终通过”这一规则，并使用一个通用模型来描述在 Linux 上执行任何由 RISC-V 编译的二进制文件意味着什么。从历史上看，证明此类规范曾极其困难，因为编写一个能够涵盖并论证数万条汇编指令在任意输入下的所有可能行为与交互的证明本身就极其复杂（而且由此产生的证明往往极其庞大）。这正是当今 LLM 的用武之地：在追求一个明确定义的目标时处理数百万行代码，是 LLM 极其擅长的一项任务。

对于这个项目，我们从模糊测试开始。在这些测试中，开发者在其代码中编写一个入口点2，用于接收输入，这样任何导致崩溃的输入都是作者关心的 bug。然后，模糊测试器（一个测试引擎）在该入口点生成大量半随机和变异输入，以试图找到 bug（如图 1 所示）。模糊测试器运行时间越长，它能找到的 bug 就越多。但这本质上是一个暴力过程，无论你尝试多少输入，都不能保证覆盖所有可能的代码路径。

模糊测试的工作原理是通过一个入口点运行大量生成的输入，以找出会导致崩溃的输入。输入是无限的，因此搜索永远无法完成。

为了找出模糊测试原本会暴露的所有 bug，我们把该模糊测试转换成了一个定义在编译后的 RISC-V 指令之上的规范。该规范表示，对于任何小于 64 MB 的输入，模糊测试都不会崩溃。3 如果 Claude 能证明这个规范，那么对 RISC-V 的模糊测试就变得多余了：对该入口点进行模糊测试将永远找不到任何 bug。

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

开源库及其现有的模糊测试被编译为 RISC-V 可执行文件。该可执行文件，连同 Theorem 的 RISC-V 和操作系统形式语义以及期望的无崩溃性质，机械地产生一个证明必须满足的规范。Claude 编写证明；Rocq 内核根据该规范对其进行检查。绿色标记已证明的内容，前提是受信任组件是正确的。

在几周的时间里，Claude 成功修补了它发现的缺陷，然后证明了在 123 个不同的 OSS-Fuzz 库中的 239 个入口点上，对于任何输入（最大 64 MB）都不存在崩溃。这些证明作用于编译后的 RISC-V 指令（即可执行二进制文件），由约 1.8 亿行 Rocq 组成，一个典型证明约 60 万行，为长度中位数为 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 压缩算法的模糊测试断言：如果你压缩一个输入，然后解压它，结果应与原始输入相同。如果该属性不成立，程序就会崩溃——因此证明测试永不崩溃等价于证明该属性本身。

即使属性并非由开发者直接指定，这种情况也可能发生。例如，为了让 Claude 完成针对 cpp-httplib 的 OSS-Fuzz 证明，有必要排除因 std::set 析构函数中递归过多而导致栈溢出的可能性。该递归深度受树的最大深度限制，因此 Claude 必须（在机器码上！）证明 libc++ 的红黑树再平衡算法被正确优化，使树的深度保持对数有界。

其他形式化验证案例研究

形式化验证是一个广阔的领域。上面的“从模糊测试到证明”示例是 LLM 通过直接将证明应用于机器码，使形式化验证更广泛可用的一个实例。

我们还看到了在其他方式上使用 LLM 进行形式化验证的成功案例。例如，我们让 Claude 编写 RFC 1950 的形式化规范，该技术文档定义了 zlib 压缩文件格式。然后，我们让 Claude 证明 Linux 内核中的 zlib 实现正确实现了该规范。与上述示例一样，Claude 在二进制层面证明了该属性，只不过这次不是 RISC-V，而是使用 Claude 生成（并经过大量测试）的 x86 ISA 形式化语义，直接证明了 x86 编译的二进制文件。⁷ 随后，我们对另外六个广泛使用的库重复了这一过程。在此过程中，我们在极端情况中发现了一些轻微（不可利用）的 bug，目前正在向上游提交。我们从这次实践中得出两个结论：（1）这些经过极其充分测试的代码库已经几乎完全正确；（2）可以对真实现有代码库证明端到端正确性属性。

在另一项实验中，我们让 Claude 用 Rust 开发一个支持 Python 大部分子集的解释器，并证明（使用 Verus，一个 Rust 验证工具）它符合一篇学术论文中概述的 CPython 语义。然后，我们通过运行超过 170 万个随机生成的 Python 程序，实证衡量其对 CPython 行为的符合程度，发现 99.95% 的测试与 CPython 行为完全一致，其余测试差异属于意料之中的已知极端情况。

我们还通过对简单安全属性进行形式化验证尝试，在几个广泛使用且关键的应用中发现了问题。其中一个应用里，我们发现了一个潜伏十多年、此前未知的逻辑 bug。在验证一个广泛使用的 PDF 阅读器的过程中，我们一周内发现的安全 bug 数量与通常一年报告的数量相当。

有关其中一些工作的更多细节，请参见附录。

这只是开始

LLM 辅助形式化验证的关键限制之一是，证明可能需要消耗数亿个 token 才能产出。如果我们的目标是让这些方法惠及整个软件生态系统，成本效率至关重要。幸运的是，有充分理由预期效率会提高。

更新的模型需要更少的 token

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

Opus 5.5 比早期模型更快完成证明。图为在给定 token 预算下，由单个智能体证明的 36 个形式化验证任务的占比。每个任务在 500 万 token 预算下获得三次独立的单智能体尝试，当第一次尝试完成时即计为已证明。

证明可以复用

当智能体独立工作时，它们往往会重复大量工作。证明就像软件一样，是由更小的证明递归构建而成——而证明越小，往往越容易复用。为了衡量这一点的影响，我们让智能体在证明各自目标时复制彼此的证明。在获得这个共享工作区后，智能体所需的 token 比单独工作时少 17%，一些智能体甚至在之前单独尝试失败后取得了成功。

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

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

智能体复制现有证明，并将其改编用于每个新程序。每一列按字节占比表示一个程序的完整证明。区块是证明的组成部分，每个区块显示其中有多少保持完全相同、轻微编辑（同一文件，大小差异在 2% 以内）、编辑更多或新写入。共享部分几乎没有增加新代码。

证明的这种可复用性，正是 Mathlib 这个 Lean 形式数学共享库成长为拥有近 300,000 个由 700 多名贡献者提交的定理的方式：每个新证明都建立在现有成果之上。我们在 OSS-Fuzz 工作中也积累了一个类似的证明库，其中一些将包含在我们的发布中（我们不会发布可能暴露开源软件中未修补漏洞的证明）。

随着我们从这些初步实验中走出来，我们需要一种策略来验证庞大的现有软件体系，从最关键依赖开始。正如我们所展示的，这可以通过使用通用规范和二进制层面工作大规模实现，从而避免需要用另一种语言重写整个代码库。

这种方法还促进了包级别粒度的证明复用，这意味着每个依赖只需要验证一次。依赖遵循幂律：即使只证明一小部分共享库，也能让大量软件变得可证明。更多细节，请参见 Theorem 关于验证整个 Nix 生态系统的路线图，其中包括 glibc、OpenSSL 和 cURL 等关键基础设施。

局限性

在实践中，形式化验证有时能证明的代码安全性可能比我们希望的要少。

“形式化验证”并不意味着“没有缺陷”。Claude 可以编写一个证明，表明编译后程序的行为满足形式化规范的要求（该证明由外部证明检查器验证）。然而，证明检查器无法告诉你你的规范是否与现实相符。为了与现实相符，规范必须正确涵盖并建模已验证程序所运行的真实世界机器的一切，包括 CPU 和操作系统。当已验证代码中出现缺陷时，是因为规范或假设的机器语义与现实不同。幸运的是，这也意味着我们知道去哪里寻找剩余缺陷，以及如何设计一个系统来最小化这些仍然可能有缺陷的缺口。下面说明这如何适用于我们的证明，以及未来工作如何弥合这些差距。