Anthropic 用 Claude 在数周内形式化验证上百个开源库的安全性质
AI 导读
Anthropic 在 Frontier Red Team 博客发布新研究，与 Theorem Labs 合作，用 Claude 在数周内对上百个真实开源库证明了安全性质。形式化验证能证明代码不含特定类别的 bug，但过去只对小代码库可行或需要大量专家时间；Anthropic 称随着 AI 模型出现，这种情况开始改变。Logan Graham 称这项工作预示的团队方向是先找出并修复所有 bug，进而重写软件基础使其从一开始就不含 bug。研究全文见 https://www.anthropic.com/research/formal-verification
正文 · 原文
step 1: find and fix all the bugs
step 2: rewrite the foundations of software to not have bugs in the first place
Proud of this work from @keenlooks and @theoremlabs and team. This is a glimpse of the direction we're going.
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在 X 查看被引用的帖子