Anthropic says Claude has written computer-checked mathematical proofs that 239 entry points across 123 widely used open-source libraries cannot crash on any input up to 64 MB. The work, done with the verification company Theorem, applies formal verification (proving that software behaves as specified, rather than just testing it) to each library’s compiled machine code. Anthropic calls it the first large-scale effort to use AI this way on production software. It took a few weeks and produced about 180 million lines of proof.
Along the way Claude found bugs that years of testing had missed, including an out-of-bounds write in a decompressor that only a rare input of roughly 20 MB could trigger. It patched them, then proved the fixed code safe. Theorem is offering to run the same process for other open-source projects through a service called OSS Verify.
Why it matters: proofs like these used to take experts years, so they were kept for the most critical code. If AI makes them cheap, more of the software everyone relies on could carry guarantees rather than hopes. Anthropic is clear about the limits: the proofs assume a specific RISC-V and Linux setup, and “formally verified” does not mean “bug-free”. Read Anthropic’s write-up.