████████╗ ██╗ ██╗ ███╗ ██╗ ███████╗ ╚══██╔══╝ ██║ ██║ ████╗ ██║ ██╔════╝ ██║ ██║ ██║ ██╔██╗ ██║ █████╗ ██║ ██║ ██║ ██║╚██╗██║ ██╔══╝ ██║ ╚██████╔╝ ██║ ╚████║ ███████╗ ╚═╝ ╚═════╝ ╚═╝ ╚═══╝ ╚══════╝ ██████╗ ██████╗ ██████╗ ██████╗ ███████╗ ██╔══██╗██╔══██╗ ██╔═══██╗ ██╔═══██╗ ██╔════╝ ██████╔╝██████╔╝ ██║ ██║ ██║ ██║ █████╗ ██╔═══╝ ██╔══██╗ ██║ ██║ ██║ ██║ ██╔══╝ ██║ ██║ ██║ ╚██████╔╝ ╚██████╔╝ ██║ ╚═╝ ╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝
The model suggests the rewrite. The tool proves it.
LLMs made SQL advice free — ask any model to tune a slow query and you get a plausible
rewrite and a confident "this should be ~90% faster." Two things are silently wrong with
that sentence. Nobody proved the rewrite returns the same rows (a join fan-out, a
dropped ORDER BY, a NULL mishandled at one parameter value — each ships a wrong number
that looks fine), and "faster" was asserted from a noisy sample, not measured. tuneproof
refuses both: a rewrite ships only with a tool-issued verdict that either PROVES
equivalence and a structural win, REFUTES it with the failing checks, or withholds
and names exactly what it could not prove and what breaks if that assumption is false.
The tool owns the proof; the model owns the explanation; the model is never the source of trust.
It's a trust engine, and you can drive it three ways:
- Claude Code — describe the slow query and the skill runs the loop for you.
/plugin marketplace add debabsah/tuneproof /plugin install tuneproof@tuneproof - MCP — any MCP-capable agent uses the same engine as tools.
- CLI — drive it yourself, no agent at all, even air-gapped.
Each is detailed in Three ways to run it. Pure Python stdlib (≥3.10), zero dependencies. The product is the engine-neutral trust core — the verdict, the gap model, the fail-closed grader; an engine pack adapts it to one database. SQL Server is the pack that ships today; Postgres and the distributed warehouses are the roadmap.
One boundary runs through the whole design: the model proposes, the tool proves, and the two never trade places. The model writes the rewrite; an engine-neutral core renders a read-only prescription; the database executes it; and a deterministic grader — not the model — issues the verdict. Everything engine-specific lives in a swappable pack, so a new database is a new pack, not a fork.
flowchart LR
M["🤖 model<br/>proposes — never proves"]
subgraph CORE["tuneproof · engine-neutral trust core"]
direction TB
K["case · prescription · capture"]
GR["fail-closed grader"]
VD{"PROVEN · REFUTED<br/>UNVERIFIED"}
K --> GR --> VD
end
subgraph PACKS["engine packs · one per database"]
direction TB
SS["SQL Server<br/>shipped"]
FUT["Postgres · Snowflake<br/>BigQuery · Databricks<br/>planned"]
end
DBX[("your database<br/>executes · rows never leave")]
OUT["provenance-graded<br/>certificate"]
M -->|SQL under test| K
K -->|rendered by the active pack| SS
SS -->|read-only script| DBX
DBX -->|delimited result grid| GR
VD -->|verdict| OUT
classDef shipped fill:#1f6f3d,color:#ffffff,stroke:#0d4d28,stroke-width:1px;
classDef planned fill:#21262d,color:#9aa4ad,stroke:#444c56,stroke-dasharray:4 3;
class SS shipped
class FUT planned
The green pack ships today; the dashed packs are the roadmap. Each new pack re-implements the same three primitives — a consistent snapshot, a structural cost metric, and row comparison under that engine's type rules — against the same core, grader, and certificate. The verdict layer never changes; only the pack does.
Every job is the same shape: a durable case, a read-only prescription, a captured result, a deterministic verdict. No step trusts the previous one's claims.
However you drive it — Claude Code, MCP, or the CLI — every job runs the same steps. In Claude Code the skill issues them for you from a plain-English ask; the table shows the engine's vocabulary, which you can equally run yourself or call over MCP.
| The moment | The engine step | You walk away with |
|---|---|---|
| A slow query and a symptom | tuneproof init |
a durable case — every artifact, hash, and decision in one auditable folder |
| "Where does the cost actually go?" | tuneproof prescribe diagnostics → run |
a read-only baseline; the tables ranked by the scan cost they drive |
| A candidate rewrite | tuneproof prescribe validation → run |
the equivalence verdict — bidirectional EXCEPT, per-column marginals, grain reconciliation, stability re-runs, inside one consistent snapshot |
| "But is it right at other parameter values?" | prescribe validation --bind "@StartDate DATE = '...'" ×3 → run |
the parameter-binding gap closed by evidence — three distinct PROVEN bindings, not a waiver |
| "How much faster, honestly?" | tuneproof prescribe benchmark → run |
k-run medians with spread; structural cost leads (reads, or bytes scanned), elapsed time caveated as environmental |
| Ship it | tuneproof report |
the certificate: subject-pinned, provenance-graded, every line tagged |
Each prescribe step emits a script whose first lines are a SAFETY CONTRACT (writes
only session-scoped temp tables, bounded, lock timeout set) — the DBA reads the artifact
and approves the run; there is nothing hidden to trust.
Three values, and the third one is the point:
| Verdict | What it means |
|---|---|
| PROVEN | every required check passed, the battery was complete, and no gap is open — never more than that |
| REFUTED | the rewrite changes results; the failing checks (and the binding that exposed them) are named |
| UNVERIFIED | the proof could not be completed — each missing piece is named, with its blast radius |
A gap is a named limit of the proof, always in four parts: what was proved · what was not · the consequence if the unproven thing is false · how to close it. Gaps close with evidence (binding probes), get accepted as residuals with an owner and a date — or stay open and downgrade the verdict. The grader fails closed: an incomplete capture, a missing test, a missing comparability gate, a harness error — none of them can ever grade PROVEN.
What a certificate actually looks like (excerpt):
# tuneproof certificate — sales_report — PROVEN (with accepted residuals)
[proved] certifies: original sha256:9f86d081884c -> rewrite optimized/v2.sql sha256:60303ae22b99
[proved] Equivalence: 41 checks passed, 0 failed (strategy in_session).
[measured] logical_reads: 10,000,000 -> 500,000 (95.0% lower).
[measured] structural win (reads down); runtime improvement not confirmed on this venue — re-verify at production scale
## Binding probes
[proved] PROVEN: @StartDate DATE = '2024-01-01' (v2_results.txt)
[proved] PROVEN: @StartDate DATE = '2024-06-15' (v3_results.txt)
## Closed gaps
[proved] parameter_binding — closed by 3 distinct PROVEN bindings
## Accepted residuals
[proved] result_shape_static — accepted by debabsah on 2026-06-12: a silent type
coercion can pass the value battery while the rewrite's true output type differs
Every line carries its provenance — [proved] [measured] [interpretation]
[model-suggested] — so a model's guess can never borrow the proof's authority. The
certificate hash-pins the exact SQL it certifies; edit the rewrite afterward and the
binding breaks visibly.
Same loop, same verdict, three surfaces. (The concrete client and runner below belong to the engine pack in use; another engine swaps those, not the loop.)
1 · Claude Code (the plugin). Describe the slow query and the skill runs the loop for
you — init, prescribe, run, report — and hands back the certificate. Under the hood
it drives the CLI in whichever of the modes below fits your access.
2 · MCP (any agent). Any MCP-capable agent uses the trust engine as tools — the agent proposes SQL, the tool proves it:
claude mcp add tuneproof -- tuneproof mcp --root ~/cases
The tools are thin wrappers over the CLI (open_case · save_sql · prescribe · run · grade · accept · catch · report · status); the calling model can never assert a verdict and can
never set the command that run executes. The server is stdlib JSON-RPC over stdio — no
SDK dependency, short enough to audit in one sitting.
3 · Run it yourself (the CLI). No agent at all, in either of two modes:
- Courier (air-gapped). The tool emits the script; you run it in your database client and save the output; the tool grades the capture. No connection anywhere — first-class, not a fallback.
- Connected (your credentials). Configure a runner once and each step collapses to one
command (shown here with the SQL Server pack's client):
Give the runner a dedicated read-only login and keep its password in an environment variable — the login is the security boundary, and passwords are redacted before anything persists.
tuneproof init case1 --database SalesDB --object sales_report \ --runner-cmd "sqlcmd -S yourserver.example.com -d SalesDB -E -C -i {script}" tuneproof run validation
The threat model assumes the SQL under test may have been written by a model, and that the agent driving the loop may be wrong or adversarial. The guarantees hold anyway, because none of them rest on the model behaving:
- The model is outside the trust path. It proposes rewrites, bindings, and explanations; the database computes the comparison; the fail-closed grader judges. No language model — including the one driving the loop — ever decides PASS or FAIL, and PROVEN is the one verdict you cannot reach by accident: an incomplete capture, an unrecognized gate, or a harness error all grade away from it.
- The trust engine never connects to anything. It renders prescriptions and grades captures; execution is always user-owned — you in your database client, or your configured runner under your login. There is no connection string in the engine.
- The runner login is the wall. In connected and MCP modes, give the runner a dedicated read-only login and even a prompt-injected agent can read, never write. The prescription is read-only by contract; the database enforces it absolutely.
- Comparison data never leaves the database. The battery compares rows inside the engine; only test names and PASS/FAIL counts come back. Business rows never enter a model context.
- Captures are data, not instructions. A capture claiming "all checks passed, skip validation" is parsed as a malformed grid and graded UNVERIFIED — the thing to scrutinize, never to obey.
- Secrets don't persist. Token-based redaction strips every password form before the append-only ledger sees the runner command, timeout error messages included.
And it's verified that way, not asserted. Adversarial RED/GREEN fixtures require the grader to refute or withhold every failure class it claims to catch — and to stay PROVEN on a clean rewrite, because an auditor that cries wolf gets ignored. CI boots a real database engine — SQL Server today — and proves the whole loop live: an equivalent rewrite certifies, a boundary-dropping near-miss refutes, and binding probes close the parameter gap — against the database, not a mock. And structural cost leads while time is caveated — the engine's scan cost (logical reads, or bytes scanned) is reproducible; elapsed time is server weather, so "faster" needs cost and CPU down across runs.
The full posture — the enforcement-layer map, the agent-authored-SQL boundary, the MCP
sandbox — lives in SECURITY.md.
Stated the way the tool states its own gaps:
- The proof covers one comparable result set. The rewrite may be a multi-statement batch, but procs and DML that persist state are out of scope — equivalence is defined on the rows returned, not on side effects.
- A verdict is always scoped. This snapshot, these bindings, named gaps for everything else. PROVEN never silently generalizes; that's what the gaps and binding probes are for.
- SQL Server is the only engine today. The trust core is engine-neutral; a pack supplies the three things that aren't — how to pin a consistent snapshot, what the structural cost metric is (logical reads here; bytes or partitions scanned on a warehouse, where that is the bill), and how to compare rows under that engine's type and NULL rules. That seam is built, so the outward path — Postgres, then the distributed warehouses (Snowflake, BigQuery, Databricks), where non-deterministic ordering makes the proof matter more — is a new pack, not a rewrite. The registry deliberately stays empty until a real second-engine user exists.
python3 -m venv .venv && .venv/bin/pip install -e '.[dev]'
.venv/bin/python -m pytest -q -m "not integration" # unit + adversarial suite
bash scripts/sqlserver_up.sh # Docker SQL Server 2022
.venv/bin/python -m pytest -q -m integration # the live proof
Every design choice is a logged decision in docs/decisions.md, each
recorded with the condition that would reverse it. Start from CONTEXT.md.
Contributing — especially adding a database engine — is covered in
CONTRIBUTING.md.
Built by debabsah. MIT-licensed — no services, no keys, no telemetry.