Claude 在 RISC-V 汇编层证明了 123 个开源库、239 个入口在 64 MB 以内任何输入下都不会崩溃
Anthropic 与 Theorem 合作，把开源库现成的模糊测试转成形式化规格，再让 Claude 写证明。这一条讲规模、顺带找到的漏洞，以及代价。
// 要点
- 做法是把 OSS-Fuzz 里开发者写的模糊测试入口转成定义在编译后 RISC-V 指令上的规格：「这个测试在任何输入下都不会崩溃」，证明成立后，对该入口继续模糊测试就不会再找到漏洞。
- Claude 修补了证明过程中发现的漏洞，最终证明 123 个库的 239 个入口在 64 MB 以内的任何输入下都不会崩溃；证明过程总共发现了数百个漏洞，例如一个只在约 20 MB、特定布局的输入下才会触发的越界写。
- 在对一款广泛使用的 PDF 阅读器做验证时，一周内找到的安全漏洞与通常一年报告的数量相当；另有一个潜伏十多年的逻辑漏洞被发现。
- 主要限制是成本：单个证明可能消耗数亿 token；Theorem 提供为其他开源项目运行同一流程，并公开了部分证明。
开发者视角短期内这不是每个团队都用得起的东西，数亿 token 一个证明。但思路可以先抄：把现有测试当规格，让智能体「证明它总能通过」或至少把边界输入跑透。我会先挑解析上传文件的那一段（AI 云盘里处理 PDF、图片的代码）试，这类代码最容易被超大或畸形文件打穿。