Anthropic 在 Frontier Red Team 博客中介绍，与 Theoremlabs 合作使用 Claude 在数周内为一百多个真实开源库证明安全属性。Anthropic 称形式化验证过去只适用于小型代码库或需大量专家时间，AI 模型正开始改变这一状况。完整研究见 https://www.anthropic.com/research/formal-verification。
战略研判
基于公开信息若该方法可复现，形式化验证的适用范围可能从少量小规模代码库扩展到上百个真实开源库，降低对专家人力的依赖。
验证覆盖的具体安全属性与代码规模；与 Theoremlabs 的分工及结果能否被独立复现。
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