# Claude狂写1.8亿行证明！万亿次测试漏掉的Bug，被AI一锅端

- 原标题：Claude狂写1.8亿行证明！万亿次测试漏掉的Bug，被AI一锅端
- 类型：博客
- 来源：新智元
- 发布时间：2026-10-24
- 首次精选：2026-11-03 21:30
- 分级：值得看
- 是否付费：免费（全文公开可读）
- 预估学习时长：约 6 分钟（按全文字数估算）
- 学习层级：深入
- 主题：[ai-mathematics-proofs](<https://oplearnx.com/md/topics/ai-mathematics-proofs.md>)（第 11 位）、[code-review-verification](<https://oplearnx.com/md/topics/code-review-verification.md>)（第 35 位）
- 原文链接：[https://aiera.com.cn/asi-post.html?id=120295](<https://aiera.com.cn/asi-post.html?id=120295>)
- 本站页面：[https://oplearnx.com/resources/pk\_36c74a57b624](<https://oplearnx.com/resources/pk_36c74a57b624>)

## 摘要

新智元报道，Anthropic前沿红队团队与Theorem Labs发布报告，让Claude对RISC-V机器码进行形式化验证，在123个开源代码库的239个测试入口上累计写出约10亿行Rocq证明，其中约1.8亿行通过Rocq检查器核验。文章描述了该方法与OSS-Fuzz模糊测试的区别：把测试入口改写为数学命题，要求证明规定范围内（小于64MiB输入）不触发约定崩溃，过程中发现数百个Bug，Claude会自行打补丁后继续证明；并给出在Rust写的Python解释器里埋7个Bug、随机测试漏掉5个而证明全部找出的对照实验，以及cJSON一个391行解析入口对应63万行证明的例子。适合关注形式化验证与AI辅助软件安全的人阅读。

---
来源：LearnMap · 学径（https://oplearnx.com）