Formalizing CPython

Every report, with its script, is in the repository. Do this for your own project None of this is specific to Python. It works for anything with source code you can read and a working version you can run: another language, a library, a file format, a compiler. What made the difference for us: Pick one exact version and stick to it. Every copy points at specific lines in that version. List everything first. Count progress against the full list, so nothing gets skipped quietly. Copy the code, not the documentation. A copy written from the docs agrees with the docs, and the bugs are where the code and the docs disagree. Let user code misbehave. Model callbacks that throw errors or change things mid-operation. That's where the worst bugs were. Test before you prove. Proving things about a wrong copy wastes time. When something is false, keep the counterexample. Don't water the statement down until it becomes provable. Check proved statements against the real thing. A valid proof about a wrong copy is the most misleading result you can get. Count only what an independent reviewer accepts, and have that reviewer ask whether a broken version would pass. The instructions our agents worked from are in the repository and meant to be reused: AGENTS.md for the agents doing the work, REVIEW_PROMPT.md for the reviewers, and the full list of functions with their status in coverage/methods. Related work The closest project is julia-in-lean, which did this for the Julia language and directly inspired this one1. It modelled Julia's standard library in Lean, tested the models against Julia, recorded about 400 bugs and filed 75. Its finding that 128 of 130 quick proofs had quietly assumed away the hard case shaped our review rules. A recent paper models NVIDIA's PTX GPU instruction set in Lean to prove GPU kernels correct2, building on earlier formal work on PTX's memory model3. For Python specifically, λπ4 and a K framework semantics of Python 3.35 described the language mathematically; this project copies CPython's actual code instead. Similar efforts exist for JavaScript6,7 and WebAssembly8, and CompCert9 and seL410 remain the high bar for fully verified software. Comparing two implementations on the same inputs, the testing half of this project, goes back decades11,12. Where it stands The project started on 29 October 2026. 4,071 of the 26,004 functions worth checking (15.7%) have been copied, tested, proved and accepted by review. The Lean code is 613,318 lines in 1,539 files, containing 18,898 theorems and lemmas; 3,834 of the top-level properties are proved and 588 are proved false with a counterexample. Most of Python is still ahead, especially the large part of the standard library written in Python itself. Multithreading is out of scope for now. In these 57 files, every function copied so far has passed review. The 30 with the most accepted functions: Python/bytecodes.c310 Grammar/python.gram278 Lib/collections/__init__.py184 Lib/_pydecimal.py160 Lib/_pydatetime.py150 Modules/_struct.c122 Objects/longobject.c119 Objects/listobject.c114 Objects/memoryobject.c107 Objects/dictobject.c104 Objects/bytesobject.c100 Objects/exceptions.c97 Objects/unicodeobject.c94 Objects/bytearrayobject.c93 Modules/arraymodule.c84 Lib/_collections_abc.py81 Modules/_operator.c73 Modules/itertoolsmodule.c72 Modules/_collectionsmodule.c64 Python/codecs.c61 Lib/operator.py59 Lib/_pyio.py58 Objects/typeobject.c57 Lib/weakref.py54 Objects/genobject.c46 Lib/urllib/parse.py46 Parser/action_helpers.c43 Modules/_zoneinfo.c43 Objects/floatobject.c38 Objects/tupleobject.c37 The project is open, and help is welcome. Most of CPython is still unmodelled: pick a file whose functions are still marked todo in coverage/methods, follow AGENTS.md, and send a pull request. Independent reviews of existing work count as much as new models. See CONTRIBUTING.md. Cite @misc{andrews2026formalizing, author = {Andrews, David and Zhang, Chao}, title = {Formalizing {CPython}: A Lean Model of {CPython} 3.15.2}, year = {2026}, howpublished = {\url{https://broyojo.com/python-formalization/}}, note = {Code: \url{https://github.com/Broyojo/python-formalization}} } References M. Cranmer. Formalizing Julia in Lean (and finding 400+ bugs in Base). Julia Discourse, 2026. Code: MilesCranmer/julia-in-lean. L. Koska, T. Koska, B. Koska. Formalizing PTX in Lean to Prove GPU Kernel Correctness. arXiv:2611.04447, 2026. D. Lustig, S. Sahasrabuddhe, O. Giroux. A Formal Analysis of the NVIDIA PTX Memory Consistency Model. ASPLOS 2019. J. G. Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, S. Krishnamurthi. Python: The Full Monty. A Tested Semantics for the Python Programming Language. OOPSLA 2013. D. Guth. A Formal Semantics of Python 3.3. M.S. thesis, University of Illinois at Urbana-Champaign, 2013. Code: runtimeverification/python-semantics. M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith. A Trusted Mechanised JavaScript Specification. POPL 2014. D. Park, A. Ştefănescu, G. Roşu. KJS: A Complete Formal Semantics of JavaScript. PLDI 2015. C. Watt. Mechanising and Verifying the WebAssembly Specification. CPP 2018. X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 2009. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, et al. seL4: Formal Verification of an OS Kernel. SOSP 2009. W. M. McKeeman. Differential Testing for Software. Digital Technical Journal 10(1):100–107, 1998. X. Yang, Y. Chen, E. Eide, J. Regehr. Finding and Understanding Bugs in C Compilers. PLDI 2011.