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 内核——当今测试最充分的软件之一，部署在全球数十亿台设备上——最近被披露了超过 1000 个漏洞。随着前沿模型越来越有能力将看似无害的缺陷串联成严重漏洞利用，我们需要能够在这些缺陷于真实环境中被利用之前检测并修复它们的技术。
理想情况下，这类技术能够发现并修补所有缺陷，然后提供某种证明，表明再也找不到更多缺陷。形式化验证是做到这一点的一种方式。在形式化验证中，开发者将代码翻译成数学模型，然后尝试证明它始终遵循某组已定义的安全规则。如果无法证明这一点，就意味着代码中可能存在违反某条规则的 bug，而失败的性质暗示了 bug 可能是什么。重复这一过程（每次消除失败原因后）最终将得出证明，表明代码不存在任何会违反这些规则的 bug。
然而，形式化验证并不容易。证明的规模可能比原始代码大许多倍，编写证明需要大量精力以及小众且高度专业化的技能。例如，实现 seL4 操作系统内核花费了两人年，但20人年才完成形式化验证。因此，形式化验证此前只在真正关键任务的应用中才具有实用性，例如Airbus 的航空电子代码。
但 LLM 正在让它变得容易得多。前沿模型现在能够完全自主地为真实世界的软件生成正确性证明。为了演示这一点，我们让 Claude 为 123 个开源库证明有用的安全属性，包括证明其中一些可执行产物在某些条件下永远不会崩溃。具体而言，Claude 证明了这些程序对于所有小于 64 MB 的输入以及所有建模的 Linux 操作系统（OS）响应和内存布局，在某些假设下（即程序作为单线程静态二进制运行，在 RISC-V1CPU 上使用 Linux OS，并具有固定内存预算），将始终正常退出，不会触发内存安全错误或断言失败。这距离修复所有可能的 bug 仍然很远，但它确实让我们比以往更接近，并提供了通往该目标的路线图。
我们正在发布这些证明的一个子集，以便任何人都能验证和复用它们，同时发布RISC-V 和 OS 语义。Theorem，我们在该项目上的合作者，也提出为其他开源项目运行相同的流水线，并正在发布一个Claude skill，以帮助开发者开始验证自己的代码。
形式化验证是一个涵盖众多方法的广泛领域。下面，我们还将描述使用其他形式化验证方法来加速其他安全或软件开发任务的初步探索，例如评估 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 会自动为 C 和 C++ 程序插桩 AddressSanitizer4（ASan），使其在内存被不当访问时崩溃（这是软件漏洞的主要成因）。像内存安全这样的广谱规范几乎适用于所有软件。
该开源库及其现有的模糊测试被编译为 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
这并不意味着这些库不包含 bug。相反，这意味着任何剩余的 bug 要么存在于上述列出的产物中，要么超出了 Claude 证明的范围。加固这些仍可能存在 bug 的可信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但这比调试规模化证明所覆盖的每一行代码要容易处理得多——尤其是因为这种方法可以在不增加可信组件规模的情况下保障任意数量的项目。
我们欢迎对我们的证明进行独立验证，并鼓励改进我们的方法。为此，我们公开发布了为本项目构建的、尚未公开的可信组件（见上文）；Claude 为无需修补的模糊测试提供的完整 Rocq 证明；以及我们未能证明的其他模糊测试的规范。
发现并修复 bug
上文我们展示了，你可以将许多开源库中开发者编写的测试（模糊测试）转化为规范，Claude 可以证明这些规范将始终通过，有时是在修补了它发现的剩余 bug 之后。因此，尝试证明这些规范的过程发现了数百个 bug。
在 Claude 尝试证明数百个入口点的过程中，大量 bug 浮现出来。为确保 Claude 不必每次遇到这种情况都停下来等待人工介入，我们让 Claude 修复它发现的 bug：它修补代码，这导致规范随修补后的代码重新生成，然后 Claude 继续证明新的规范。6
我们发现的许多 bug 是模糊测试器不太可能找到的。模糊测试器会变异小输入，通常上限为 1 MB，并且通常依赖代码覆盖率来引导它们找到 bug。在证明某个库中的一个入口点时，Claude 在其解压器副本中发现了一个计数器下溢，该下溢会导致越界写入，但仅在输入约为 20 MB 且具有一种罕见、特定布局时才会触发。其他 bug 包括：一个图像解码器中的越界读取，需要 64 MB 输入和超过 2 GB 内存；另一个库中的越界读取，需要对同一文件的两个句柄执行特定的调用序列；以及在 libexpat 中重新发现 CVE-2026-56132，该漏洞需要深度嵌套的输入。Claude 还发现了根本不会导致崩溃的逻辑 bug。例如，在证明某个库是内存安全的过程中，它注意到一个用于限制应用程序可加载哪些文件的功能并不总是被强制执行。
这个项目的最终目标是获得一个证明，即经 RISC-V 编译的模糊测试已没有剩余的崩溃可被发现。然而，上述这类 bug 表明，无论该目标是否达成，这个过程还有另一个好处：即使只是尝试这个过程，也会产生需要修复的真实 bug。
证明超越内存安全的内容
证明一个模糊测试已没有更多崩溃可被发现，其意义比听起来更重大。在现实世界的代码中，模糊测试常常用于检测有意义的高层属性是否被违反，例如编码-解码往返、幂等性、代数定律、差分测试、自洽性，或与参考实现等价。例如，针对 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 编译的二进制文件。7随后，我们对另外六个广泛使用的库重复了这一过程。在此过程中，我们在边缘案例中发现了一些轻微（不可利用）的 bug，目前正在向上游提交。我们从这项工作中得出两个结论：(1) 这些经过极其充分测试的代码库已经几乎完全正确；(2) 对真实现有代码库证明端到端的正确性属性是可能的。
在另一项实验中，我们让 Claude 用 Rust 开发一个支持 Python 大部分子集的解释器，并（使用 Verus——一个 Rust 验证工具）证明其符合一篇学术论文中概述的 CPython 语义。随后，我们通过运行超过 170 万个随机生成的 Python 程序，实证测量了其对 CPython 行为的符合程度，发现 99.95% 的测试中行为与 CPython 完全一致，其余测试差异均为意料之中的已知边缘案例。
我们还通过对简单安全属性的形式化验证尝试，在几个广泛使用且关键的应用程序中发现了问题。在其中一个应用里，我们发现了一个潜伏了十多年的此前未知的逻辑缺陷。在验证一款广泛使用的 PDF 阅读器的过程中，我们一周内发现的安全缺陷数量相当于通常一年报告的数量。
参见附录了解其中一些工作的更多细节。
这仅仅是开始
LLM 辅助形式化验证的关键局限之一是，生成证明可能需要数亿个 token。如果我们的目标是让这些方法惠及整个软件生态，成本效率就至关重要。幸运的是，有充分理由预期效率会提升。
更新的模型需要更少的 token
我们构建了 36 个小型验证任务来自真实的 OSS-Fuzz 代码。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 等关键基础设施。
局限性
在实践中，形式化验证有时能证明的代码安全性可能少于我们的期望。
“形式化验证”并不意味着“没有 bug”。Claude 可以写出一个证明，表明编译后程序的行为满足形式化规范的要求（该证明由外部证明检查器验证）。然而，证明检查器无法告诉你你的规范是否与现实相符。要与现实相符，规范必须正确地涵盖并建模已验证程序所运行的真实机器的一切，包括 CPU 和操作系统。当已验证的代码中出现 bug 时，是因为规范或假定的机器语义与现实不符。幸运的是，这也意味着我们知道在哪里寻找剩余的 bug，以及如何设计一个系统，将这些仍可能存在 bug 的缺口最小化。以下是这如何适用于我们的证明，以及未来工作的思路——这些工作将弥合这些缺口。
真实机器做了模型未描述的事情。我们的证明针对的是单线程、静态链接到 musl libc 的 RISC-V 二进制文件。然而，大多数人会在 x86 或 ARM 上运行这些库，并将它们动态链接到 glibc。要弥合这一缺口，我们需要更接近实际部署系统的系统模型。例如，朝这个方向迈出的一步是为 x86 生成准确的语义。
该主张可能并未涵盖我们关心的所有内容。我们证明了在 Google OSS-Fuzz 的许多模糊测试入口点上，对于任何小于 64 MB 的输入都不会触发崩溃，包括 ASan 崩溃。然而，ASan 并不能检测所有内存安全 bug，而且我们并未验证每个库的所有入口点。即使我们做到了，验证所有入口点也无法覆盖整个库（尤其是在存在死代码的情况下）。此外，真实程序可能会误用该库，导致调用方发生内存损坏。要弥合这一缺口，我们需要规定调用方对每个公共函数必须做什么，并且调用方必须严格遵守。
我们预计，随着我们对如何利用 LLM 进行形式化方法的学习不断深入，以及模型持续改进，这些局限性将变得可解决，我们将能够验证我们所依赖代码中更大比例的部分。
结论
轨迹很清晰：形式化验证过去只有在最关乎安全的代码中，为定制化专家手工打造的保证才具有实际可行性，而它很快就会像今天的模糊测试之于几乎所有生产软件那样切实可行。正如静态类型、测试框架和其他正确性工具一样，验证将从“外挂式”成熟为“内置式”，其驱动力不仅来自 LLM，还来自语言设计和开发工作流的创新。
在当今世界——LLM 会自动扫描并发现越来越多的代码漏洞——我们必须采用能够保证代码安全属性的流程。LLM 规模化的形式化验证是一种很有前景的方法，能够以前所未有的范围和规模来确保这些保证。我们鼓励其他人也进行实验，这样我们就能共同构建一个世界：稳健的软件广泛普及，软件缺陷成为被充分理解且可快速处理的罕见现象。