Anthropic's Claude automatically proves existing code correctness using mathematical verification

Anthropic's Frontier Red Team, partnering with Theorem, used Claude to mathematically prove the correctness of existing software by translating crash tests into mathematical problems and analyzing compiled machine code. This process generated roughly 180 million lines of mathematical proof code from 123 open-source libraries in Google's OSS-Fuzz project. The independent verification program Rocq checks these proofs, and Anthropic claims the process requires almost no human reviewers. Claude found bugs missed by years of testing, such as security bugs in a PDF reader equivalent to a year's worth, and a decade-old logical error. However, the proofs are limited to strict conditions: a specific processor architecture, single-threaded programs, and inputs under 64 MB.