SQLVerify Documentation

SQLVerify formally proves that two SQL queries return the same result on every database — or hands you a concrete database where they disagree. It is a solver, not a linter: an equivalent verdict is a proof, and a divergent verdict comes with the counterexample that produced it.

Quickstart

Every surface talks to the same engine. Pick whichever fits where the query lives. You'll need an API key from the API Keys page first.

HTTP

curl -X POST https://sqlverify.com/api/verify/text \
  -H "Authorization: Bearer $SQLVERIFY_API_KEY" \
  -H "Content-Type: application/json" \
  -d '{
    "ddl_sql": "CREATE TABLE users (id INT PRIMARY KEY, org_id INT);",
    "sql_v1": "SELECT id FROM users",
    "sql_v2": "SELECT id FROM users WHERE org_id IS NOT NULL"
  }'

CLI

export SQLVERIFY_API_KEY=sqv_your_key_here

sqlverify verify --ddl schema.sql --v1 before.sql --v2 after.sql

# or verify every query your branch changed:
sqlverify diff --base origin/main --ddl migrations/ 'queries/*.sql'

AI agents (MCP)

Expose verification as a tool to Claude Code, Claude Desktop, or Cursor so an agent can check its own SQL rewrites in-loop and revise against a real counterexample instead of guessing.

Setup instructions →

API reference

POST /api/verify/text

Authentication

Send your key as Authorization: Bearer sqv_… or X-API-Key: sqv_…. Keys are shown once at creation and stored only as a hash — if you lose one, revoke it and mint another.

Request body

Field	Type	Default	Description
ddl_sql	string	required	Flyway-style CREATE TABLE DDL defining the schema both queries run against. ALTER TABLE statements are folded in statement order.
sql_v1	string	required	The original / trusted SELECT query.
sql_v2	string	required	The rewritten query to prove equivalent to sql_v1.
dialect	string	generic	Parser dialect hint. Both queries are read as the same dialect — cross-dialect comparison is out of scope.
bound	integer	3	Maximum rows per table Z3 explores. Higher catches rarer bugs and costs solve time. Values above 6 are rejected.
timeout_ms	integer	60000	Solver budget in milliseconds. Clamped to 120,000. On timeout the status is unknown — never a wrong verdict.
project_id	string \| null	null	Optional project UUID to tag the run with. Silently dropped if the project isn't yours.

Response body

Field	Type	Description
status	string	equivalent, divergent, unknown, or error. See the table below.
divergence_reason	string \| null	Short summary of how the two queries differ. Present when status is divergent.
counterexample_db	object \| null	A concrete database — table name to rows — on which the two queries disagree. This is the proof, and it is replayable.
query_v1_output	array \| null	Rows sql_v1 returns when run on counterexample_db.
query_v2_output	array \| null	Rows sql_v2 returns when run on counterexample_db.
error_message	string \| null	Why the input was rejected. Present when status is error.
explanation	string \| null	Prose explanation of the divergence, written by the configured LLM. Populated automatically for divergent results.

Status values

equivalent	Proven: no database within the bound distinguishes the two queries.
divergent	The queries disagree. `counterexample_db` holds a database that proves it, and both outputs are replayed on it.
unknown	The solver ran out of time. Not a proof of equivalence — it means we don't know.
error	The input used SQL outside the supported subset, or the DDL didn't parse. SQLVerify fails closed rather than silently ignoring what it can't encode.

Example: a divergent result

The quickstart request above returns this — the rewrite silently drops users whose org_id is NULL:

{
  "status": "divergent",
  "divergence_reason": "A row returned by sql_v1 is absent from sql_v2",
  "counterexample_db": {
    "users": [{ "id": 1, "org_id": null }]
  },
  "query_v1_output": [{ "id": 1 }],
  "query_v2_output": [],
  "error_message": null,
  "explanation": "sql_v2 adds `WHERE org_id IS NOT NULL`. Under three-valued
    logic `NULL IS NOT NULL` is false, so the row is filtered out …"
}

Error responses

401	Missing, malformed, or revoked API key.
402	Free-tier monthly run limit reached. See pricing.
422	Body failed validation — a missing field, or a `bound` above 6.
429	Per-IP rate limit exceeded. Back off and retry.

Note that a divergent verdict is still an HTTP 200 — the request succeeded, the queries just aren't equivalent. Only the codes above indicate a failed call.

Limits

bound caps at 6 rows per table.
timeout_ms defaults to 60,000 and is clamped to 120,000.
Uploaded SQL files cap at 512 KB each.
An equivalent verdict is sound within the bound — it rules out every counterexample up to that many rows per table, which covers the overwhelming majority of real rewrite bugs.

Supported SQL

SQLVerify handles multi-table join chains mixing INNER, LEFT, RIGHT, and FULL joins, GROUP BY and HAVING with aggregates, three-valued NULL logic, non-recursive CTEs, and uncorrelated IN (SELECT …) subqueries. NULLs, primary keys, foreign keys, and NOT NULL constraints are all modelled.

Anything outside that subset — window functions, UNION, SELECT DISTINCT, LIMIT, correlated subqueries — returns error rather than a guess. That is deliberate: a verifier that quietly skips what it can't encode would report equivalent for queries it never actually checked, which is the one failure mode a proof tool must not have.