Anthropic称Claude为123个开源库生成汇编级形式化证明

Anthropic与形式化验证公司Theorem合作，将开源项目现有的模糊测试转换为数学规范，再由Claude编写证明、交给Rocq证明检查器核验。Anthropic称，团队在数周内完成了123个开源库、239个测试入口的证明，证明代码合计约1.8亿行。其核心结论是：对小于64 MB的输入，在设定的Linux响应和内存布局下，经过修补并编译为特定RISC-V程序的测试入口不会因内存安全错误或断言失败而崩溃。Claude在编写证明时也发现并修补了此前测试未发现的问题，包括需罕见输入才能触发的越界读写。与反复抽样的模糊测试相比，形式化证明能覆盖所定义范围内的所有输入；但结论取决于规范、机器模型和检查器是否准确。目前的主要证明针对单线程、静态链接等特定运行条件，也未覆盖每个库的全部代码。Anthropic已公开部分证明，供外界复核和复用。这项研究展示了AI降低形式化验证工作量的可能性，尚不能据此宣称123个库已“无漏洞”。