Anthropic：LLM 让软件形式化验证在更大规模上变得可行

Anthropic 与 Theorem 合作，用 Claude 为 123 个 OSS-Fuzz 开源库的 239 个模糊测试入口在 RISC-V 汇编层面证明了无崩溃性质，并称这是首个在汇编代码层面用 AI 对生产软件做形式化验证的大规模工作。证明合计约 1.8 亿行 Rocq，覆盖小于 64 MB 的所有输入，前提是程序为 Linux 上的单线程静态二进制。证明过程中 Claude 发现并修复了数百个长期未被测出的 bug，包括需要约 20 MB 特定布局输入的越界写和 libexpat 中的 CVE-2026-56132；对某广泛使用的 PDF 阅读器做验证时，一周发现的安全 bug 相当于通常一年的报告量。效率方面，Opus 5.5 在 36 个小型验证任务上以比 Opus 5 少约 40% 的 token 证明了一半任务。