AI首次实现生产级软件汇编层形式化验证

Anthropic联合Theorem团队，基于Claude模型在RISC-V架构的汇编层级对123个主流开源库实施系统性形式化验证。实验设定在单线程静态二进制、固定内存预算、标准RISC-V CPU与Linux系统环境，且输入数据小于64MB的约束下，确认所有代码路径均未触发内存越界或断言失败。

覆盖超亿行代码，揭示多年潜伏漏洞

此次验证过程涵盖239个函数入口点，涉及约1.8亿行Rocq语言代码。值得注意的是，Claude在分析中识别出若干长期存在于核心组件中的隐蔽缺陷，这些漏洞即使经过数万亿次自动化测试仍未能暴露，凸显传统测试手段的局限性。

验证结果依赖可信基础假设

Anthropic强调，尽管成果具有里程碑意义，但形式化验证的有效性建立在对底层组件（如RISC-V指令集与Linux内核语义）正确性的信任之上。任何底层假设的偏差都可能影响最终结论的可靠性，因此该验证并非绝对无漏洞保证。