Make the proof a required check.
Run Skolem on every pull request that touches SQL. If a rewrite diverges from the query it replaces, the step exits non-zero and the counterexample database is printed in the job log — before review, not after deploy.
A thin Python client over the API — httpx
is its only dependency. The solver runs server-side, so the runner stays light.
Mint a key on the API Keys page and store it as a CI secret. The same variable works for the CLI and the MCP server.
Mark the job as a required check and SQL that diverges from the query it replaces can no longer merge.
Wiring
// whichever runner you use# .github/workflows/sql-proof.yml — using the packaged action name: sql-proof on: [pull_request] jobs: prove: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 with: fetch-depth: 0 # diff needs the merge base - uses: NguyenTienDat377/SQLVerify/action@main with: ddl: migrations/ glob: 'queries/*.sql' base: ${{ github.event.pull_request.base.sha }} api-key: ${{ secrets.SKOLEM_API_KEY }}
# .gitlab-ci.yml sql-proof: image: python:3.12-slim rules: - if: $CI_MERGE_REQUEST_IID variables: GIT_DEPTH: "0" # diff needs the merge base script: - pip install pipx && pipx install ./cli - | skolem diff \ --base origin/$CI_MERGE_REQUEST_TARGET_BRANCH_NAME \ --ddl migrations/ 'queries/*.sql' \ --output json > proof.ndjson artifacts: paths: [proof.ndjson] when: always
# any runner, any shell pipx install ./cli export SKOLEM_API_KEY=skm_your_key_here # one explicit pair skolem verify --ddl schema.sql --v1 before.sql --v2 after.sql # or every query the branch changed skolem diff --base origin/main --ddl migrations/ 'queries/*.sql' # stricter gate: treat unknown and error as failures too skolem diff --base origin/main --ddl migrations/ 'queries/*.sql' \ --fail-on divergent,unknown,error
skolem diff derives the pairs from git:
each changed file is compared against its own content at
git merge-base --base HEAD, so the same
command gives the same answer locally on a dirty tree and in CI after
checkout. That's why the checkout needs full history — with a shallow
clone there is no merge base to diff against. The packaged
GitHub Action
is a composite action that installs and calls the same CLI — nothing it
does isn't also available as the plain workflow step above.
Exit codes
Gate on the exit code, or parse the JSON on stdout. The split that matters is verdict versus infrastructure.
| 0 | gate passed — every pair satisfied --fail-on |
| 1 | gate failed — a verdict matched --fail-on (by default, divergent) |
| 2 | the CLI itself failed — bad flags, unreadable file, network, 401, 402, 429 |
A lapsed key or a network blip exits 2, never 1. A gate that reports a broken pipeline as a broken query is a gate people learn to ignore. Across many files the worst code wins: 2 beats 1 beats 0.
Choosing a policy
--fail-on defaults to
divergent alone.
unknown and
error warn loudly and pass.
Fail-closed is right for the verifier — a wrong verdict is
fatal, so unsupported SQL is rejected outright. It's wrong for the
gate: a check that reddens the first time someone writes a
CTE gets uninstalled by the end of the week. An
unknown always prints "not a proof
of equivalence", so it can never read as a pass. Strict teams opt in
with --fail-on divergent,unknown,error.
Every run counts against your monthly quota, including
unknown and
error — see pricing.
AI agents (MCP)
// verification in the generation loopExpose verification as a tool to Claude Code, Claude Desktop, or Cursor. The agent proposes a rewrite, gets back a proof or a concrete counterexample, and revises against ground truth instead of guessing — the counterexample-driven repair loop.
{
"mcpServers": {
"skolem": {
"command": "/abs/path/to/Skolem/mcp/.venv/bin/python",
"args": ["/abs/path/to/Skolem/mcp/skolem_mcp.py"],
"env": {
"SKOLEM_API_KEY": "skm_your_key_here",
"SKOLEM_URL": "https://sqlverify.com"
}
}
}
}
# the MCP server is standalone — its own venv, # and it never imports the solver cd mcp python -m venv .venv .venv/bin/pip install -r requirements.txt # same env vars as the CLI, one setup for both export SKOLEM_API_KEY=skm_your_key_here export SKOLEM_URL=https://sqlverify.com
Wire it into one repo tonight.
Install the CLI, add a secret, make the job required. Free while you evaluate.