Anthropic 使用 Claude 在 RISC-V 汇编层面正式验证 123 个 OSS-Fuzz 库

Anthropic 和 Theorem 宣布的内容

Anthropic 宣布，与验证公司 Theorem 合作，Claude 能够以以前不切实际的规模编写正式软件证明。该团队使用 Claude 直接在超过 100 个真实世界开源库的编译后 RISC-V 汇编上证明安全属性——具体来说，是 123 个 OSS-Fuzz 库中的 239 个模糊测试入口点。Anthropic 这样描述结果：“据我们所知，这是首次大规模使用 AI 在汇编代码层面将正式验证应用于生产软件。”

所证明的属性比“无缺陷”更窄，Anthropic 对此非常明确。Claude 证明了每个被覆盖的程序对于所有小于 64 MB 的输入以及所有建模的 Linux 操作系统响应和内存布局，都将始终正常退出，而不会触发内存安全错误或断言失败。这些证明假设程序作为单线程静态二进制文件，在运行 Linux 的 RISC-V CPU 上以固定内存预算运行。

OSS-Fuzz 验证工作的关键数字

  • 证明了 123 个不同 OSS-Fuzz 库中的 239 个模糊测试入口点。
  • 总共约 1.8 亿行 Rocq 证明。
  • 一个典型证明约 60 万行，覆盖中位长度为 18,000 条 RISC-V 指令的二进制文件。
  • 生成证明花费了几周时间。

正式验证历来在专家时间上昂贵，而不是在计算上。Anthropic 引用了 seL4，即经过验证的操作系统内核，它花了两个人年实现，但花了 20 个人年进行正式验证。这种成本状况是验证一直局限于关键任务代码（如空中客车航空电子设备）的原因。这项工作的主张是，LLM 生成的证明改变了这种计算方式。

模糊测试如何转换为正式规范

核心方法论举措是避免手动编写规范。对于大多数程序，全面且无歧义的规范是困难的部分——正如 Anthropic 所问，文本编辑器或网络浏览器“正确”意味着什么？相反，该团队将“这个现有测试套件始终通过”的规则编码为对编译后 RISC-V 指令的正式规范，使用一个通用模型来描述在 Linux 上执行任何 RISC-V 编译二进制文件意味着什么。

具体来说，该流程分四个阶段进行：

  1. 将库及其现有模糊测试编译为 RISC-V 可执行文件。OSS-Fuzz 自动使用 AddressSanitizer (ASan) 检测 C 和 C++ 程序，这会使不当的内存访问崩溃。
  2. Theorem 的正式 RISC-V 指令和 Linux 进程语义将机器代码转换为数学模型。
  3. Claude 编写一个 Rocq 证明，证明生成的规范成立。
  4. Rocq 证明检查器根据规范机械地验证证明。

该规范声明，模糊测试对于任何小于 64 MB 的输入都不会崩溃。如果证明成立，那么对该入口点进行模糊测试将无法再发现任何问题。在链接了 ASan 的情况下证明“不崩溃”也确立了所覆盖路径的内存安全性，因为 ASan 将越界访问转换为崩溃。

开发人员实际必须信任什么

Anthropic 认为，几乎不需要人工审查任何生成的证明代码，因为 Rocq 证明检查器会根据规范强制执行证明的正确性。剩余的受信任工件很小且可枚举：

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

Anthropic 直截了当地说明了后果：“这并不意味着这些库没有缺陷。”剩余的缺陷要么存在于这些受信任组件内部，要么超出证明范围。加固这些组件并非易事，但 Anthropic 认为这比审计证明覆盖的每一行代码要容易得多——而且与代码不同，随着更多项目被验证，受信任基础不会增长。

发现多年模糊测试遗漏的缺陷

尝试证明过程发现了数百个缺陷，Claude 被允许自主修补它们：它修复了代码，从修补后的代码重新生成规范，然后 Claude 证明了新规范。这很重要，因为许多缺陷超出了传统模糊测试的范围，传统模糊测试通常变异限制在约 1 MB 的小输入，并依赖覆盖率指导。

Anthropic 报告的具体示例：

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

Anthropic 总结了这一点：即使最终目标——完成无崩溃证明——没有实现，尝试本身也会产生需要修复的真实缺陷。

证明超出内存安全的属性

证明模糊测试从不崩溃比听起来更强大，因为现实世界的模糊测试经常编码高级属性：编码-解码往返、幂等性、代数定律、差分测试、自洽性或与参考实现的等价性。例如，LZO 压缩算法的模糊测试断言压缩输入然后解压缩会返回原始输入。如果属性失败，程序会崩溃，因此证明测试从不崩溃等同于证明属性本身。

属性也可能在证明过程中变得必要，而无需开发人员声明。为了完成 cpp-httplib 的 OSS-Fuzz 证明，Claude 必须排除由 std::set 析构函数中过度递归引起的堆栈溢出。该递归深度受树的最大深度限制，因此 Claude 必须在机器代码上证明 libc++ 的红黑树重新平衡算法保持树深度对数有界。

同一报告中的其他正式验证案例研究

Anthropic 描述了 OSS-Fuzz 流程之外的三个额外实验。

zlib 对照 RFC 1950。 Claude 编写了 RFC 1950（定义 zlib 压缩文件格式的文档）的正式规范，然后证明了 Linux 内核中的 zlib 实现正确实现了该规范。该属性在二进制级别被证明，但针对的是 x86 编译的二进制文件而不是 RISC-V，使用了 Claude 生成并经过大量测试的 x86 指令集正式语义。Anthropic 对另外六种广泛使用的库重复了该过程，并在边缘情况中发现了轻微、不可利用的缺陷，这些缺陷正在向上游提交。得出的两个结论：这些经过极其充分测试的代码库已经几乎完全正确，并且关于真实现有代码库的端到端正确性属性是可证明的。

使用 Verus 验证的 Rust 编写的 Python 解释器。 Claude 用 Rust 开发了一个大型 Python 子集的解释器，并使用 Verus 证明它遵循了一篇学术论文中概述的 CPython 语义。Anthropic 随后使用超过 170 万个随机生成的 Python 程序进行了经验测试，发现 99.95% 的测试与 CPython 行为相同，其余差异被描述为意料之中的已知边缘情况。

关键应用程序中的安全属性。 验证广泛使用软件的简单安全属性直接发现了问题：在一个应用程序中，发现了一个潜伏了十多年、以前未知的逻辑缺陷；在一个广泛使用的 PDF 阅读器中，一周内发现的安全缺陷数量与通常一年报告的数量相当。

成本、令牌效率和证明重用

Anthropic 将成本列为主要当前限制：证明可能需要数亿个令牌才能生成。给出了两个预期改进的趋势。

首先，更新的模型需要更少的令牌。在 36 个基于真实 OSS-Fuzz 代码构建的小型验证任务中，Opus 5.5 以比 Opus 5 少约 40% 的令牌证明了一半的任务。每个任务在 500 万令牌预算下进行了三次独立的单代理尝试，并在第一次尝试完成时计为已证明。Anthropic 预计随着模型在长验证任务上训练，这一趋势将继续。

其次，证明可以重用。证明像软件一样，递归地由更小的证明构建，而更小的证明更可重用。当代理在共享工作区中工作并复制彼此的证明时，他们需要的令牌比单独工作的代理少 17%，并且一些代理在之前单独失败后成功了。在 36 个任务的实验中，共享工作区的成本在 34 个完成的证明中有 30 个低于单独平均成本，而单独工作的代理无法完成其中两个。

同样的效果在 OSS-Fuzz 工作中大规模出现。任何证明的大部分都涉及每个程序都包含的代码，特别是 C 运行时和 AddressSanitizer 初始化，因此不相关的程序最终会有大量重叠的证明。代理团队复制了完成的证明并使其适应自己的程序；在发布的 libcups、freerdp 和 libzmq 比较中，共享部分几乎没有获得新代码。

Anthropic 将此与 Mathlib（Lean 中正式数学的共享库）进行比较，该库已增长到近 30 万个定理，由 700 多人贡献，因为每个新证明都建立在现有工作之上。该公司发布了 OSS-Fuzz 证明的一个子集，扣留了可能揭示未修补缺陷的证明。

发布的工件以及如何复现这项工作

  • 证明：一个子集发布在 github.com/theorem-labs/oss-verify-proofs，包括不需要修补的模糊测试的完整 Rocq 证明，以及无法证明的模糊测试的规范。
  • 语义：用作受信任模型的 RISC-V 和 Linux 进程语义发布在 github.com/theorem-labs/rocq-linux-process-semantics。
  • 工具：Theorem 发布了一个 Claude 技能，以帮助开发人员上手他们自己的代码，并提供为其他开源项目运行相同流程的服务。
  • 完整附录：一个更长的 PDF 附录涵盖了额外的案例研究和外部专家对证明的评估。

LLM 辅助正式验证的既定局限性

Anthropic 用一节专门解释为什么“正式验证”不等于“无缺陷”，并指出了三个不同的差距。

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

声明可能未涵盖所有重要内容。 ASan 不能检测所有内存安全缺陷，并且并非每个库中的每个入口点都经过验证。即使验证所有入口点也不能覆盖整个库，特别是如果存在死代码。真实程序也可能误用库并在调用者中导致内存损坏；缩小这一差距需要指定调用者必须为每个公共函数做什么，并要求调用者遵守。

规范可能与现实不符。 证明检查器无法告诉您规范是否与现实世界对应。Anthropic 写道：“Claude 可以编写一个证明，表明编译后程序的行为满足正式规范的要求（由外部证明检查器验证）。但是，证明检查器无法告诉您您的规范是否与现实相符。”当验证代码中出现缺陷时，那是因为规范或假定的机器语义与现实存在分歧——这至少告诉您去哪里寻找。

Hacker News 讨论补充了什么

讨论中被转载最多的批评是验证的好坏取决于其规范。一位评论者将阶梯总结为愿景、蓝图和检查：“这项研究使检查接近完美。但检查只检查蓝图，而不是我们的愿景，因此根据错误蓝图建造的房子仍然可以通过完美检查。”一个相关评论问，人们如何确定模型忠实地代表了正在验证的程序——“难道不可能您证明的不是您的实际程序吗？”另一位更直率地说：“想象一下为现实制定一个正式规范！”

第二个主题是标准的验证与确认区分仍然适用。一位评论者用 IEEE 术语表述：验证问“我们是否正确地构建了产品？”而确认问“我们是否构建了正确的产品？”——“您可以编写数学上完美无缺的代码，高效地解决错误的问题。”

第三个主题是预测的能力墙。一位评论者引用了报告自己的附录，该附录询问代理是否可以将冗长的证明风格扩展到更复杂的程序，并指出“来自其他基于代理的验证项目（如 MachCSL）的经验表明，答案可能是否定的：代理在冗长的证明风格上遇到了复杂性墙。”同一位评论者认为，正式验证是 LLM 推理的有用试金石，正是因为这些系统不一定在模型的分布上，这为“凸包”假设提供了可信度，即 LLM 将在人类产生的数学前沿之外停滞不前。

讨论中的从业者报告了他们自己的成功。一位说他们构建了一个编译器，将 Rust 和 C 都翻译成 Lean，并让 LLM 证明行为等价性，覆盖了约 12% 的代码——约 70,000 行 C——用于单线程执行，发现了非常小的差异，例如浮点行为在不同平台上有所不同。另一位描述了一个代理打开了一个 PR，使用 SIMD 或 CUDA 加速了一个函数，并自信地合并了它，“因为 PR 有一个 Rocq 证明，证明它与原始实现行为等价。”第三位报告使用 Codex 构建了一个授权系统的 Alloy 模型，然后对服务器进行了数小时的红队测试，没有产生权限提升。

怀疑也集中在组织激励而非技术限制上。一位评论者怀疑采用会随之而来：“由于我们迄今为止在软件中采用 LLM 主要是为了抛弃最佳实践，我怀疑它会导致我们扩大验证，”将这一承诺比作高管预测更短的工作周。另一位警告说，懒惰是真正的风险——跳过代码审查和“氛围编码”正式验证仍然会带来麻烦，并且“完美是好的敌人。”

几位评论者直接提出了劳动力影响，一位问报告作者是否考虑过证明与 Lean 类比中一个看似合理但不匹配其正式工件的论文相匹配，指的是早期 OpenAI Lean 工作。其他人要求提供更多关于从代码到证明的工作流程细节，至少有一位指出，除非被指示，否则 Claude 不会主动使用正式验证。

为什么这对软件构建方式很重要

Anthropic 的结论是一个轨迹声明，而不是成品声明：正式验证，历史上仅在最安全关键的代码中为定制的专家级保证而实用，将变得像今天的模糊测试一样对大多数生产软件实用，从附加式转变为内置式，与语言设计和开发工作流程变化并行。该公司明确鼓励那些尝试过使用能力较弱的模型进行正式验证但发现不起作用的开发人员再次尝试。

该报告还概述了现有软件基础的战略：在二进制级别使用通用规范进行验证，这样代码库就不需要用另一种语言重写，并在包粒度重用证明，这样每个依赖项只需验证一次。依赖项遵循幂律，因此证明一小部分共享库——Theorem 的路线图在 Nix 生态系统中提到了 glibc、OpenSSL 和 cURL——将使大量软件变得可验证。

Sources

相关