Claude Found Hundreds of Bugs by Proving Other People's Code Correct

Claude is Anthropic's AI model. To check code written by other people, Anthropic used Claude to verify the correctness of about 123 open source libraries in OSS-Fuzz, Google's ongoing fuzz-testing project for open source software. Working with its formal-verification partners at Theorem, Anthropic generated about 180 million lines of formal verification proofs, written in the Rocq proof assistant language. Each proof was checked independently with a separate tool. Along the way, Claude found and fixed hundreds of long-standing bugs. These proofs are not universal. They hold for a single-threaded runtime, the RISC-V instruction set architecture, and files under 64 MB.

If you are someone who uses AI agents to work on real code, this is more interesting than another benchmark score. Checking that code is correct is often the bottleneck in the workflow. Generating code in the first place is not the hard part anymore. In this case, Claude had to verify code it did not write itself. This does not replace code review, because the results only hold under certain constraints. But we are moving toward a future where AI agents do more than suggest autocompletions. They generate code and check it too.