Pith. sign in

REVIEW 3 major objections 5 minor 3 cited by

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

T0 review · 3 major / 5 minor · reviewed 2026-08-05 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that LLM-based Python-to-C transpilation can be faithful enough that bounded model checking of the C code gives a valid correctness verdict on the original Python program.

desk verdict Useful idea and an honest empirical study, but the central soundness claim is not backed: LLM transpilation can silently fix bugs, so a C verdict is not a Python verdict. read the letter →

arxiv 2508.08171 v1 pith:VRZ5PKOR submitted 2025-08-11 cs.SE cs.AI

Pedro Orvalho , Marta Kwiatkowska This is my paper
classification cs.SEcs.AI
keywords LLMtranspilationPythonverificationboundedmodelcheckingCBMCMaxSATfaultlocalisationsemanticequivalencecodetranslationassertion-based
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

PyVeritas claims that a large language model can translate small but non-trivial Python programs into C closely enough that a mature C bounded model checker (CBMC) can decide whether the original Python program satisfies its assertions. If the C translation verifies, the paper treats the Python program as verified; if it fails, a MaxSAT-based fault localiser finds a minimal set of faulty C statements, and the LLM maps those back to Python source lines. On two Python benchmarks the paper reports verification success up to 92% for the best coding-focused model, and fault-localisation accuracy up to about 52% for a model that preserves faulty semantics. This matters because Python lacks a robust native model checker, while C has mature symbolic verification and fault-localisation infrastructure. The price is a semantic-equivalence assumption: a CBMC verdict is only a verdict on the original Python if the translation is faithful.

What carries the argument

The load-bearing mechanism is the two-stage bridge: LLM prompt-based transpilation from Python to C, followed by bounded model checking of the generated C. The verification step is CBMC, which symbolically explores C executions up to a bound and checks assertions; the fault-localisation step encodes the C program's trace formula as a MaxSAT problem, with soft clauses over statement-healthiness variables, to return a minimum set of faulty statements; a final LLM query maps those C lines back to Python lines. The paper's own example shows the pipeline locating a duplicated assignment in a 9-line Python function after checking a C translation.

What would settle it

Take a program PyVeritas reports as verified, then run the original Python on a much larger random or exhaustive input set than the provided tests, or check it with an independent Python verifier; a single assertion violation in Python on an input where the C translation verified would show the translation was not equivalent and the verdict did not transfer.

Watch

Extended reading notes

Core claim

The paper's central claim is that LLM-based transpilation is a viable bridge between Python and C verification infrastructure. PyVeritas prompts an LLM for C from the Python program, a description, and assertions; keeps only translations that compile and pass the assertions on the given inputs; then runs CBMC. A CBMC success is taken as a verdict on the original Python, while a CBMC failure triggers CFAULTS, which computes a minimal faulty-statement diagnosis on the C code, and an LLM query maps it back to Python. The empirical result is model-dependent: the best coding-specialised model reached 83.7% verification on LiveCodeBench and 92.0% on Refactory, whereas the model that preserved bugg

Load-bearing premise

The load-bearing premise is that the LLM's C code is semantically equivalent to the original Python program, so a CBMC verdict on the C transfers to the Python; the only direct checks are running both on the provided inputs and assertions and, in the evaluation, human labelling of equivalence.

Editorial extensions

If this is right

  • Python programs in the supported class can be checked with mature C tooling today, without waiting for a native Python model checker.
  • A CBMC success on the translation is treated as a formal correctness verdict on the Python source, so assertions become machine-checked specifications rather than test-only guards.
  • Fault localisation gives developers a minimal set of suspect statements in the original Python, via the back-mapping step, when the translation preserves the faulty semantics.
  • Model choice matters: models that preserve structure localise bugs better, while reasoning-oriented models often repair the bug during translation and yield higher verification rates but lower localisation rates.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper leaves open that 'verified' is conditional on LLM semantic fidelity; a formal check of Python/C equivalence, or a certified transpiler, would upgrade this from empirical to sound.
  • An untested extension is applying the same pipeline to real, multi-statement faults; the injected single-statement mutations used here are easier to localise, so real-world accuracy may be lower.
  • If larger or reasoning models continue to repair bugs during translation, the framework's verification and localisation goals pull in opposite directions; a prompt that forbids semantic repair could recover localisation power.
  • Because only test inputs and human labels validate equivalence, feeding PyVeritas outputs into property-based differential testing—running Python and the C translation on random inputs—would be a cheap, immediate way to catch unfaithful translations.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes PyVeritas, a pipeline that uses an LLM to transpile small Python programs to C, filters the generated C via a C interpreter, then applies CBMC for bounded-model-checking verification and CFAULTS for MaxSAT-based fault localization. The localised C faults are mapped back to Python statements via a second LLM query. The authors evaluate four open LLMs (Qwen 2.5-Coder 32B, DeepSeek-Coder-V2 16B, Granite Code 8B, Llama 3.2 3B) on two benchmarks (Refactory and a 125-program subset of LiveCodeBench), reporting verification-success rates up to 83.7% on LiveCodeBench and 92.0% on Refactory, and fault-localization success rates between 7.6% and 52.4% depending on model, benchmark, and injected fault type (WBO or ADC). The paper's central claim is that CBMC success on the LLM-generated C program is sufficient to conclude that the original Python program satisfies the given assertions.

Significance. If the central claim were sound, this would be a practically useful bridge: it would let mature C model checkers and MaxSAT fault localizers be applied to Python without awaiting a native Python model checker. The paper also contains a valuable empirical measurement: LLM transpilation of Python to C is nontrivial but, for the best model, often successful; and the observation that reasoning-oriented LLMs often inadvertently repair the injected fault during transpilation, while fidelity-oriented models preserve it, is interesting for tool design. However, the paper's main inference--from a CBMC verdict on the transpiled C code to a verdict on the original Python--is not formally established and is in fact contradicted by the paper's own fault-localization data. The positive results are partly based on manual expert labeling of semantic equivalence (Section 5), which is an evaluation step, not a runtime safeguard. The paper therefore cannot support the claim that PyVeritas verifies Python programs; it can support the weaker, still interesting claim that it verifies the LLM-transpiled C code and that, in the majority of inspected cases, that C code is semantically equivalent to the Pyt

major comments (3)
  1. [Section 4, 'Verification via CBMC'] The inference 'CBMC succeeds on C, therefore the original Python satisfies S' is unsound. The C-interpreter filter only discards a candidate when C fails an assertion that Python satisfies; it cannot reject a C program that changes Python semantics while still passing the assertions in S. This is not a hypothetical concern: Tables 2 and 3 show that the same LLM that produces the verified C code frequently 'fixes' the injected fault during transpilation. For example, in Table 3, Qwen 2.5-Coder produces 'Transpiled Fixed Code' in 62.6% (WBO) and 81.4% (ADC) of LiveCodeBench cases. Such outputs would pass the interpreter, pass CBMC, and be reported as 'Python verified' for a Python program that itself fails the assertion. The manual semantic-equivalence labeling used in Table 1 is an evaluation procedure, not a component of the tool, so it does not prevent these false positives. The paper s
  2. [Section 5, Table 1 and Abstract] The headline claim of 'up to 80--90%' verification accuracy is not supported as a property of the PyVeritas tool. Table 1 reports the proportion of C programs that were both CBMC-verified and manually judged semantically equivalent. Without the manual equivalence filter, the automated pipeline would also count C programs that are not semantically equivalent but happen to pass the given assertions. The paper does not report the CBMC-only success rate, so the reader cannot tell how much of the reported accuracy depends on human inspection. This is load-bearing for the central claim; please report the automated verification rate and the human-equivalence rate separately, and avoid stating that PyVeritas 'formally verifies Python code' when the formal verdict is only on C and equivalence is not checked at runtime.
  3. [Section 5, Fault localization experiments] The fault-localization evaluation measures what happens when the LLM preserves the bug, but it does not measure the more serious failure mode: when the LLM repairs the bug and the pipeline returns a false 'verified' verdict for a buggy Python program. The 'Transpiled Fixed Code' percentages in Tables 2 and 3 (e.g., 81.4% for Qwen on ADC in LiveCodeBench) imply that, for buggy Python inputs, PyVeritas would frequently terminate with a verification-success output rather than a fault report. To assess the tool's actual behavior, please run the full pipeline on the mutated programs and report the fraction that are incorrectly declared verified. Without this number, the paper cannot support the claim that PyVeritas provides 'interpretable fault diagnosis' for Python programs in general.
minor comments (5)
  1. [Section 4, Figure 1] The text says the C interpreter discards candidates when 'C fails to satisfy the assertions that P satisfies,' but the pipeline figure is not included in the text and the control-flow for the case 'C passes and P fails' is not described. Please clarify which branch is taken and what the user is told when the C program passes but the Python program itself fails the assertion on the test inputs.
  2. [Section 5, baseline] The statement that ESBMC-Python 'was unable to verify any of the programs' is presented without detailed error counts or a timeout report. Since this is a central motivation, a short table or a precise statement of the unsupported constructs would strengthen the comparison.
  3. [Section 5, experiment reporting] The 'Verification success rates' in Table 1 combine CBMC verification with manual semantic-equivalence labeling. The methodology paragraph correctly describes this, but the table title and the surrounding text call it 'verification success,' which is ambiguous. Please rename the column to something like 'CBMC-verified and manually equivalent.'
  4. [Appendix C] The DeepSeek example in Appendix C shows the LLM introducing a new semantic error while fixing the original bug. This is a useful illustration of semantic drift, but it also shows that the mapping stage can report a Python line that is not actually the injected fault. Please add a sentence noting that this can also happen in the fault-localization experiments, not only in the illustrative example.
  5. [General] The paper repeatedly uses 'semantically equivalent' without defining what is preserved (e.g., partial equivalence on terminating paths, assertion behavior, resource use). A precise definition would help, especially because the C program may have undefined behavior or different integer semantics (e.g., signed overflow, modulo behavior) than Python.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the central claims are measured empirically against external benchmarks and do not reduce to their own inputs.

full rationale

PyVeritas is an empirical systems paper. Its main claim—that LLM-based Python-to-C transpilation can be semantically faithful enough to enable verification and fault localization—is evaluated directly on external benchmarks (LiveCodeBench and Refactory) with human-labeled semantic equivalence and CBMC verdicts. None of the reported success percentages is fitted from the data it is used to predict; there are no learned parameters or calibration steps that would make a prediction equal to its input by construction. The use of CFAULTS (Orvalho, Janota, and Manquinho 2024) is a citation to the authors' prior tool, but CFAULTS is applied to C code as an external, published component, not invoked as an unverified justification for the paper's central claim. The manuscript's own limitation—that CBMC success on the transpiled C program is transferred to the Python program without an automated semantic-equivalence check—is a real soundness risk, especially given the high 'Transpiled Fixed Code' rates in Tables 2 and 3, but it is a correctness/validation gap, not a circularity of the kind where a result is equivalent to its inputs by definition or by a self-citation chain. Therefore the circularity score is 0.

Assumptions & free parameters 3 free parameters · 5 assumptions · 0 invented entities

The load-bearing premises are the unverified semantic equivalence between the Python source and the LLM-generated C code, the trust placed in CBMC and CFAULTS as external tools, and the reliance on human labeling to measure equivalence. No new speculative entities are introduced.

free parameters (3)
  • LLM retry limit = 5
    The pipeline requests a new C candidate up to five times when the interpreter finds a mismatch; this value is chosen by hand and directly affects verification success rates.
  • Per-run time limit = 10 minutes
    A wall-clock budget of 10 minutes is imposed on the whole pipeline, including CBMC; this choice affects which programs can be verified.
  • LLM sampling temperature = 0
    Temperature is set to 0 for all models to aim for deterministic output; this removes sampling randomness but does not eliminate model variability across runs.
assumptions (5)
  • domain assumption The LLM-generated C code is semantically equivalent to the input Python program, at least with respect to the assertions S.
    Invoked in Section 4 under 'Verification via CBMC', where a CBMC success on C leads to the conclusion that the Python program satisfies S. The tool only checks equivalence on the supplied test inputs, not in general.
  • standard math CBMC soundly reflects C program behavior within the given bounds.
    PyVeritas relies on CBMC as a trusted third-party bounded model checker; this is a standard assumption for using an existing verification tool.
  • domain assumption CFAULTS correctly identifies minimal faulty statements in C programs via MaxSAT.
    Used for fault localization in Section 4; the tool was developed by the first author in prior work and is not independently validated within this paper.
  • domain assumption The provided assertions S are the correct formal specification of intended behavior.
    The pipeline treats S as ground truth and uses it both to guide the LLM and to verify the C code. The paper notes in Section 4 that descriptions and assertions may be inconsistent with buggy code.
  • domain assumption Human expert labeling of semantic equivalence is accurate.
    In Section 5, verification success rates are based on manual inspection by experts to determine whether transpiled C code is semantically equivalent to the original Python. This judgment is subjective and not automated.

how reviews work

0 comments
Cite this review

Pith. "Pith review of PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C." pith.science (2026). https://pith.science/paper/VRZ5PKOR

@misc{pith2026250808171,
  author       = {Pith},
  title        = {Pith review of: PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VRZ5PKOR}},
  note         = {Machine review of arXiv:2508.08171}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2508.08171 by the authors.

Figure 1
Figure 1. PYVERITAS’s pipeline for Python verification and bug localisation. Verification via CBMC. If the C candidate passes the interpreter, PYVERITAS verifies it using a bounded model checker for C, CBMC (Clarke, Kroening, and Lerda 2004). If verification succeeds, PYVERITAS concludes that the original Python program satisfies the specification S. MaxSAT-Based Fault Localisation. If verification fails, the candidate C is a… view at source ↗

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta-Analysis in Python

    cs.SE 2026-07 accept novelty 6.0 of 10

    Why3-py is a Python front-end to Why3 plus an extended StatWhy that verifies annotated hypothesis-testing and meta-analysis programs by discharging assumption and interpretation obligations.

  2. MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

    cs.AI 2026-07 conditional novelty 5.0 of 10

    MaxSAT-based feedback that keeps Sudoku rules hard and VLM placements soft improves logical consistency and solve rates of vision-language models on Sudoku.

  3. MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

    cs.AI 2026-07 conditional novelty 5.0 of 10

    Adding MaxSAT-based conflict feedback to a vision-language model increases solved Sudoku instances across all tested models, most notably GPT-5.5 in full-board mode (45 to 73 solved).

Reference graph

Works this paper leans on

17 extracted references · 13 canonical work pages · cited by 2 Pith papers

  1. [1]

    **Function Definition**: The function `makeTheIntegerZero` takes two integers `num1` and `num2` as input and returns an integer

    work page

  2. [2]

    **Variable Initialization**: We initialize `a` to 0, and `x` and `y` to `num1` and `num2` respectively

    work page

  3. [3]

    Inside the loop: - `x` is decremented by `y`

    **While Loop**: The loop continues as long as `x` is less than `y`. Inside the loop: - `x` is decremented by `y`. - `a` is incremented by 1. - Variables `b`, `c`, `cc`, and `z` are initialized. `b` is set to `x`, `c` and `cc` to 0, and `z` to 1

    work page

  4. [4]

    - `c` counts the number of 1s in the binary representation of `b`

    **Inner While Loop**: This loop calculates the number of 1s in the binary representation of `b` (`c`) and the sum of powers of 2 corresponding to those 1s (`cc`). - `c` counts the number of 1s in the binary representation of `b`. - `cc` calculates the sum of powers of 2 corresponding to the positions of 1s in `b`

    work page

  5. [5]

    **Condition Check**: If `c` is less than or equal to `a` and `cc` is greater than or equal to `a`, the function returns `a`

    work page

  6. [6]

    **Return Statement**: If the loop exits without finding a valid `a`, the function returns `-1`

    work page

  7. [7]

    All assertions passed

    **Main Function**: The `main` function includes an assertion to test the function with the example provided. If the assertion passes, it prints "All assertions passed." This C code should behave the same way as the provided Python code. – QWEN 2.5-C ODER transpiled Algorithm 5 to C; note that it preserved the program’s semantics by retaining the buggy bin...

    work page

  8. [15]

    The `distributeCandies` function calculates the number of ways to distribute `n` candies among 3 children such that no child gets more than `limit` candies

    work page

Show all 17 references
  1. [16]

    The `main` function includes the `assert` statement to check if the `distributeCandies` function returns the expected result for the given input `n = 5` and `limit = 2`

  2. [17]

    The `assert` statement in the `main` function ensures that the result of `distributeCandies(5, 2)` is equal to 3, as per the example provided. – DEEP SEEK -C ODER -V2 transpiled Algorithm 6 to C, and during this process the model fixed the injected bug, by removing line 4 (i.e...

  3. [301]

    Springer. Llama3. 2024. The Llama 3 Herd of Models. arXiv:2407.21783. Marques-Silva, J.; Janota, M.; Ignatiev, A.; and Morgado, A. 2015. Efficient Model Based Diagnosis with Maximum Satisfiability. In IJCAI 2015, 1966–1972. AAAI Press. Maveli, N.; Vergari, A.; and Cohen, S. B....

    2024 arXiv

  4. [398]

    Huang, H.; Tsai, W.; Paul, R

    IEEE. Huang, H.; Tsai, W.; Paul, R. A.; and Chen, Y . 2005. Auto- mated Model Checking and Testing for Composite Web Ser- vices. In Eighth IEEE International Symposium on Object- Oriented Real-Time Distributed Computing (ISORC 2005), 18-20 May 2005, Seattle, WA, USA , 300–307....

    2005 arXiv

  5. [2009]

    IOS Press

    Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press. Chong, N.; Cook, B.; Kallas, K.; Khazem, K.; Monteiro, F. R.; Schwartz-Narbonne, D.; Tasiran, S.; Tautschnig, M.; and Tuttle, M. R. 2020. Code-level model checking in t...

    2020 arXiv

  6. [2021]

    In NeurIPS

    Self-Supervised Bug Detection and Repair. In NeurIPS. Bacchus, F.; J¨arvisalo, M.; and Martins, R. 2021. Maximum Satisfiability. In Biere, A.; Heule, M.; van Maaren, H.; and Walsh, T., eds.,Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Inte...

    2021

  7. [2024]

    In Glober- sons, A.; Mackey, L.; Belgrave, D.; Fan, A.; Paquet, U.; Tomczak, J

    Verified Code Transpilation with LLMs. In Glober- sons, A.; Mackey, L.; Belgrave, D.; Fan, A.; Paquet, U.; Tomczak, J. M.; and Zhang, C., eds., Advances in Neu- ral Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024...

    2024

  8. [2025]

    All assertions passed.\n

    VERINA: Benchmarking Verifiable Code Generation. CoRR, abs/2505.23135. Zhang, H.; David, C.; Wang, M.; Paulsen, B.; and Kroen- ing, D. 2025. Scalable, Validated Code Translation of Entire Projects using Large Language Models. Proc. ACM Pro- gram. Lang., 9(PLDI). Zhang, J.; Cam...

    2025

  9. [5140]

    Lahtinen, J.; Valkonen, J.; Bj¨orkman, K.; Frits, J.; Niemel ¨a, I.; and Heljanko, K

    AAAI Press. Lahtinen, J.; Valkonen, J.; Bj¨orkman, K.; Frits, J.; Niemel ¨a, I.; and Heljanko, K. 2012. Model checking of safety-critical software in the nuclear engineering domain. Reliab. Eng. Syst. Saf., 105: 104–113. LeetCode. 2025. https://leetcode.com. Accessed: 2025-07-...

    2012

Pith tools

Reviewed August 5, 2026 · model on record in the stance chip above.