Provensql – prove two SQL queries are equivalent

Hacker News

Share card

Provensql – prove two SQL queries are equivalent

I'm a data/infra engineer and kept hitting the "is this SQL refactor actually safe?" question in review. Provensql decides equivalence of two queries and returns one of four honest verdicts: EQUIVALENT (proven), DIFFERENT (with a concrete counterexample row), SCHEMA_CHANGE, or UNKNOWN — it refuses rather than guess. It's sound by construction: it never returns a false EQUIVALENT. Across 511 equivalence-breaking mutations it produced zero. There's an SMT proof engine for the conjunctive fragment and a counterexample search for the rest. As a baseline I ran a gpt-5 judge over the same 213 labeled pairs — it claimed EQUIVALENT on 2 pairs that actually differ; provensql structurally can't make that error. The part I'm most interested in feedback on: it also catches rewrites valid over the reals but that diverge under IEEE-754 (reassociation) or change runtime-error behavior (a/b → SAFE_DIVIDE) — cases every other checker treats as exact-real and silently accepts. Try it: pip install provensql, a GitHub Action that gates PRs (github.com/nac7/provensql-action), and an interactive demo in the repo. Apache-2.0, github.com/nac7/provensql. Feedback on fragment coverage and which dialects to add next is very welcome.