Anthropic称Claude为123个开源库编写了正式证明，证明它们不会崩溃

Anthropic称，在与 Theorem 合作期间，他们使用 Claude 在汇编层面（RISC-V）证明了100多个真实开源库的安全属性，并称这是 AI 首次大规模用于对生产软件进行这一层面的形式化验证。

据 Anthropic 介绍：

• 证明了什么：针对123个 OSS-Fuzz 库中的239个模糊测试入口，证明对于所有小于64 MB的输入，程序都能正常退出，不会出现内存安全错误或断言失败。这一结论基于以下假设：单线程静态二进制文件、固定内存预算，以及运行 Linux 的 RISC-V CPU。证明总计约1.8亿行 Rocq 代码，并由 Rocq 证明检查器验证。
• 如何做到：将每个库现有的模糊测试转化为一项规范（“此测试永不崩溃”），再由 Claude 编写证明，并在过程中修复发现的漏洞。Anthropic称，这一过程发现了数百个漏洞，包括模糊测试器不太可能触及的漏洞，例如需要罕见的20 MB输入才会触发的越界写入，以及在 libexpat 中重新发现的 CVE-2026-56132。
• 其他实验：Claude 在 x86 二进制层面证明，Linux 内核的 zlib 实现符合 RFC 1950 规范；还构建了一个 Rust Python 解释器，其行为与 CPython 在170万个随机程序中的99.95%上相符。Anthropic还称，对一款广泛使用的 PDF 阅读器进行形式化验证的尝试，在一周内发现的安全漏洞数量，达到通常一年报告的数量。
• 成本：证明可能需要数亿个 token。Anthropic称，在36项小型验证任务中，Opus 5.5有一半能完成证明，所需 token 比 Opus 5 少约40%；共享证明的智能体所需 token 则减少了17%。

Anthropic 正在发布部分证明，以及 RISC-V 和 Linux 的语义模型。Theorem 表示可为其他开源项目运行相同流程，并正在发布一项用于验证自有代码的 Claude skill。Anthropic指出，这并不能证明这些库没有漏洞：剩余漏洞可能存在于受信任组件中，或在证明范围之外。