Claude generated about 180 million lines of formal proofs for 123 open-source libraries and found hundreds of bugs

Anthropic's Frontier Red Team and partner Theorem used Claude to mathematically verify existing software and produce formal proofs that the code is correct. According to The Decoder, the model wrote roughly 180 million lines of proof code in a few weeks, working from test programs in 123 open-source libraries. Along the way it found hundreds of bugs that conventional testing had missed. Formal verification proves that software behaves correctly in every possible case, but it has always been very expensive. A team of specialists needed 20 person-years to formally verify the small seL4 operating system kernel, so the method has mostly been used in extreme cases such as Airbus avionics software. Anthropic says it wants AI-assisted formal verification to become as routine as standard testing. The work addresses a central concern about AI-generated software: whether code written by a model can be trusted. If models can produce both code and machine-checkable evidence that it is correct, more of the review burden could shift from people to proofs. The Decoder notes that the approach still has strict practical limits, so the results show what is possible on these libraries rather than a general guarantee for any software.