What Skolem actually proves

Given a schema S, two queries Q₁ and Q₂, and a bound k, Skolem asks Z3 for a database that satisfies S, holds at most k rows per table, and makes the two output bags differ.

divergent is absolute: a counterexample is a counterexample at any scale. equivalent is bounded — see bounds & completeness. Skolem runs z3 5.1.0.

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 $SKOLEM_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 SKOLEM_API_KEY=skm_your_key_here

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

# or verify every query your branch changed:
skolem 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.

API reference

Authentication

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

Request body

Response body

Status values

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

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.

Coverage

What the encoder handles today. Anything in the rejected column returns error — never a guess, and never a silently dropped clause.

Bag semantics

SQL returns bags, not sets. Duplicate multiplicity is part of the answer, so the encoder compares row counts per distinct tuple — not membership. Two queries returning the same rows in different multiplicities are divergent.

{(1), (1), (2)} = {(1), (2)}
-- would call these equal

count(1)=2 vs count(1)=1
-- divergent: a JOIN duplicated a row

ORDER BY is accepted and ignored — equivalence is judged on the bag, not the ordering. SELECT DISTINCT is rejected, not silently treated as a set.

Three-valued logic

Every column is encoded as a value plus an is-null flag, and predicates evaluate to true / false / unknown. A WHERE clause keeps a row only on true — this is where most LLM rewrites break.

The second row is the classic trap: negating a predicate does not recover the rows it filtered out, because NOT unknown is still unknown.

Bounds & completeness

Verification is bounded: the solver searches databases of at most k rows per table. This is the honest limit of the tool, and the reason an equivalent verdict is always reported with its bound attached.

In practice small-model bias does the work: join, grouping and NULL bugs almost always have a two- or three-row witness. Cost grows roughly boundtables joined, so a raised bound on a deep chain can exhaust the timeout and return unknown — which is not a pass.

The integer value domain is also finite, widened automatically to cover every numeric literal in the two queries. An equivalent verdict is sound within that window.

CLI flags

$ skolem verify --ddl schema.sql --v1 before.sql --v2 after.sql
$ skolem diff --base origin/main --ddl migrations/ 'queries/*.sql'

Exit codes and pipeline wiring are covered on integrations.