engineering / UCL / 2025
Formal verification of Python standard-library code
Verifying CPython standard-library functions by symbolic execution, and testing where the method breaks.
CrossHair / Z3
Question
Can symbolic execution verify contracts for Python standard-library functions, and expose a deliberately seeded failure?
Why it matters
A verification result is useful only within the contracts and paths examined. Testing a known counterexample checks whether the method can expose a failure.
Method and findings
- Verified CPython standard-library functions by symbolic execution: 32 of 33 contracts verified.
- Seeded a deliberate counterexample to test where the method fails, rather than reporting only the cases where it succeeds.
Limitations
The result concerns the 33 contracts examined. It is not a proof of correctness for the Python standard library as a whole.
Next questions
Which additional contracts and execution paths can be analyzed within practical solver limits?
Sources
Project details supplied by the author. A public technical report is not linked here.