Anthropic 研究：LLM 使大规模形式化软件验证变得可行

凯恩·卢卡斯, 安格斯·林奇, 卢娜·通, 卢克·钱普恩, 泽基·斯特拉兹尼克纳斯, 丹尼奥·迪斯特凡诺, 哈希卡·阿格拉瓦尔
埃维塔尔·本·阿谢尔, 艾娃·豪厄尔, 萨米·贾瓦哈尔, 克里斯·罗尔夫, 尼科莱亚·泽尔多维奇
尼古拉斯·卡林尼, 拉贾什里·阿格拉瓦尔, 詹森·格罗斯

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

引言

即使是成熟且经过大量测试的软件也包含错误，而大型语言模型在 越来越擅长 发现它们。当今最经过充分测试的软件之一——Linux 内核，最近披露了 超过 1,000 个漏洞。随着前沿模型在 将看似无害的错误链式反应 成为核心漏洞的能力不断增强，我们需要技术来在它们在野外被利用之前检测和修复这些错误。

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

然而，形式化验证并不容易。证明可能比原始代码大很多倍，而编写它们需要大量的工作和一个专门的、高度专业化的技能集。例如，实现 seL4 操作系统内核花费了两个人年，但 20 个人年 用于形式化验证它。因此，形式化验证仅在真正关键的应用中才是可行的，例如 空客的航空电子代码。

但是，大型语言模型让这一切变得容易得多。前沿模型现在可以完全自主地为现实世界中的软件生成正确性证明。为了证明这一点，我们要求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将这些字节解码为相应的图像。但对于大多数程序来说，事情并不那么简单。对于一个文本编辑器或一个网络浏览器来说，“正确”意味着什么？获得全面且无歧义的规范的难度是大规模验证软件的一个重大障碍。

To address this for the code in the open-source libraries that we sought to prove, we take the approach of automatically converting their preexisting compilable test suites into a spec by encoding the rule “this test suite always passes,” using a general model of what it means to execute any RISC-V-compiled binary on Linux. Historically, proving such specs was intractable, given the inherent complexity of writing a proof that can encompass and make an argument over all possible behaviors and interactions of tens of thousands of assembly instructions over any input (and the fact that proofs tend to be extremely large as a result). This is where today’s LLMs come in: churning through millions of lines of code in pursuit of a well-defined goal is a task that LLMs are extremely well suited for.

For this project, we started with fuzz tests. In these tests, developers write an entry point² into their code that takes inputs, such that any input that causes a crash is a bug the authors care about. Then the fuzzer, a testing engine, generates enormous numbers of semirandom and mutated inputs at the entry point to try to find a bug (visualized in Figure 1). The longer a fuzzer runs, the more bugs it can find. But this is inherently a brute-force process, with no guarantee of exercising every possible code path, regardless of how many inputs you try.

To find all the bugs that would’ve been surfaced by a fuzz test, we turned the fuzz test into a spec defined over the compiled RISC-V instructions. The spec says that the fuzz test won’t crash for any input less than 64 MB.³ If Claude can prove this spec, the fuzz test on RISC-V becomes superfluous: fuzzing that entry point will never find any bugs.

We did this for hundreds of projects in Google’s OSS-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects. OSS-Fuzz contains thousands of developer-authored entry points that look for broken code properties by crashing (for example, on a failed assertion). OSS-Fuzz automatically instruments C and C++ programs with AddressSanitizer⁴ (ASan), causing them to crash whenever memory is accessed improperly (which is a leading cause of software vulnerabilities). Broad-spectrum specifications like memory safety apply to almost all software.

在几周的时间里，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 编写的证明的看法。

虽然这是一个巨大的证明代码量，但几乎不需要手动审查。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 直接使用 Claude 生成的（并经过大量测试）的 x86 指令集的形式语义来证明 x86 编译的二进制文件。⁷ 然后，我们重复了这个过程，针对另外半打其他广泛使用的库。在这个过程中，我们发现了一些在边缘情况下的轻微（不可利用的）错误，这些错误正在提交给上游。从这个练习中，我们得出两个结论：(1) 这些经过极好测试的代码库已经几乎完全正确，(2) 可以证明真实现有代码库的端到端正确性属性。

在另一个实验中，我们要求 Claude 用 Rust 开发一个 Python 大部分子集的解释器，并使用 Verus（一个用于 Rust 的验证工具）证明它遵循学术论文中概述的 CPython 语义。然后，我们通过运行超过 170 万个随机生成的 Python 程序来经验性地测量其对 CPython 行为的遵循程度，发现 99.95% 的测试与 CPython 行为一致，剩余的测试差异作为不令人意外的已知边缘情况。

我们还通过简单的安全属性形式验证尝试，在几个广泛使用且关键的应用中发现了问题。在其中之一，我们发现了一个潜伏了十多年的以前未知的逻辑错误。在努力验证一个广泛使用的 PDF 阅读器期间，我们发现了一周内的安全错误数量通常一年才会报告一次。

有关这些工作的更多详细信息，请参见 附录。

这只是一个开始

LLM 辅助形式验证的一个关键限制是，证明可能需要数亿个 token 来生成。如果我们的目标是使这些方法可供整个软件生态系统使用，那么成本效益至关重要。幸运的是，有充分的理由预期效率会提高。

新模型需要的 token 更少

我们从真实的 OSS-Fuzz 代码中构建了 36 个小型验证任务 来自真实 OSS-Fuzz 代码。Opus 5.5 证明其中一半任务所需的 token 比 Opus 5 少了大约 40%。我们预计随着模型在长时间验证任务上进行训练，这一趋势会继续。

证明可以被重用

当代理独立工作时，它们往往会重复大量工作。证明，就像软件一样，是递归地从较小的证明构建起来的——较小的证明越小，它们就越容易被重用。为了衡量这种影响，我们让代理在证明自己的目标时复制彼此的证明。当获得访问这个共享工作空间时，代理需要的 token 比单独工作少了 17%，有些代理甚至在之前单独尝试失败后成功了。

我们在OSS-Fuzz证明工作中观察到相同的现象以规模发生。证明中的大部分代码涉及每个程序都包含的代码（特别是C运行时和AddressSanitizer的初始化），因此非常不同的程序最终可能会得到显著重叠的证明。代理团队利用这一点，通过复制另一个团队完成的证明，然后将其调整到自己的程序（图6）。

这种证明的可重用性是Mathlib，Lean中的形式数学共享库，增长到近30万条定理，由超过700名贡献者提交的原因：每个新的证明都建立在现有工作基础上。我们在OSS-Fuzz工作中积累了类似的证明体，其中一些我们包含在我们的发布中（我们不发布可能揭示开源软件中未修复漏洞的证明）。

随着我们从这些初始实验中毕业，我们需要一个验证庞大现有软件的策略，从最关键的依赖项开始。正如我们所展示的，这可以通过使用通用规范并在二进制级别工作来实现，从而避免了需要在另一种语言中重写整个代码库的需要。

这种方法也促进了在包级粒度上重用证明，这意味着每个依赖项只需要验证一次。依赖项遵循幂律：证明即使是少量共享库也能使大量软件变得可行。更多详情，请参阅Theorem’s roadmap，用于验证Nix生态系统的全部内容，其中包括关键基础设施如glibc、OpenSSL和cURL。

局限性

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

“形式验证”并不意味着“无错误。” Claude可以编写一个证明，显示编译程序的行为满足形式规范的要求（该规范由外部证明检查器验证）。然而，证明检查器无法告诉您您的规范是否与现实相符。要与现实相符，规范必须正确涵盖和模拟验证程序运行的现实机器的所有内容，包括CPU和操作系统。当验证的代码中出现错误时，是因为规范或假设的机器语义与现实不符。幸运的是，这也意味着我们知道在哪里查找剩余的错误，以及如何设计一个系统，使那些仍然可能存在错误的间隙最小化。以下是这种方式如何适用于我们的证明，以及为关闭这些差距的未来工作的想法。

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

这个声明可能无法涵盖我们关心的所有内容。我们证明了在 Google OSS-Fuzz 中的许多模糊入口点下，任何小于 64 MB 的输入都不会触发崩溃，包括 ASan 崩溃。然而，ASan 并不能检测所有内存安全漏洞，我们也没有验证每个库的所有入口点。即使我们验证了所有入口点，整个库也不会被覆盖（尤其是如果有死代码）。此外，真实程序可能会误用库，导致 调用者 的内存损坏。为了弥补这个差距，我们需要指定每个公共函数调用者必须做什么，并且调用者必须严格遵守它。

我们预计，随着我们更多地了解如何利用 LLMs 进行形式化方法，并且随着模型的持续改进，这些限制将成为可行的，我们将能够验证我们依赖的更大百分比的代码。

结论

轨迹是清晰的：形式化验证，历史上只在最安全关键代码中实用的是定制专家制作的保证，很快将像今天模糊测试对几乎所有生产软件一样实用。就像静态类型、测试框架和其他正确性工具一样，验证将从“附加的”成熟为“内置的”，不仅由 LLMs 驱动，还由语言设计和开发工作流程的创新驱动。

在当今世界——其中 LLMs 自动扫描并发现越来越多的代码漏洞——我们必须使用能够 保证 代码安全属性的流程。LLM 规模的形式化验证是一种有前景的方法，可以在以前无法达到的范围和规模上确保这些保证。我们鼓励其他人进行实验，以便我们能够共同建设一个在稳健软件已非常广泛普及，软件错误是众所周知且可以快速解决的罕见性的世界。

阅读完整附录。