Claude 形式化验证研究能否帮助防御方应对网络攻击？

Anthropic 与 Theorem Labs 发布研究报告，利用 Claude 在汇编指令层面开展大规模形式化软件验证。研究覆盖123个开源软件库中的239个程序入口，生成约1.8亿行 Rocq 证明代码，并发现和修复数百个 Bug，验证以 RISC-V 指令集为基础。