provensql: Sound, Catalog-Aware Detection of Behavior-Changing SQL Edits — and Why LLMs Can't Be Trusted To Do It

provensql decides whether an edit to a SQL query changes its result. It returns EQUIVALENT only with a proof (canonical-form or SMT), DIFFERENT only with a concrete, executable counterexample database instance, and otherwise abstains (UNKNOWN) rather than guess — soundness (never a false EQUIVALENT) is enforced structurally and defended at runtime by a cross-engine backstop. This paper presents the tool, evaluates it on 213 hand-labeled real-world SQL edits and 511 adversarial mutations (zero false EQUIVALENT; Clopper–Pearson 95% upper bound 0.58%), compares it against a state-of-the-art LLM judge (OpenAI gpt-5: 85.9% accuracy but 2 false EQUIVALENT vs provensql's 0), and honestly places it against the SQL-equivalence-proving frontier (QED, VeriEQL). Open source (Apache-2.0) at github.com/nac7/provensql.