AI能否帮助网络防御方应对攻击，Anthropic报告评估Claude的RISC-V形式化验证

Anthropic与Theorem Labs发布报告，称Claude可将形式化验证推进到基于RISC-V指令集的汇编层。Claude针对123个开源软件库的239个程序入口生成约1.8亿行Rocq证明代码，并发现、修复数百个Bug，包括一些历经数万亿次测试仍未发现的漏洞。该验证只在特定假设、约束和范围内成立，并不等同于软件绝对安全，第三方依赖和生产部署仍是挑战。