Python
Python
ESBMC-Python is a frontend for ESBMC that enables formal verification of Python programs. It converts Python source code into ESBMC’s internal representation, allowing the engine to apply bounded model checking and SMT-based reasoning to detect bugs, assertion violations, and undefined behavior.
Architecture, pipeline stages, and how the frontend works.
Invoke ESBMC on Python files and interpret the results.
Supported language constructs, data structures, and standard library modules.
Known restrictions in the current version.
Generate pytest test cases automatically from counterexamples.
How the random module stub is modelled.