我们 Frontier Red Team 博客上新了：使用 Claude 对大规模软件进行正式验证。
正式验证可以证明代码没有某些错误，但历史上只有针对小型代码库时才可行（或者需要大量专家时间）。
然而，随着人工智能模型的兴起，这种情况正开始改变。与 @theoremlabs 合作，我们利用 Claude 在几周时间内对一百多个真实世界的开源库的安全性特性进行了验证。
在此处完整阅读我们的研究：https://www.anthropic.com/research/formal-verification