Claude 为 123 个开源库出汇编级形式化证明：239 个入口证明永不崩溃

10 月 22 日 Anthropic 公布与 Theorem 合作的结果：让 Claude 在编译后的 RISC-V 指令（即可执行二进制）上证明「任何不超过 64 MB 的输入都不会崩溃、越界或断言失败」，覆盖 123 个 OSS-Fuzz 开源库的 239 个入口点。证明总量约 1.8 亿行 Rocq，单个证明典型约 60 万行，对应二进制的指令数中位为 1.8 万条。

意义在于把「证明」变成可以批量生产的东西。此前形式化验证只用于航天等极少数场景——seL4 内核实现只要 2 人年，验证却要数十人年。而这里由 Rocq 检查器保证证明确实满足规格，开发者只需信任三样东西：RISC-V 与 Linux 进程的形式语义、被证明的定理陈述、检查器本身。

过程中发现数百个 bug 并让 Claude 自行修补，例如只在 20 MB 稀有布局输入下触发的下溢越界写、需 64 MB 输入和 2 GB 内存才出现的解码器越界读，以及 libexpat 里 CVE-2026-56132 的再发现。边界：目前假设单线程静态二进制、固定内存预算、RISC-V 加 Linux，官方只公开了一部分证明。

原文链接：Anthropic 官方页面