Anthropic用Claude实现大规模形式化软件验证

发生了什么

Anthropic与Theorem合作，使用Claude在RISC-V汇编代码级别对123个开源库证明了安全属性，据称是首次大规模将AI形式化验证应用于生产软件汇编级别。Claude在写证明过程中发现了多年未被检测到的bug。Anthropic正在发布部分证明供验证和复用。