Formal Verification of SQL Queries in Lean for Enhanced Accuracy
Verifying SQL queries in Lean
Querying databases with SQL is a core part of data analysis. In the case of data analysis done by agentic AI systems, the queries are often obtained by translating from natural language. If the translation is incorrect the resulting analysis becomes suspect. Thus, it is important to ensure that translation to SQL has high accuracy.
We describe a system to use formal verification in Lean to significantly increase the accuracy of translation from natural language to SQL. As we obviously do not have a translation known to be correct (or we would simply use it), we cannot directly prove, or even state, what correction means. Instead we use proof challenges, which are tests of internal consistency that are unlikely to be satisfied by wrong translation.
The Key Idea
Concretely, we can ask an LLM to generate more than one translation to SQL. If all the translations are correct, then they must be equivalent, i.e., give the same answer for all databases. This equivalence can be formulated as a mathematical statement in Lean, and proof automation can attempt to prove this. A failure to prove equivalence, or better still a counterexample, indicates (in the case of a counterexample proves) that at least one of the queries is incorrect.
On the other hand, if two translations are equivalent but not correct, they have to not only both be wrong but both be wrong in exactly the same way. This is unlikely, especially if we prompt in a way so that the two translations are not literally identical. Indeed, SQL queries are generally optimised for performance and conciseness. If we generate a translation with the default prompt, and a second translation with a prompt asking for a query that optimised ease of understanding, we are likely to get different translations. Furthermore, a query optimised for understandability is more likely to be correct than one optimised for performance. Thus, an equivalence of two translations generated in this fashion is strong evidence of correctness of both of them.
We emphasise that when we prove equivalence we are not testing equivalence in the case of a specific database. Instead we only specify the database schema — the names and data types of the columns, and prove that for all databases with this schema the two queries return equal results. Obviously we cannot check this for all databases. However, we can (and do) abstract this as equality of two mathematical functions, and attempt to prove this equality.
There are many ways to refine this. The most obvious one is to generate more than one translation and attempt to prove that these are all equivalent. Further, instead of proving equivalence we can generate queries so that the results returned by the desired query is a subset of those returned by an auxiliary one. For instance, all voters must be at least 18 years of age. So if the goal is to generate a query that gives all eligible voters in a constituency, we can also translate the query to retrieve all those with age at least 18, and try to prove that indeed all voters have age at least 18.
Further, columns of a database are not independent. Indeed some may be computed in terms of others, while in some cases we have clear relations or constraints. Thus, queries may become equivalent (or become subsets) given the constraints and relations, and we must consider this more general notion.
Proving versus testing
An alternative to our approach not involving formal verification would be to randomly generate a collection of databases and check if equivalence of queries (or other expected properties) hold for each of these. However, this approach can miss corner cases. As an example, a query for voters who are voting for the first time may be accidentally translated as (18 ≤ AGE) AND (AGE + 5 ≤ 18) (we assume that the last election was 5 years ago and the eligibility age is 18). This is a typical mistake made when negating an inequality and forgetting that the negation of a weak inequality such as ≤ involve a strict inequality such as <. If a second (more "easy to understand" query is correct), the difference will be noticed only if someone was exactly 13 years old in the last election. While such a person is likely to be present, an actual query may ask for only male voters in a specific constituency and may be in terms of the date of birth. Thus, the error (more precisely the discrepancy between the incorrect and correct queries) will be noticed only if there is a male voter born on a specific date in a specific constituency, and a random database is quite likely to have no such voters.
Implementation
Lean is a programming language whose foundations allow it to be used as a formal proof system. It also has excellent support for extending syntax and other metaprogramming. We use all these aspects of Lean to implement verification of equivalence (and other properties) of SQL queries, with a JSON API over HTTP that allows integration into agentic frameworks.
Modelling SQL
The first part of the implementation is a model of SQL queries in Lean. For this we define types (essentially analogues of classes or structures) and functions for database schemas, then for databases (corresponding to a schema) and finally for SQL queries on databases. Our model for databases is Relation Algebras. Our model for a row in a database is what we call a TypedTuple, which is parametrized by (our model of) Database schemas. Databases are finite sets of such rows. SQL queries then become functions on databases.
The Lean implementation of our model for a Database.
We also define relational algebra operators in Lean that would help us represent SQL queries in Lean.
This defines the restriction operator which selects rows based on a predicate
This is the implementation of set difference operator
While the first step has analogues in any high-level programming language, the subsequent steps need special features of Lean.
Proving Basic Theorems
Our next step is to state and prove theorems about our model for SQL queries. Firstly, we prove the basic properties of queries in a relation algebra. In addition to these we prove many other basic results.
Proving these theorems has two uses. Firstly, it serves as a check on our model. Indeed, it is a common experience in working with Lean that subtle mistakes in definitions are uncovered when trying to prove a theorem and ending up at a dead-end or a false statement. In addition, the theorems we prove can be used in proofs of equivalence of specific queries such as those obtained by translation.
Some basic theorems proved in Lean
Proof Automation
While the above two steps allow us to state and interactively prove (or fail to prove) equivalence of queries, for autonomous use such as in agentic frameworks it is necessary to have push-button automation, i.e., where a single function call proves equivalence. Such a function call cannot always succeed in proving queries are equivalent if they are, as it is known that the equivalence of queries is algorithmically undecidable. However, we want such a function to succeed in a large fraction of the cases we encounter in practice.
Our next step is to use Lean's automation, based on tactics, to do implement such push-button automation. Specifically, Lean has a powerful tactic called grind that can use both known theorems as well as various decision procedures (including SMT solvers) to prove results. To allow us to use these effectively we prove several theorems and annotate them so that they are used by grind. With enough such theorems proved, and with some further enhancements, we manage to prove equivalence in a large number of cases.
SQL Syntax in Lean
The syntax of Lean can be readily extended, even adding new syntax categories. This can be done recursively. We introduce new syntax categories corresponding to SQL queries as well as various components of SQL queries. We then introduce constructions that let us interpret SQL queries as syntax within Lean.
sql_query is the syntax category corresponding to SQL queries.
Finally, we implement parsers, which are Lean functions that map the syntax of SQL queries to terms (objects) in our model of SQL.
A working example
We look at the following example of two databases orders and customers.
orders
| Column | Type |
|---|---|
| order_id | INT |
| cust_id | INT |
| region | STRING |
| amount | INT |
| status | STRING |
customers
| Column | Type |
|---|---|
| cust_id | INT |
| name | STRING |
| tier | STRING |
| active | BOOL |
We prove that the following two queries are equivalent:
Using the parsers and the mapped SQL syntax, we state the equivalence in Lean as shown below and a push-button automation tactic sql_equiv finishes off the proof.
sql_equiv is a naive push-button automation that proves the equivalence of the queries.
Interfaces
All of the above forms a Lean library and can be used interactively by simply including it as a dependency or opening the project and working in it. However, for integration with agentic frameworks we need to work from outside Lean. Note that the startup time for Lean and loading its Mathematics library Mathlib is high, so it is important to have a running Lean process with which agents can interact.
Fortunately Lean is written in Lean and the same functions that are used by the interpreter to prove using tactics (among other things) are available in a convenient API. Using this, we have implemented a Lean executable that runs in a loop, repeatedly taking as input JSON consisting of a database schema and a collection of queries, and output JSON with the result of attempting to prove equivalence and some diagnostics. This is wrapped in an http server (which is dockerized), allowing convenient integration into agentic flows.
Future work
In ongoing and future work, we will implement the following:
- Support for proof challenges other than equivalence.
- Equivalence and other relations given constraints on and relations between columns.
- Better diagnostic information in case of failure to prove.
- Integration with Lean's plausible library to generate counterexamples.
- Benchmark the gains in accuracy as well as also success rate in proving equivalence when true.
- Strengthen proof automation to raise the success rate of proving equivalence.