Anthropic与Theorem用Claude为123个开源库的239个入口生成RISC-V形式化证明

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 还发现了despite 数万亿次测试运行而多年来一直未能检测到的漏洞。随着模型能力不断提升，我们预计形式化验证将成为安全软件开发不可或缺的组成部分。

简介

即便是成熟且经过大量测试的软件也仍存在缺陷，而 LLM 在发现这些缺陷方面正变得越来越娴熟。Linux 内核——当今经过最充分测试的软件之一，部署在全球数十亿台设备上——最近被披露存在超过 1,000 个漏洞。随着前沿模型越来越能够将看似无害的漏洞串联成严重漏洞利用，我们需要能够在这些漏洞被用于真实环境之前检测并修复它们的技术。

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

然而，形式化验证并不容易。证明的规模可能是原始代码的数倍，而编写证明需要大量工作以及小众且高度专业化的技能。例如，实现 seL4 操作系统内核花费了两个人年，但对其进行形式化验证却花费了 20 人年。因此，形式化验证一直只适用于真正攸关生死的应用，例如 Airbus 的航电代码。

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

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

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

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

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

将测试转化为证明

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

为了解决我们希望证明的开源库代码中的这一问题，我们采用以下方法：利用一个关于在 Linux 上执行任何经 RISC-V 编译的二进制文件意味着什么的通用模型，将其原有的可编译测试套件自动转换为规范，并编码规则“此测试套件始终通过”。过去，证明此类规范几乎无从下手，因为要编写一个涵盖并论证任意输入下数万条汇编指令所有可能行为和交互的证明，本身就极其复杂（而且由此产生的证明往往也极其庞大）。如今 LLM 发挥作用了：围绕明确目标处理数百万行代码，恰好是 LLM 极为胜任的任务。

在本项目中，我们首先使用了模糊测试。在这些测试中，开发者会在代码中编写一个入口点²来接收输入，因此任何导致崩溃的输入都是作者关心的缺陷。随后，模糊测试器这一测试引擎会在入口点处生成海量的半随机输入和变异输入，试图找出缺陷（如图 1 所示）。模糊测试器运行得越久，就能发现越多缺陷。但这本质上是一种暴力过程，无论尝试多少输入，都无法保证覆盖每一条可能的代码路径。

为了找出模糊测试本应暴露的所有缺陷，我们将模糊测试转换为针对已编译 RISC-V 指令定义的规范。该规范规定，对于任何小于 64 MB 的输入，模糊测试都不会崩溃。³如果 Claude 能证明这一规范，那么 RISC-V 上的模糊测试就变得多余了：对该入口点进行模糊测试永远都不会发现任何缺陷。

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

在数周之内，Claude 成功修复了它发现的漏洞，随后证明了对任何输入（最大 64 MB），123 个不同 OSS-Fuzz 库中的 239 个入口点均不会发生崩溃。这些证明针对编译后的 RISC-V 指令（即，可执行二进制文件）运行，由约 180 million 行 Rocq 构成；典型证明长达约 600,000 行，可为中位长度达 18,000 条 RISC-V 指令的二进制文件提供安全保证。这些证明的构建方式是利用 Theorem 的 RISC-V 指令语义和 Linux 进程语义，将 RISC-V 汇编代码转换为数学模型。这意味着，这些证明目前假定程序以单线程静态二进制文件的形式，在使用 Linux OS 的 RISC-V CPU 上以固定的内存预算运行。扩大这些证明的覆盖范围完全可行，因为这将为更多汇编架构和其他操作系统进程制定标准化语义。请查看专家对 Claude 所编写证明的解读。

虽然这是数量极其庞大的证明代码，但几乎无需人工审查。Rocq 证明检查器确保规范已由证明正确满足。因此，开发者唯一需要信任的产物是：

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

这并不意味着这些库完全没有错误。 相反，这意味着任何仍然存在的错误，要么位于上述构件之中，要么在 Claude 证明所涵盖的范围之外。强化这些可能仍存在错误的可信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但这比调试规模化证明所涵盖的每一行代码要可行得多——尤其是因为这种方法可以在不增加可信组件规模的情况下，为任意数量的项目提供保障。

我们欢迎对我们的证明进行独立验证，也鼓励对我们的方法加以改进。为此，我们正在发布为该项目制作但尚未公开的可信组件（见上）；Claude 针对无需修补的模糊测试的完整 Rocq 证明；以及其他我们无法证明的模糊测试的规格说明。

查找并修复错误

上文表明，你可以将许多开源库由开发者编写的测试（模糊测试）转化为规格，并让 Claude 证明这些规格将始终通过，有时只需先修补它发现的剩余错误。因此，尝试证明这些规格的过程发现了数百个错误。

Claude 在尝试证明数百个入口点的过程中发现了大量错误。为了确保每次发生这种情况时 Claude 都不必停下来等待人类处理，我们让 Claude 修复它发现的错误：它对代码进行了修补，导致规格根据修补后的代码重新生成，随后 Claude 继续证明新的规格。⁶

我们发现的许多缺陷都是模糊测试器几乎不可能找到的。模糊测试器会对小型输入进行变异，通常上限为 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 编译生成的二进制文件。⁷ 随后，我们对其他六个广泛使用的库重复了这一过程。在此过程中，我们发现了一些边缘情况中的轻微（无法利用）漏洞，目前正在向上游提交。我们从这次实践中得出两个结论：(1) 这些经过极其充分测试的代码库几乎已经完全正确；(2) 可以针对现实中已有的代码库，证明端到端的正确性属性。

在另一项实验中，我们让 Claude 使用 Rust 开发一个涵盖 Python 大部分子集的解释器，并使用 Verus（一种 Rust 验证工具）证明它遵循学术论文中阐述的 CPython 语义。随后，我们通过运行超过 1.7 million 个随机生成的 Python 程序，实测其对 CPython 行为的遵循程度，发现两者在 99.95% 的测试中行为一致，其余测试差异也如预期般属于已知的边缘情况。

我们还通过形式化验证尝试检查简单安全属性，发现了几个广泛使用且关键的应用中存在的问题。其中一个应用存在一个此前未知、且已潜伏十余年的逻辑漏洞。在验证一款广泛使用的 PDF 阅读器时，我们一周内发现的安全漏洞数量，就相当于通常一年内报告的数量。

有关其中一些尝试的更多详情，请参阅附录。

这只是开始

LLM 辅助形式化验证的一项主要局限在于，生成证明可能需要数亿个 token。如果我们希望将这些方法提供给整个软件生态系统，成本效率至关重要。幸运的是，我们有充分理由期待效率会得到提升。

较新的模型需要更少的 token

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

证明可以重复使用

当智能体分别工作时，它们往往会重复大量工作。证明和软件一样，是由规模更小的证明递归构建而成的；证明越小，通常越容易被重复使用。为衡量这一点的影响，我们允许智能体在证明各自目标时互相复制对方的证明。能够访问这个共享工作区后，智能体所需的 token 比独自工作时少 17%；有些智能体甚至在之前的单独尝试失败后成功完成了证明。

在我们的 OSS-Fuzz 证明工作中，我们观察到同样的现象也以大规模方式发生。一份证明的大部分内容都涉及所有程序都包含的代码（尤其是 C 运行时和 AddressSanitizer 的初始化），因此，即使程序差异很大，最终的证明也可能大范围重叠。智能体团队利用这一点，复制另一支团队已完成的证明，然后根据自身程序对其进行调整（图 6）。

证明的这种可复用性，使 Mathlib——一个用 Lean 编写形式化数学的共享库——发展到了接近 300,000 个定理，这些定理由 700 多名贡献者提交：每个新证明都建立在已有的工作成果之上。在 OSS-Fuzz 证明工作过程中，我们积累了一批类似的证明，其中一些将包含在我们的发布版本中（对于可能暴露开源软件中尚未修补漏洞的证明，我们不会发布）。

随着我们完成这些初步实验，我们需要制定一套策略，从最关键的依赖项开始，验证数量庞大的现有软件。正如我们所展示的，借助通用规范并在二进制层面工作，可以大规模实现这一目标，从而无需将整个代码库重写为另一种语言。

这种方法还支持在软件包级粒度上复用证明，这意味着每个依赖项只需验证一次。依赖关系呈幂律分布：即使仅证明一小部分共享库，也能让证明大批软件成为可能。有关验证整个 Nix 生态系统的更多详情，请参阅 Theorem 的路线图；该生态系统包括 glibc、OpenSSL 和 cURL 等关键基础设施。

局限性

在实践中，形式化验证有时无法像我们希望的那样充分证明代码的安全性。

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

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

该声明可能无法涵盖我们所关心的所有方面。我们证明了在 Google OSS-Fuzz 中许多模糊测试入口点（包括 ASan 崩溃）上，任何小于 64 MB 的输入都不会触发崩溃。然而，ASan 不会检测所有内存安全错误，我们也没有验证每个库的所有入口点。即便我们做到了，验证所有入口点也无法覆盖整个库（尤其是在存在死代码的情况下）。此外，真实程序可能会误用该库，导致调用方出现内存损坏。要弥合这一差距，我们需要为每个公共函数指定调用方必须执行的操作，并且调用方必须严格遵守这些要求。

我们期望，随着我们对如何利用大语言模型进行形式化方法的研究不断深入，以及模型的持续改进，这些限制将变得可以解决，我们将能够验证我们所依赖代码的更大比例。

结论

趋势很明确：形式化验证——过去仅在最关键安全代码中定制化的专家级保证方面才切实可行——很快将对几乎所有生产软件变得像今天的模糊测试一样实用。正如静态类型、测试框架以及其他正确性工具一样，验证将从“附加式”走向“内置式”，这一进程不仅由大语言模型驱动，也得益于语言设计和开发工作流方面的创新。

在当今世界——大语言模型能够自动扫描并发现越来越多的代码漏洞——我们必须使用能够保证代码安全属性的流程。大语言模型加持下的形式化验证是一种前景广阔的方法，能够以此前无法企及的广度和规模来落实这些保证。我们鼓励其他人进行实验，以便共同构建一个健壮软件广泛普及、软件错误成为被充分理解并能快速解决的罕见问题的世界。

阅读完整附录。