solver online z3 5.0.0 bag semantics dialects: generic · postgres · mysql · sqlite

bound 1–6 fail-closed on unsupported SQL

SMT-backed equivalence checking

Don't test the
rewrite. Prove it.

Skolem compiles both queries to SMT constraints and asks Z3 whether a database exists where they disagree. If one does, you get that database — every row, every NULL.

$ pipx install ./cli skolem verify · skolem diff

or wire it into CI and your coding agent — see /integrations

passwordless — one-time magic link, no credentials stored

bound = 3

original.sql

SELECT u.id, COUNT(o.id)
FROM users u
LEFT JOIN orders o
  ON o.user_id = u.id
GROUP BY u.id;

rewrite.sql · llm

SELECT u.id, COUNT(*)
FROM users u
JOIN orders o
  ON o.user_id = u.id
GROUP BY u.id;

$ skolem verify --bound 3

ready — press Run proof to encode both queries

V1__users_orders.sql · flyway migration

CREATE TABLE users (
  id    INT  PRIMARY KEY,
  name  TEXT NOT NULL
);

CREATE TABLE orders (
  id       INT PRIMARY KEY,
  user_id  INT NOT NULL REFERENCES users(id),
  cents    INT NOT NULL
);

-- keys and NOT NULL become Z3 assertions: the solver may only build databases your schema actually permits, so a counterexample is never one your production data could not contain.

Anatomy of a proof

// six stages, no test data involved

01 · parse

SQL → AST

Dialect-aware parse of both queries, plus your Flyway DDL with every ALTER TABLE folded in.

02 · normalize

Relational algebra

Bag semantics preserved — duplicates are part of the meaning, so multiplicity is compared, not just membership.

03 · encode

SMT constraints

Schema, keys and three-valued logic become Z3 assertions. Each cell is an (is_null, value) pair.

04 · solve

Z3 satisfiability

Ask for a database where the outputs differ, bounded to k rows per table.

05 · verdict

unsat = equivalent

No such database exists within the bound — or here is one, printed as rows you can paste.

06 · cross-check

Replay on SQLite

Every counterexample is re-run on a real SQLite database. If the outputs agree after all, we report an internal error rather than show you a fake.

Counterexample database

A failing test you didn't have to write

The LEFT JOIN → JOIN rewrite drops users with no orders. Two rows are enough to prove it, and Skolem hands you those two rows.

PK FK NN constraints honoured in the model

users

id	name
1	ada
2	lin

orders

id	user_id	cents
10	1	4900

original.sql output2 rows

u.id	count
1	1
2	0

rewrite.sql output1 row — u=2 lost

u.id	count
1	1

-- reproduce locally
INSERT INTO users VALUES (1, 'ada'), (2, 'lin');
INSERT INTO orders VALUES (10, 1, 4900);

Verification coverage

// what the encoder handles today

SELECT / projectionencoded

WHERE / HAVING (3-valued)encoded

INNER · LEFT · RIGHT · FULLencoded

NULL semanticsencoded

GROUP BY + HAVINGencoded

COUNT(*) · COUNT(col) · SUMencoded

Bag multiplicityencoded

PK · FK · NOT NULLencoded

Non-recursive CTEspartial

IN (SELECT …) uncorrelatedpartial

TEXT / TIMESTAMPequality only

ORDER BYparsed, ignored

UNION · DISTINCT · LIMITrejected

Window functionsrejected

EXISTS · correlated subqueriesrejected

MIN · MAX · AVG · LIKErejected

encoded — proved for every database within the bound partial — supported subset, limits documented rejected — refused outright, never guessed

Anything outside the subset raises an error instead of being silently dropped. A skipped predicate would weaken the encoding and could return a false “equivalent” — the one failure mode a verifier must not have.

CI/CD API

One engine, three surfaces

The workspace, the skolem CLI and the MCP server all call the same solver. Gate a pull request on status == "equivalent" and let the counterexample land in the PR comment.

POST /api/verify/text

curl -X POST https://sqlverify.com/api/verify/text \
  -H "Authorization: Bearer $SKOLEM_API_KEY" \
  -H "Content-Type: application/json" \
  -d '{
    "ddl_sql": "CREATE TABLE users (...);",
    "sql_v1":  "SELECT ...",
    "sql_v2":  "SELECT ...",
    "bound":   3
  }'

200 OK · response.json skolem verify → exit 1

{
  "status": "divergent",
  "divergence_reason": "row presence differs",
  "counterexample_db": {
    "users":  [[1, "ada"], [2, "lin"]],
    "orders": [[10, 1, 4900]]
  },
  "query_v1_output": [[1, 1], [2, 0]],
  "query_v2_output": [[1, 1]],
  "explanation": "The rewrite turns the LEFT JOIN…"
}

Ship the rewrite with a proof attached.

Free for solo projects and open source. No database credentials required — Skolem only reads your schema and your SQL.

Run your first proof bound 1–6 · 100 runs/month free