Claude 数周产出 239 个形式化证明,验证 123 个开源库无崩溃

kieranklaassen · x · 2026-11-12

Serokell 博客解读 Anthropic Frontier Red Team 与 Theorem 10 月 22 日发布的报告:Claude 在几周内为 123 个开源库中的 239 个 fuzz-test 入口点生成了机器可验证的证明,证明其在任意 64 MB 以内输入下都不会崩溃,且是直接对编译后的 RISC-V 二进制在建模的 Linux 环境中推理得出的。这些库中包括一些尽管经过数万亿次 fuzzing 仍多年未被发现、由 Claude 找到并修复的 bug。文章分析了形式化验证的启示:LLM 生成的「slop 代码」需要人工审查,而机器检查的证明则不同——它要么通过要么不通过,无需同样程度的人工把关。随着 AI 代码生成成本下降,形式化证明正从仅限任务关键代码的奢侈品,变成可适用于更广泛应用的可行手段。