Source-linked AI summary
TrustedCode: Evaluating Large Language Models for Developing Trusted Code through Automated Program Verification
Muhammad Danial, Muhammad Taimoor Khan
TL;DR
Formal verification offers a way to establish software trust, but writing specifications and proving correctness remain difficult, and Python support is limited. TrustedCode uses an LLM and Why3 in a LangGraph repair loop to verify Python programs. In tests on ten functions, simple functions were solved with a 100% success rate and averaged 1.5 tries, while more complex cases required more attempts and bubble sort lacked a sound proof.
Problem
Formal verification of Python has limited practical adoption amid specification and proof-writing challenges, and existing verification tools offer minimal Python support.
Source: §I · p. 1Method
TrustedCode combines LLM-based Python typing and WhyML translation with Why3 verification and iterative LangGraph repair using solver feedback.
Source: §I · p. 1, A. System Architecture · pp. 1–2Results
100% of simple functions were solved at an average of 1.5 tries; for-loop functions averaged 4 tries, while hard while-loop functions averaged 5.5 tries, and bubble sort lacked a sound proof.
Source: B. Quantitative Analysis · p. 2Takeaways & Limitations
The evaluation finds that the LLM’s attempts increase with algorithmic complexity, with complex loop invariants and termination terms posing greater difficulty.
Source: B. Quantitative Analysis · p. 2
Abstract
from arXiv · showhide
Recent reports, such as "Who is using AI to code?", indicate that approximately 30\% of Python code contributions to GitHub are AI-generated. Given the inherent unreliability of this code, formal verification emerges as a promising approach to establish trust in software correctness. Although leveraging large language models (LLMs) for formal verification has garnered increasing attention, practical adoption remains limited due to the challenges in writing formal specifications and verifying program correctness against them. Existing tools predominantly support verification for languages such as Java and C, with minimal support for Python. We present TrustedCode, an automated framework for verifying AI-generated Python code. TrustedCode uses LLMs to (i) type-check Python code, (ii) translate it into WhyML via the Why3 framework, and (iii) verify it against formal specifications using Why3 back-end automated theorem provers. Our method integrates chain-of-thought prompting through LangGraph to identify and address LLM limitations in specification generation and proving the specified programs. To evaluate TrustedCode, we conducted experiments on ten Python programs of varying complexity. Our analysis reveals that 50\% of the observed errors stem from domain knowledge gaps, 30\% from syntactic inaccuracies, and the remaining 20\% from semantic and type-related issues. These findings underscore the importance of targeted improvements in LLM-guided formal verification workflows for Python. TrustedCode is an open source tool available at: \href{github.com/mtaimoorkhan/TrustedCode}{github.com/mtaimoorkhan/TrustedCode}. The video demonstration is available at: \href{youtu.be/Nr5I2g8ec-s}{youtu.be/Nr5I2g8ec-s}
I. INTRODUCTION
Formal verification can establish trust in software, but specification and proof difficulties have limited its industrial adoption. TrustedCode investigates an LLM’s ability to translate Python into verifiable WhyML and correct errors through a self-correction loop.
I. INTRODUCTION
- Formal reasoning can establish software trust, but specification-writing and proof difficulties have limited its industry acceptance.The introduction also argues that increasing software complexity makes traditional testing increasingly inadequate.Source: §I · p. 1
- Prior work has explored proof repair with Coq, LLM-based premise selection and proof generation [3], and iterative complete-proof generation with Baldur.These examples are presented as related efforts addressing proof generation or repair.Source: §I · p. 1
- TrustedCode studies Claude Sonnet 4’s capability gaps in translating Python into automatically verifiable WhyML and its effectiveness in a self-correction loop.The paper asks how the model performs within that workflow and what gaps arise.Source: §I · p. 1
- The framework combines LLMs, Why3, and iterative LangGraph repair to translate Python into WhyML and produce provably correct programs.It also classifies gaps in types, theory, syntax, and semantics rather than relying only on pass/fail.Source: §I · p. 1
A. System Architecture
TrustedCode uses a stateful LangGraph workflow to type-check Python, generate WhyML, run verification, and feed solver errors into iterative repairs. The loop ends on success or after ten attempts.
A. System Architecture
- During error correction, the LLM is prompted to analyze the full history of prior errors and specifications before proposing a repair.This uses a chain-of-thought process with a <thinking> block.Source: A. System Architecture · p. 2
- LangGraph models the workflow as a directed graph whose vertices represent functions and whose edges include fixed and conditional transitions.The conditional retry decision routes execution to correction or to the end state.Source: A. System Architecture · p. 2
- The workflow translates input Python into well-typed Python, generates WhyML, and invokes Why3 with the Alt-Ergo back-end solver to verify it.A successful execution ends the workflow; solver errors are captured for repair.Source: A. System Architecture · pp. 1–2
- When verification fails, the error log, typed Python, and current WhyML return to the LLM for repair, with at most ten attempts.The executor reruns the revised specification until it is proven or the retry limit is reached.Source: A. System Architecture · pp. 1–2
B. Capability Gap Analysis
The capability-gap analysis classifies LLM errors across program, theory, and specification domains; typing, syntax, and semantics; and environment, domain, and proving knowledge gaps.
B. Capability Gap Analysis
- The framework classifies errors by domain—program, theory, or specification—and by type: typing, syntax, or semantics.A semantic error may occur in the logical, mathematical, or contractual part of code.Source: B. Capability Gap Analysis · p. 2
- It also distinguishes knowledge gaps involving the environment, domain, or proving.The analysis is applied to the LLM’s steps to expose deficiencies in its knowledge base.Source: B. Capability Gap Analysis · p. 2
- Semantic errors are assigned to different domains depending on whether they arise in generated logic, mathematics, or contractual code.This distinguishes the location of an error from its type.Source: B. Capability Gap Analysis · p. 2
A. Dataset Description
The evaluation uses ten Python functions spanning behavioral complexity from basic conditionals to loops, to assess LLM reasoning in specifying and proving correctness.
A. Dataset Description
- The evaluation analyzes ten Python functions selected to cover common language constructs and varied behavioral complexity.Performance is assessed qualitatively and quantitatively.Source: A. Dataset Description · p. 2
- The functions are grouped into Easy basic if-else statements, Medium for-loops, and Hard while-loops.These categories reflect behavioral complexity for specifying and proving correctness.Source: A. Dataset Description · p. 2
- The evaluation uses the three complexity groups to examine the LLM’s reasoning capabilities in specifying and proving program correctness.Source: A. Dataset Description · p. 2
B. Quantitative Analysis
TrustedCode’s verification effort rose with function complexity, but complexity did not predict the number of repair attempts linearly. The LLM did not produce a sound proof for bubble sort.
B. Quantitative Analysis
- 100% of simple functions were verified in an average of 1.5 tries, while more complex for-loop functions averaged 4 tries.The sum array function took the full 10 tries.Source: B. Quantitative Analysis · p. 2
- Hard while-loop functions with complex invariants or termination terms averaged 5.5 tries, and bubble sort did not yield a sound proof.The analysis aggregated capability gaps and relevant functions in Table III and visualized them in Figure 2.Source: B. Quantitative Analysis · p. 2
C. Library Knowledge Gaps
Knowledge gaps were the most prevalent errors, and Why3 ecosystem knowledge recurred across programs. Verification attempts did not increase linearly with program complexity, while highly complex postconditions remained difficult to translate or prove.
C. Library Knowledge Gaps
- Circa 50% of errors were attributed to knowledge gaps.The authors identify missing knowledge of the Why3 ecosystem and suggest targeted prompts referencing relevant library APIs as a way to address it.Source: C. Library Knowledge Gaps · p. 3
- The number of attempts did not relate linearly to program complexity: medium sum array took 10 tries, while hard binary search took 8.An easy division program took one attempt, while an easy absolute-value function initially had an EKnow error.Source: C. Library Knowledge Gaps · p. 3
- Why3 API knowledge recurred across programs; in Dutch national flag, the LLM used incorrect syntax and did not specify the relevant library.It then explicitly defined a function but still did not import the correct library.Source: C. Library Knowledge Gaps · p. 3
- In factorial, the LLM referenced a nonexistent library, then could not prove termination of its recursive replacement and reverted to a loop.Source: C. Library Knowledge Gaps · p. 3
- The LLM could not directly translate or prove highly complex postconditions and reverted to the simplest specification option.For bubble sort, the prover timed out after the maximum 10 tries.Source: C. Library Knowledge Gaps · p. 3
D. Syntactic Gaps
WhyML syntax errors accounted for roughly 30% of observed gaps, and the authors report that error-log context was not optimized for self-correction. Binary search also exposed limited knowledge of WhyML lambda syntax.
D. Syntactic Gaps
- Roughly 30% of program gaps stemmed from misunderstanding WhyML syntax, with GCD modulo errors requiring several attempts to correct.The authors suggest that syntactic errors and insufficient context from Why3 error logs contributed to the repeated attempts.Source: D. Syntactic Gaps · p. 4
- WhyML error-log context was not optimized for LLM performance in the self-correcting loop.Source: D. Syntactic Gaps · p. 4
- In binary search, the LLM confused Python’s division operator with Why3 syntax and showed limited knowledge of WhyML lambda expressions.It also mismatched a function signature with the number of arguments provided.Source: D. Syntactic Gaps · p. 4
E. Semantic and Typing Gaps
Semantic and typing errors were relatively uncommon, but examples show difficulty translating data types and proving programs with multiple postconditions.
E. Semantic and Typing Gaps
- Semantic errors accounted for 19% of errors, while type errors accounted for 3%.The authors suggest that knowledge gaps may explain these low shares.Source: E. Semantic and Typing Gaps · p. 4
- In sum array, using “list” as a variable name led the LLM to nest list types and mismatch the expected integer type.The final attempt replaced the iterative approach with a recursive function; the authors suggest the LLM could not handle multiple postconditions.Source: E. Semantic and Typing Gaps · p. 4
- In binary search, the LLM failed to translate Python floats into Why3 theory types, but an integer-based specification was successfully proven by the SMT solver.An attempted repair using real numbers also failed.Source: E. Semantic and Typing Gaps · p. 4