Anthropic与Theorem Labs发布大模型形式化软件验证报告

Anthropic与Theorem Labs发布报告，展示Claude模型通过生成1.8亿行Rocq证明代码，在123个开源软件库中发现并修复数百个漏洞，包括传统测试难以发现的长期隐藏漏洞。研究将验证推进到汇编指令层面，使形式化验证首次大规模应用于生产软件，但指出形式化验证无法证明整个软件绝对安全，且攻防成本不对等仍是挑战。