How to Prove the Correctness of AI-Generated Code Using Formal Methods
As AI-generated code becomes increasingly common, ensuring its correctness, particularly in safety- and security-critical systems, has become a pressing challenge. Traditional testing approaches are insufficient when code is generated by non-deterministic models from ambiguous natural-language prompts. We explore how formal methods, using the SPARK programming language, can be applied to prove the correctness of AI-generated code with mathematical rigour.
More and more code is being generated by AI, generated by non-deterministic models from ambiguous text in English or another language. How do you prove the correctness of this code?
The standard way of proving correctness is to run the code through unit and regression test cases. Which may be good enough for enterprise code, but that certainly will not be sufficient for code that is safety or security critical.
The video below demonstrates another approach using the programming language SPARK. SPARK is a subset of Ada that adds formal proof as a first-class entity into the language. SPARK allows the programmer to 1) prove the absence of runtime errors; and 2) prove functional correctness of a piece of code.
The demonstration starts off with the specification of binary search, which is given with pre- and post-conditions. From there, formal proof can be used to validate the AI-generated implementation, which turns out to have a couple of corner cases that are problematic.
SPARK provides a breakthrough in the use of formal methods in industrial strength programming languages. It has been proven in use, it is performant, and available on a wide array of hardware targets and operating systems.
This demonstration uses a basic workflow using VS Code and GitHub Copilot. More advanced agentic workflows are possible by using Model-Context-Protocol (MCP) integrations to provide mode information to the AI agents, but that is content for a follow-on demonstration.
