Anthropic 的 Claude 实现自动代码安全证明

Anthropic 使用 Claude 对现有代码进行数学证明，验证其安全性，生成约1.8亿行证明代码，覆盖123个开源库。该过程由独立工具Rocq验证，几乎无需人工审查。Claude在验证中发现数百个隐藏漏洞，包括一个十年未被发现的逻辑错误。验证仅限特定硬件、单线程和64MB以内输入，单次证明消耗数亿token。项目目标扩展至glibc、OpenSSL等关键基础设施。