Anthropic says Claude can automatically formally verify code security

Anthropic's Frontier Red Team, in collaboration with Theorem, had Claude formally verify the test programs of 123 open-source libraries in Google OSS-Fuzz, producing about 180 million lines of proof code within a few weeks. Claude did not write new code; instead, it translated crash tests into mathematical problems, analyzed the compiled machine code and generated proofs, which were then automatically checked by the independent verifier Rocq; according to Anthropic, this process requires almost no human review. During proof generation, Claude encountered hundreds of bugs and was permitted to fix them itself; for example, when verifying a widely used PDF reader, the number of security bugs it found within one week was comparable to the number typically reported for that software over an entire year, and it also found a logic error that had gone unnoticed for more than a decade. Anthropic acknowledges that formal verification does not equal being error-free: the proofs hold only for a specific processor architecture, single-threaded programs and inputs smaller than 64MB, and a single proof may consume hundreds of millions of tokens.