Anthropic 与 Theorem Labs 用 Claude 大规模验证开源软件安全属性

AI 导读

Anthropic 与 Theorem Labs 合作，使用 Claude 在数周内为超过 100 个真实世界开源库证明安全属性。Anthropic 表示，传统形式化验证过去主要适用于小型代码库或需要大量专家时间，AI 模型正在改变这一限制。研究全文发布于 anthropic.com/research/forma…。

正文 · AI 翻译

我们 Frontier 红队博客的最新文章：如何使用 Claude 对大规模软件进行形式化验证。

形式化验证可以证明代码不存在某些类型的错误，但过去它只适用于小型代码库（或者需要投入大量专家时间）。

然而，借助 AI 模型，这一情况开始发生变化。我们与 @theoremlabs 合作，在数周时间内使用 Claude 为一百多个现实世界中的开源库证明了安全属性。

在此阅读全文我们的研究：anthropic.com/research/forma…

来源：AnthropicAI · x.com