AI rewrites Python's C guts to prove them, finds hundreds of hidden bugs

Researchers used OpenAI's Opus 5.5 AI to perform a massive formal verification project on CPython, the core C implementation that runs nearly all Python code. The AI system rewrote 613,318 lines of CPython's C source code into Lean, a language designed for writing machine-checked mathematical proofs. Each rewritten function was meticulously tested against the real Python interpreter on tens of thousands of inputs before any proof attempts began. So far, 4,071 functions have passed independent AI verification, creating 18,898 formally proven theorems and lemmas about Python's behavior.

This unprecedented formal verification effort uncovered 418 bugs in CPython that were previously unknown. About 55 of these bugs are serious—capable of crashing the Python interpreter or corrupting memory during normal operation. The work addresses Python's lack of a precise formal specification, where "Python" effectively means "whatever CPython does." This project demonstrates how AI-assisted formal methods can find subtle, dangerous bugs in critical software infrastructure that traditional testing misses.