# PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 40 references that are in the map.
- First posted on arXiv 11 Aug 2025.

## Builds on (most cited first, 7 of 7)

- [LiveCodeBench: Holistic and Contamination Free Evaluation of Large Language Models for Code](https://mlsanity.com/paper/2403.07974/) (2024)
- [DeepSeek-Coder-V2: Breaking the Barrier of Closed-Source Models in Code Intelligence](https://mlsanity.com/paper/2406.11931/) (2024)
- [Granite Code Models: A Family of Open Foundation Models for Code Intelligence](https://mlsanity.com/paper/2405.04324/) (2024)
- [Repair Is Nearly Generation: Multilingual Program Repair with LLMs](https://mlsanity.com/paper/2208.11640/) (2022)
- [What can Large Language Models Capture about Code Functional Equivalence?](https://mlsanity.com/paper/2408.11081/) (2024)
- [ESBMC-Python: A Bounded Model Checker for Python Programs](https://mlsanity.com/paper/2407.03472/) (2024)
- [Automatically Testing Functional Properties of Code Translation Models](https://mlsanity.com/paper/2309.12813/) (2023)

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

- [MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku](https://mlsanity.com/paper/2607.12711/) (2026)
- [Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits](https://mlsanity.com/paper/2512.02898/) (2025)
- [Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python](https://mlsanity.com/paper/2607.03951/) (2026)
- [T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework](https://mlsanity.com/paper/2608.14953/) (2026)

## Abstract (arXiv)

Python has become the dominant language for general-purpose programming, yet it lacks robust tools for formal verification. In contrast, programmers working in languages such as C benefit from mature model checkers, for example CBMC, which enable exhaustive symbolic reasoning and fault localisation. The inherent complexity of Python, coupled with the verbosity and low-level nature of existing transpilers (e.g., Cython), have historically limited the applicability of formal verification to Python programs. In this paper, we propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model checking and MaxSAT-based fault localisation in the generated C code. PyVeritas enables verification and bug localisation for Python code using existing model checking tools for C. Our empirical evaluation on two Python benchmarks demonstrates that LLM-based transpilation can achieve a high degree of accuracy, up to 80--90% for some LLMs, enabling effective development environment that supports assertion-based verification and interpretable fault diagnosis for small yet non-trivial Python programs.