Anthropic revealed that Claude formally verified security properties across 123 open-source software libraries, uncovering hundreds of bugs.

Working with Theorem, Claude generated approximately 180 million lines of formal proofs covering 239 entry points, fixing discovered issues and mathematically proving crash-free execution under specified conditions. The research demonstrates how AI-assisted formal verification can uncover long-standing defects missed by conventional testing, although the proofs do not guarantee completely bug-free software.