Anthropic 在 Frontier Red Team 博客发布研究,介绍用 Claude 大规模进行形式化验证的方法。与 Theorem Labs 合作,团队在数周内为超过一百个真实开源库证明了安全属性,突破了形式化验证过去仅适用于小型代码库或需大量专家人工的限制。全文见 https://www.anthropic.com/research/formal-verification。
同一件事,精选收录的是《Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明》
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