Anthropic的LLM形式化验证：Claude在RISC-V汇编层面证明123个OSS-Fuzz库的无崩溃属性

Anthropic及其合作者Theorem报告称，Claude自主证明了123个真实世界开源库的无崩溃安全属性，直接针对编译后的RISC-V汇编代码而非源代码工作。Anthropic称这是首次大规模将AI驱动的形式化验证应用于汇编代码级别的生产软件，并表示这些证明还发现了多年模糊测试未能发现的漏洞。

公告内容

核心主张是，LLM辅助的形式化验证已跨越实用性门槛。不再仅仅依赖模糊测试（一种概率性搜索崩溃的方法），Claude生成了数学证明，证明某些编译后的程序在定义范围内对任何输入都不会崩溃。

具体而言，Anthropic报告称，Claude在超过100个真实世界开源库的RISC-V汇编级别证明了有用的安全属性。在整个工作中，Claude完成了对来自Google OSS-Fuzz计划的123个库中239个入口点的证明。这项工作与Theorem合作完成，后者提供了用于将机器代码转换为数学模型的RISC-V指令和Linux进程语义。

Anthropic明确阐述了动机：Linux内核是现存测试最严格的软件之一，最近披露了超过1000个漏洞，而前沿模型越来越能够将看似良性的漏洞串联成关键攻击。如果LLM能够大规模发现漏洞，那么防御者需要能够证明漏洞不存在而不仅仅是测试其存在的技术。

使用Claude，我们在超过100个真实世界开源软件库的汇编代码级别（RISC-V）证明了安全属性。据我们所知，这是首次大规模使用AI将形式化验证应用于汇编代码级别的生产软件。

流水线如何将模糊测试转化为证明

该流水线复用了开发人员已完成的工作。OSS-Fuzz项目包含数千个由开发人员编写的入口点，当属性被违反时（例如断言失败或AddressSanitizer检测到不当内存访问），这些入口点会使程序崩溃。这些入口点以及现有的模糊测试被编译成RISC-V可执行文件。

该可执行文件，结合Theorem的RISC-V和Linux语义以及所需的无崩溃属性，机械地产生一个证明必须满足的规范。然后Claude编写证明，Rocq证明检查器根据该规范验证它。如果证明尝试失败，失败点指向一个真实漏洞；Claude修补代码，从修补后的代码重新生成规范，循环重复。

所证明的确切属性狭窄但有意义：对于所有小于64 MB的输入，以及所有建模的Linux操作系统响应和内存布局，这些程序将始终正常退出，不会触发内存安全错误或断言失败。

证明在声明的假设下成立：程序作为单线程静态二进制文件，在运行Linux的RISC-V CPU上以固定内存预算运行。Anthropic指出，扩大范围将涉及为更多汇编架构和其他操作系统进程标准化语义。

证明工作的规模

这些数字是证明这是与手写验证不同机制的头条证据。

在123个OSS-Fuzz库中证明了239个入口点
总共产生了约1.8亿行Rocq证明
典型证明约60万行
证明覆盖的二进制文件大小中位数：约18,000条RISC-V指令
输入范围：所有小于64 MB的输入
时间线：几周时间

Anthropic引用的历史对比是seL4操作系统内核，它花了两个人年实现，但花了20个人年进行形式化验证。这个比例是形式化验证一直局限于关键任务领域（如Airbus的航空电子代码）的原因。

开发人员仍需信任的内容

1.8亿行证明代码中几乎不需要人工审查，因为Rocq证明检查器验证了它。Anthropic列出了开发人员必须信任的恰好三个工件：

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

这是关键的结构性论点。可信计算基础不会随着验证项目数量的增加而增长。Anthropic明确警告，这并不意味着这些库没有漏洞。这意味着任何剩余的漏洞要么存在于这些受信任的工件内部，要么超出证明范围。加固Rocq、RISC-V语义和Linux语义是实际工作，但这是一个有界的任务，而不是每个项目的负担。

Claude在编写证明时发现的漏洞

尝试证明本身变成了一个漏洞发现过程。Anthropic报告称，这项工作发现了数百个漏洞，其中许多是模糊测试不太可能发现的。原因是机械性的：模糊测试变异小输入（通常上限为1 MB），并依赖代码覆盖率来指导搜索。

Anthropic描述的具体示例：

一个库的解压器副本中的计数器下溢，导致越界写入，仅在约20 MB的输入且具有一种罕见特定布局时可达。
一个图像解码器中的越界读取，需要64 MB的输入和超过2 GB的内存。
另一个库中的越界读取，需要对同一文件的两个句柄进行特定序列的调用。
重新发现了libexpat中的CVE-2026-56132，这需要深度嵌套的输入。
一个完全没有崩溃的纯逻辑漏洞：在证明一个库内存安全时，Claude注意到一个限制应用程序可以加载哪些文件的功能并不总是被强制执行。

为了避免每次出现漏洞时都停下来等待人工，Anthropic让Claude在同一个循环中修补它发现的漏洞。

证明不仅仅是内存安全

证明模糊测试永远不会崩溃比听起来更强，因为真实的模糊测试编码了高级属性，而不仅仅是内存检查。Anthropic列出了编码-解码往返、幂等性、代数定律、差分测试、自一致性和与参考实现的等价性作为常见示例。例如，LZO压缩算法的模糊测试断言压缩然后解压缩输入返回原始输入；因为失败会使程序崩溃，证明测试永远不会崩溃等同于证明属性本身。

有时所需的义务超出了开发人员的意图。为了完成cpp-httplib的OSS-Fuzz证明，Claude必须排除由std::set析构函数中过度递归引起的堆栈溢出。因为该递归深度受树的最大深度限制，Claude必须在机器代码级别证明libc++的红黑树重新平衡算法保持树的深度对数有界。

其他形式化验证案例研究

Anthropic描述了除OSS-Fuzz模糊测试到证明流水线之外的几个额外实验。

zlib和RFC 1950。 Claude编写了RFC 1950（定义zlib压缩文件格式的文档）的形式化规范，然后证明了Linux内核中的zlib实现正确实现了该规范。与RISC-V工作不同，此证明直接针对x86编译的二进制文件执行，使用Claude生成并经过大量测试的x86 ISA形式化语义。该过程对另外六种广泛使用的库重复进行，并在边缘情况中发现了次要的、不可利用的漏洞，这些漏洞正在提交上游。Anthropic得出两个结论：这些经过严格测试的代码库已经几乎完全正确，并且可以证明真实现有代码库的端到端正确性属性。

Rust中的Python解释器。 Claude用Rust开发了一个大型Python子集的解释器，并使用Verus验证工具证明它符合学术论文中概述的CPython语义。对超过170万个随机生成的Python程序进行的经验测试发现，在99.95%的测试中与CPython行为相同，其余差异是已知的、不令人惊讶的边缘情况。

关键应用程序。 对简单安全属性的形式化验证尝试在几个广泛使用和关键的应用程序中发现了问题。在一个案例中，Claude发现了一个潜伏了十多年的先前未知的逻辑漏洞。在验证一个广泛使用的PDF阅读器的过程中，Anthropic报告称一周内发现的安全漏洞数量与通常一年报告的数量相当。

成本：令牌使用量及其为何应该下降

Anthropic将令牌成本确定为一个关键限制。证明可能需要数亿个令牌来生成，如果这些方法要覆盖整个软件生态系统，成本效率很重要。两个已测量的趋势表明成本将会下降。

第一个是模型改进。Anthropic从真实的OSS-Fuzz代码构建了36个小型验证任务。Opus 5.5用比Opus 5少约40%的令牌证明了一半的任务。每个任务在5M令牌预算下进行了三次独立的单代理尝试，当第一次尝试完成时算作已证明。

第二个是证明重用。当代理被给予一个共享工作区，可以在其中复制彼此的证明时，他们需要的令牌比单独工作时少17%，并且一些代理在单独尝试之前失败的任务上成功了。

同样的效果在OSS-Fuzz工作中大规模出现。大多数证明涉及每个程序都包含的代码，特别是C运行时和AddressSanitizer的初始化，因此非常不同的程序最终会有显著重叠的证明。代理团队复制了另一个团队的已完成证明并进行了调整。在libcups、freerdp和libzmq的已发布比较中，每个证明按保持相同、轻微编辑、更多编辑或新编写的数量进行分解，共享部分几乎没有新代码。在36个共享工作区证明中，34个已完成，其中30个成本低于平均单代理尝试。

Anthropic将这种动态与Mathlib（Lean中的共享形式化数学库）进行了比较，该库已增长到近30万个定理，由超过700名贡献者提交，因为每个新证明都建立在现有工作之上。

Anthropic承认的限制

该帖子明确指出，形式化验证并不提供人们假设的保证。

“形式化验证”并不意味着“无漏洞”。 证明检查器可以显示程序满足规范，但不能告诉您规范是否与现实匹配。当验证代码中出现漏洞时，规范或假定的机器语义与现实不同。Anthropic认为这仍然有用，因为它告诉您在哪里寻找剩余漏洞。

真实机器做了模型未描述的事情。 证明涵盖了链接到musl libc的单线程、静态RISC-V二进制文件。大多数人使用动态链接到glibc的x86或ARM运行这些库。缩小这一差距需要更接近部署系统的系统模型，例如为x86生成准确的语义。

声明可能不涵盖我们关心的所有内容。 ASan不会检测所有内存安全漏洞，并且并非每个库的所有入口点都已验证。验证所有入口点仍然不会覆盖整个库，尤其是在存在死代码的情况下。真实程序也可能以破坏调用者内存的方式滥用库；缩小这一差距需要为每个公共函数指定调用者必须做什么，并让调用者严格遵守。

发布内容

Anthropic和Theorem随帖子发布了几个工件：

证明的子集，位于github.com/theorem-labs/oss-verify-proofs，包括Claude对不需要修补的模糊测试的完整Rocq证明，以及无法证明的模糊测试的规范。
RISC-V和操作系统语义，位于github.com/theorem-labs/rocq-linux-process-semantics。
一个Claude技能，位于github.com/theorem-labs/oss-verify，帮助开发人员开始验证自己的代码。
Theorem提供为其他开源项目运行相同流水线的服务。

Anthropic故意扣留了可能揭示开源软件中未修补漏洞的证明，并邀请独立验证已发布的内容。

为什么这很重要

战略论点是，随着LLM在发现和串联漏洞方面变得更好，仅靠测试成为不足的防御。形式化验证提供保证而非概率，其历史障碍是编写证明的成本，而不是其价值。

Anthropic还认为，单位经济性有利于包而不是程序。证明重用适用于包级粒度，因此每个依赖项只需验证一次，并且依赖项遵循幂律：证明一小部分共享库使大量下游软件变得可证明。Theorem验证整个Nix生态系统的路线图（包括glibc、OpenSSL和cURL等关键基础设施）被呈现为直接的大规模应用。

最后的预测是，形式化验证（历史上仅适用于最安全关键代码中的定制专家精心制作的保证）将变得像今天的模糊测试一样实用，适用于几乎所有生产软件，从附加到内置。Anthropic明确鼓励那些以前尝试过形式化验证但使用能力较弱的模型发现不起作用的开发人员再次尝试。