Anthropic Frontier Red Team 博客新文：用 Claude 大规模形式化验证软件
Anthropic 发布 Frontier Red Team 博客新文，介绍与 Theorem Labs 合作用 Claude 开展大规模形式化验证的成果：双方在数周内为上百个真实开源库证明了安全性质。形式化验证可以证明代码不存在某些 bug，但历史上通常只适用于小型代码库，或需要大量专家时间；Anthropic 称 AI 模型正开始改变这一点。完整研究见 https://www.anthropic.com/research/formal-verification。
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: https://www.anthropic.com/research/formal-verification