Anthropic Used Claude to Prove Security Properties in 100-Plus Libraries

Proofs, at the scale of real libraries.

Anthropic’s Frontier Red Team has a new blog post on using Claude to formally verify software at large scale.

Formal verification can prove that code is free of certain bugs, Anthropic writes, but historically it has only been feasible for small codebases, or it required a lot of expert time. With AI models, it says, this is beginning to change.

In collaboration with @theoremlabs, Anthropic used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks. The full research is on the Frontier Red Team blog.