TLDR: PYVERITAS is a novel framework that addresses the lack of robust formal verification tools for Python. It leverages Large Language Models (LLMs) to translate Python code into C, then uses mature C verification tools like CBMC for correctness checks and MaxSAT-based fault localization to identify bugs, mapping them back to the original Python source. This approach provides a practical solution for verifying Python programs and diagnosing faults.
Python has become a cornerstone of modern programming, widely adopted for its versatility and ease of use. However, despite its popularity, Python has historically lacked robust tools for formal verification—a critical process for ensuring software correctness and reliability. In contrast, languages like C benefit from mature verification tools, such as CBMC, which allow for exhaustive symbolic reasoning and precise fault identification.
This gap in Python’s ecosystem has made it challenging to apply formal verification techniques, largely due to Python’s dynamic nature and the complexity of existing transpilers that convert Python to C. These traditional transpilers often generate thousands of lines of low-level C code, making symbolic analysis impractical.
Introducing PYVERITAS: A Novel Approach to Python Verification
A new framework called PYVERITAS aims to bridge this gap by leveraging the power of Large Language Models (LLMs). Proposed by researchers Pedro Orvalho and Marta Kwiatkowska from the University of Oxford, PYVERITAS offers a novel solution for verifying Python programs and localizing bugs. The core idea is to use LLMs for high-level transpilation, converting Python code into C, and then applying well-established C verification tools to the generated C code.
The PYVERITAS pipeline operates in several key steps:
The PYVERITAS Pipeline
First, an LLM is used to transpile the Python program, along with its textual description and specifications (assertions), into semantically equivalent C code. This step is crucial as it transforms the Python program into a format that can be analyzed by existing, mature C verification tools.
Next, the generated C code is put through a C interpreter. This step acts as a sanity check; if the C code fails to compile or doesn’t satisfy the assertions that the original Python code does, a new translation is requested from the LLM. This iterative process helps ensure the quality of the transpiled code.
Once a satisfactory C candidate is obtained, it undergoes verification using a bounded model checker for C, specifically CBMC. If this verification succeeds, PYVERITAS concludes that the original Python program meets its specified requirements.
However, if verification fails, indicating a bug, PYVERITAS employs MaxSAT-based fault localization using a tool called CFAULTS. This technique analyzes the C code to pinpoint the minimum set of faulty statements responsible for the failure.
Finally, the identified fault locations in the C code are mapped back to their corresponding statements in the original Python program. This crucial step provides interpretable diagnostic feedback directly to the Python developer, making it easier to understand and fix the root cause of the bug.
Also Read:
- Agentic AI Solves All Constraint Programming Benchmarks
- Enhancing LLM Code Generation with Klear-CodeTest’s Advanced Test Case Synthesis
Experimental Insights and Model Performance
The researchers evaluated PYVERITAS on two widely used Python benchmarks, LIVE CODE BENCH and REFACTORY, using various LLMs including QWEN 2.5-CODER, DEEP SEEK-CODER-V2, GRANITE CODE, and LLAMA 3.2. The results were insightful:
- QWEN 2.5-CODER demonstrated the highest reliability in transpiling Python to semantically faithful C code, achieving verification success rates of over 80% in many cases. This indicates its strong ability to produce verifiable C translations.
- The experiments confirmed that MaxSAT-based fault localization, when applied to LLM-transpiled C code, can effectively identify faults injected into the original Python source. This means that even if a bug originates in Python, it can be found and localized through its C translation.
- An interesting observation was the varying behavior of different LLMs. Reasoning-oriented models like QWEN 2.5-CODER and DEEP SEEK-CODER-V2 often inadvertently “fixed” bugs during transpilation by leveraging natural language descriptions and assertions to guide their output. In contrast, models like GRANITE CODE prioritized structural fidelity, preserving the original faulty semantics, which is essential for accurate fault localization. This highlights the importance of choosing the right LLM based on the specific verification task.
In conclusion, PYVERITAS offers a practical and effective interim solution for formal verification and fault diagnosis in Python programs. By leveraging the evolving capabilities of LLMs for code transpilation and integrating with mature C verification tools, it provides a powerful approach to ensuring the correctness of Python code, bridging a significant gap until native Python model checkers become fully mature. For more details, you can refer to the full research paper: PYVERITAS: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C.
