【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语义等可信组件的假设。

原文链接：https://www.anthropic.com/research/formal-verification

声明：本站所有文章，如无特殊说明或标注，均为本站原创发布。任何个人或组织，在未征得本站同意时，禁止复制、盗用、采集、发布本站内容到任何网站、书籍等各类媒体平台。如若本站内容侵犯了原著者的合法权益，可联系我们进行处理。