北京
Claude 给 123 个 OSS-Fuzz 库写出了可被机器检查的形式化证明。这件事的分量不在"AI 会写证明了"，而在它把一件原本昂贵到几乎没人做的事，压到了可以批量尝试的规模。
Anthropic 在 2026 年 10 月 22 日公布了与 Theorem 的合作结果：Claude 生成了形式化证明，证明 OSS-Fuzz 中 123 个库的 239 个 fuzz test 入口点，在任意小于 64 MB 的输入下都不会崩溃。
证明用 Rocq 写成，由证明助手的 kernel 检查，作用对象是编译后的 RISC-V 二进制，不是源码。总量约 1.8 亿行证明；一个典型证明超过 60 万行，对应的中位二进制是 1.8 万条指令。
流程的起点是项目本来就有的 fuzz test。这个测试被转成形式化命题：在 Theorem 的 Linux 进程模型和 RISC-V CPU 模型下，程序对限定范围内的所有输入都能正常结束，不出现内存错误，也不触发断言失败。Claude 负责写证明，Rocq 负责核对证明是否与规格一致。
过程中模型还找出并修掉了 bug，包括在 libexpat 中重新发现某个 CVE，以及一些跑了多年 fuzzing 都没抓到的故障。
但证明只证明被写下来的那条性质。
单线程。静态二进制。固定内存预算。RISC-V 与 Linux 被建模。输入上限 64 MB。出了这个范围——多线程、x86/ARM 上的 glibc、规格里没有点名的场景——保证不延伸过去。Anthropic 自己把话说得很直："formally verified"不等于"在任何真实用法下都没有 bug"。
这改变了围绕 AI 辅助验证的讨论。当可以在一个定义好的包络内证明"不崩溃"，通过测试就不再是天花板。昂贵的人力工作转移到别处：写对规格，决定什么进定理、什么留在外面，以及判断这些假设（操作系统模型、架构、输入上限）是否覆盖了团队真正接受的风险。
工具验证的是产物。定义"什么必须为真"的，仍然是工程。
对跑代码 agent 和安全流水线的人来说，落点很直接。团队采用模型生成的形式化证明后，检查清单不能只停在"kernel 过了吗"，还要问：
- 哪些性质被写成了命题；
- 它们建立在哪些前提之上；
- 业务上还有哪些东西必须在形式化包络之外单独处理。
少了这一层，证明就成了一枚盖在不完整合同上的章。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
