Claude 形式化验证 123 个库的 239 个入口

Anthropic Frontier Red Team 与 Theorem 当地时间 10 月 22 日发布合作结果：在声明的假设下，证明 123 个开源库里 239 个 OSS-Fuzz 入口点，对任意小于 64MB 的输入都不会崩溃。

形式化验证过，不等于没有漏洞。官方也写了：x86 / glibc 路径不在证明范围内；假设一破，结论就不成立。对维护 C/C++ 关键库的人，更实际的用法是把 OSS Verify / 即将放出的 skill 接进 CI，专门盯那些模糊测试很难撞到的超大输入路径。

注意：数字均来自 Anthropic 研究报告；证明绑定 RISC-V + musl 模型，不能直接当成你线上 x86_64/glibc 二进制已经「验完」。