A developer had Claude Opus 5.5 formalize CPython in Lean, in 613,318 lines

The developer broyojo42 says they had Claude Opus 5.5 write a formalization of CPython in Lean: 613,318 lines that copy Python's internals line by line, tested against the real interpreter and checked by Lean. They say that along the way the model found real bugs in Python, including crashes from plain Python code.

The post is the author's own account; the post had 2,066 points on X by November 10. Astral's Charlie Marsh shared it.