CPython modeling project reports 418 bugs using AI-assisted proofs

Researchers David Andrews and Chao Zhang report that an AI-assisted project modeling CPython in Lean, a language for machine-checked proofs, generated 418 bug reports. They say about 55 findings can crash the interpreter or corrupt memory using ordinary Python code. Reports not already on CPython's tracker are being submitted to the project. The process copies implementation functions, tests them against Python and requires review by a separate AI agent before acceptance. The authors report 4,071 accepted functions out of 26,004, or 15.7%. They caution that valid proofs can describe an inaccurate model; most of CPython remains unmodeled, and multithreading is outside the project's current scope.