Anthropic 用 Claude 为百个开源库做汇编级形式化安全验证

Anthropic 前沿红队在官方博客发布与 Theorem Labs 合作的研究：用 Claude 在数周内为 100 多个真实开源软件库生成 RISC-V 汇编代码层面的形式化安全证明，证明这些代码不存在特定类别的常见安全漏洞。研究方称这是首次用 AI 在汇编级对生产软件实现大规模形式化验证，相关工作还发现了潜伏多年的 bug。

已确认

• 发布方为 Anthropic Frontier Red Team 博客，合作方为 Theorem Labs，发布时间 10 月 23 日。
• 验证对象是 100 多个（m2 转述为 123 个）真实开源软件库，验证层级为 RISC-V 汇编代码，时间尺度为"几周内"。
• 形式化验证的范畴是数学化地证明代码不存在特定类别 bug；据 @chrisrohlf 转述，过程中还揪出了潜伏多年的 bug。

为什么重要

• 形式化验证过去只适用于小规模、高成本场景（如航天、密码学关键代码），难以扩展到普通生产软件。多位发帖者（@chrisrohlf、@MilesBrundage 转述等）认为，LLM 让这一技术首次具备大规模实用价值，可能显著降低安全审计与漏洞证明的门槛。
• 在汇编层而非源码层验证，意味着证明结果更贴近实际运行的二进制行为，绕过了编译器差异与源码不可得的问题。
• @bookwormengr 强调该工作展示了 Claude 在"超过一定规模的代码库"上做形式化验证的能力，是 AI 辅助软件工程可靠性的一个标志性案例。

2026-10-23 ~ 2026-10-23 · 6 条相关

• 【源头】Anthropic 用 Claude 为 100+ 开源库写下汇编级安全形式化证明 — AnthropicAI · 2026-10-23

另有 5 条近重复转述:chrisrohlf · bookwormengr · inductionheads · Miles_Brundage · PMinervini