【Anthropic用Claude形式化验证123个开源库，发现潜伏多年漏洞】

【Anthropic用Claude形式化验证123个开源库，发现潜伏多年漏洞】报道，10月23日，据Anthropic研究博客，Anthropic与Theorem合作，使用Claude在RISC-V汇编层面对123个开源库进行形式化验证，证明其在特定假设下（单线程静态二进制、固定内存预算、RISC-V CPU及Linux系统、输入小于64MB）对任意输入均不会出现内存安全错误或断言失败，相关证明涵盖239个入口点、约1.8亿行Rocq代码。Anthropic称，这是在汇编层面对生产软件进行AI形式化验证的首次大规模尝试。过程中Claude还发现并修补了潜伏多年、即便经历数万亿次测试运行也未被检出的漏洞。Anthropic同时提示，形式化验证不等于无漏洞，其结论依赖于对RISC-V及Linux语义等可信组件的假设。