Anthropic 在 Frontier Red Team 博客发布新研究，介绍用 Claude 对软件做大规模形式化验证。形式化验证可证明代码不存在某些 bug，但过去只适用于小型代码库或需要大量专家时间；Anthropic 与 theoremlabs 合作，用 Claude 在几周内证明了超过一百个真实开源库的安全属性。
原文给出用 Claude 在数周内形式化验证上百个开源库的做法和结果，读者可了解 AI 如何降低形式化验证的门槛。
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
来源：Anthropic · x.com