tuneproof

<pre> ████████╗ ██╗ ██╗ ███╗ ██╗ ███████╗ ╚══██╔══╝ ██║ ██║ ████╗ ██║ ██╔════╝ ██║ ██║ ██║ ██╔██╗ ██║ █████╗ ██║ ██║ ██║ ██║╚██╗██║ ██╔══╝ ██║ ╚██████╔╝ ██║ ╚████║ ███████╗ ╚═╝ ╚═════╝ ╚═╝ ╚═══╝ ╚══════╝ ██████╗ ██████╗ ██████╗ ██████╗ ███████╗ ██╔══██╗██╔══██╗ ██╔═══██╗ ██╔═══██╗ ██╔════╝ ██████╔╝██████╔╝ ██║ ██║ ██║ ██║ █████╗ ██╔═══╝ ██╔══██╗ ██║ ██║ ██║ ██║ ██╔══╝ ██║ ██║ ██║ ╚██████╔╝ ╚██████╔╝ ██║ ╚═╝ ╚═╝ ╚═╝ ╚═════╝ ╚═════╝ ╚═╝ </pre> [](https://github.com/debabsah/tuneproof/actions/workflows/ci.yml) [](https://www.python.org/downloads/) [](LICENSE) [](https://claude.com/claude-code) **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](#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. --- ## Architecture 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. ```mermaid 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. ## The loop 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. ## The verdict is the product 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): ```text # 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. ## Three ways to run it 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): ``` tuneproof init case1 --database SalesDB --object sales_report \ --runner-cmd "sqlcmd -S yourserver.example.com -d SalesDB -E -C -i {script}" tuneproof run validation ``` 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. ## Why you can trust the verdict 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`](SECURITY.md). ## Honest limits 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. ## Develop ``` 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`](docs/decisions.md), each recorded with the condition that would reverse it. Start from [`CONTEXT.md`](CONTEXT.md). Contributing — especially **adding a database engine** — is covered in [`CONTRIBUTING.md`](CONTRIBUTING.md). --- ## Author & license Built by [debabsah](https://github.com/debabsah). MIT-licensed — no services, no keys, no telemetry.