# VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints

arXiv: https://arxiv.org/abs/2403.03193 · HTML: https://mlsanity.com/paper/2403.03193/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Mar 2024.

## Built on by (most cited first, 8 of 8)

- [SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification](https://mlsanity.com/paper/2510.26840/) (2025)
- [Can the Rookies Cut the Tough Cookie? Exploring the Use of LLMs for SQL Equivalence Checking](https://mlsanity.com/paper/2412.05561/) (2024)
- [High-Fidelity And Complex Test Data Generation For Google SQL Code Generation Services](https://mlsanity.com/paper/2504.17203/) (2025)
- [RISE: Rule-Driven SQL Dialect Translation via Query Reduction](https://mlsanity.com/paper/2601.05579/) (2026)
- [SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints](https://mlsanity.com/paper/2603.04334/) (2026)
- [Human-Level Text-to-SQL via Reinforcement Learning on Verified Data, Without Pipeline Engineering](https://mlsanity.com/paper/2603.20004/) (2026)
- [Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search](https://mlsanity.com/paper/2504.06542/) (2025)
- [ROSE: An Intent-Centered Evaluation Metric for NL2SQL](https://mlsanity.com/paper/2604.12988/) (2026)

## Abstract (arXiv)

The task of SQL query equivalence checking is important in various real-world applications (including query rewriting and automated grading) that involve complex queries with integrity constraints; yet, state-of-the-art techniques are very limited in their capability of reasoning about complex features (e.g., those that involve sorting, case statement, rich integrity constraints, etc.) in real-life queries. To the best of our knowledge, we propose the first SMT-based approach and its implementation, VeriEQL, capable of proving and disproving bounded equivalence of complex SQL queries. VeriEQL is based on a new logical encoding that models query semantics over symbolic tuples using the theory of integers with uninterpreted functions. It is simple yet highly practical -- our comprehensive evaluation on over 20,000 benchmarks shows that VeriEQL outperforms all state-of-the-art techniques by more than one order of magnitude in terms of the number of benchmarks that can be proved or disproved. VeriEQL can also generate counterexamples that facilitate many downstream tasks (such as finding serious bugs in systems like MySQL and Apache Calcite).