TrustedCode uses AI to verify Python code correctness automatically
TrustedCode: Evaluating Large Language Models for Developing Trusted Code through Automated Program Verification
Software EngineeringLogic in Computer ScienceProgramming Languages
Summary
A growing amount of Python code on sites like GitHub is written by AI, but this code can have mistakes that are hard to trust. The authors created TrustedCode, a tool that uses AI models to check Python programs for errors by translating them into a language that can be formally verified. Their experiments show that many errors come from missing knowledge or syntax mistakes, highlighting where AI tools need improvement. This tool helps make AI-generated code more reliable and trustworthy.
What this means in practice
- •For software developers: Automatically verify AI-generated Python code against formal specifications to improve software correctness.
- •For quality assurance teams: Integrate automated formal verification for Python code to detect domain knowledge and semantic errors early in the development process.
Authors
Muhammad Danial, Muhammad Taimoor Khan
Abstract
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}