Anthropic 用 Claude 数周内形式化验证百余个真实开源库的安全性

pzakin · x · 2026-10-24

Anthropic 在 Frontier Red Team 博客发布新研究：与 TheoremLabs 合作，用 Claude 在几周内对 100 多个真实开源库证明了安全性质。形式化验证可以证明代码不存在特定类别的 bug，但历史上只适用于小型代码库或需耗费大量专家时间，AI 模型正在改变这一点。转发者补充讨论了技术路线：团队选择直接在 RISC-V 二进制上验证而非高级语言——好处是语义建模更简单、无需信任编译器工具链，但代价是证明更冗长、agent 失去高层抽象，类似二进制分析与源码分析的差异；汇编级建模适合内存安全等性质，但通用功能正确性验证会更难。