# ESBMC-Python: A Bounded Model Checker for Python Programs

arXiv: https://arxiv.org/abs/2407.03472 · HTML: https://mlsanity.com/paper/2407.03472/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 Jul 2024.

## Built on by (most cited first, 4 of 4)

- [Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview](https://mlsanity.com/paper/2503.10784/) (2025)
- [Joint Verification and Refinement of Language Models for Safety-Constrained Planning](https://mlsanity.com/paper/2410.14865/) (2024)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C](https://mlsanity.com/paper/2508.08171/) (2025)

## Abstract (arXiv)

This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.