Anthropic联手Theorem Claude首证123库RISC-V汇编零崩溃

2026年10月22日，Anthropic与Theorem联合发布研究，Claude针对Google OSS-Fuzz收录的123个真实开源库，生成约1.8亿行Rocq证明代码，在RISC-V汇编层面数学证明239个入口点“任意输入不崩溃”。

事实还原

研究显示，Claude在单线程静态二进制、固定内存预算的RISC-V CPU与Linux OS假设下，证明程序始终正常退出，不触发内存安全错误或断言失败，输入上限为64MB。该过程同时发现若干经万亿次模糊测试仍未触发的隐藏漏洞。研究发布部分证明代码及RISC-V与OS语义，Theorem同时提供同一流程供其他开源项目使用，并发布Claude技能帮助开发者起步。

机制拆解

形式化验证首先需将代码转化为数学模型，再证明其始终遵循既定安全规则。若证明失败，则指向可能违反规则的漏洞，消除原因后重复过程，最终获得无违规漏洞的证明。传统上，证明代码量远超原代码，需高度专业技能，例如seL4内核实现仅用2人年，验证却耗费20人年。此次Claude自主生成证明，将这一过程推向可量产自动化流水线。

产业影响

此举将形式化验证从仅限任务关键应用（如空客航电代码）扩展至更多真实开源库。证明可复用与修改的潜力，有望摊薄后续代码库的验证成本。Theorem的管道服务与技能发布，为开发者提供直接入口。模型能力提升下，形式化验证有望成为安全软件开发的常规组成部分。

战略判断

（分析而非事实）该工作同时考验模型长程推理、代码理解与逻辑证明能力，与现有代码执行及复杂推理量化评估形成镜像。实验室分数之外，AI的真实工程守约能力正以可验证方式浮现。若模型持续改进，证明成本下降将加速安全保障标准化，但全面消除所有可能漏洞仍需进一步探索。