核心信息

Anthropic 前沿红队发布研究：与 Theorem Labs 合作，用 Claude 在数周内对 100 多个真实开源库的安全属性完成形式化验证。

要点

  • 形式化验证能证明代码不含某些缺陷，但过去只适用于小型代码库，或需要大量专家投入。
  • Anthropic 表示 AI 模型正在改变这一可行性限制。
  • 该工作在数周内覆盖了 100 多个真实开源库。
  • 完整研究发布在前沿红队博客上。