Anthropic：Claude 在 RISC-V 汇编级形式化验证 123 个开源库
Anthropic Frontier Red Team 与 Theorem 10 月 22 日发文：用 Claude 在 RISC-V 汇编级为 OSS-Fuzz 中 123 个开源库、239 个入口点写出约 1.8 亿行 Rocq 无崩溃证明（输入 <64MB）；过程中还揪出 fuzz 多年未发现的洞。Theorem 同步开放 OSS Verify。
官方称：传统形式化验证代价极高（如 seL4 实现约 2 人年、验证约 20 人年），但前沿模型已能大规模自动写证明。团队把 Google OSS-Fuzz 的 fuzz 入口编译成 RISC-V 可执行文件，配 Theorem 的 RISC-V/Linux 语义，把「任意输入都不崩溃」写成规约；Claude 写证明，Rocq 内核校验。数周内覆盖 239 个入口、123 个库，证明约 1.8 亿行 Rocq，典型单证约 60 万行，对应中位约 1.8 万条 RISC-V 指令。
证明假设单线程、静态链接、固定内存预算的 RISC-V Linux 二进制；可信基是 RISC-V/Linux 语义、定理陈述与 Rocq 检查器本身。尝试证明时 Claude 还发现需约 20MB 特定布局才触发的解压器下溢写越界、需 64MB 输入的图像解码越界读，以及 libexpat 的 CVE-2026-56132 等。部分证明与语义已公开；Theorem 提供 OSS Verify，并放出 Claude skill 帮维护者自证。厂商强调「形式化验证≠绝对无洞」——规约与真实机差仍是剩余风险。
