Pattern scanners tell you a route looks unguarded; this tells you a route that *was* guarded no longer is, by comparing two compiled graphs. That framing also explains why it is honest about coverage — most real apps come back not proven, and the author says so rather than reporting a green. Worth noting the runtime and the prover are separable: the prover needs nothing installed in your app, while the MCP runtime injects a router into it.
A prover for AI-written backends, with an MCP server as one of its outputs. It compiles routes, database queries, state mutations, guards and side-effects into a single behaviour graph, then statically discharges correctness obligations against it. Everything runs locally and deterministically with four exact-pinned dependencies and no API key. Express, FastAPI, Flask, Next.js, NestJS, Strapi and Medusa are parsed natively; anything else compiles from an OpenAPI spec.
- A gate that catches the specific failure a text diff cannot: `sparda gate` diffs the behaviour graph before and after an edit and blocks a guard that was there and is now gone, exiting 2 so a Claude Code `PostToolUse` hook stops the edit loop
- Static proof obligations before deploy — unguarded mutation, non-atomic aggregate write across one consistency domain, unvalidated write into a column with a declared invariant, an irreversible external effect with no compensation path, taint flow from untrusted input into a critical sink, guard dominance, and aggregate member bypass
- Verdicts that refuse to over-claim: `PROVEN (PARTIAL)` when only part of the app is visible, and `PREMISE NOT VERIFIED` when it can prove it was not looking at the whole app, in which case it claims nothing
- Request replay — record a production request, replay it byte-identically against current code with the database, webhooks and clock virtualised, and export the bug as a test
- An MCP runtime that turns every route into a tool running inside your live app process, with `sparda_get_context` returning enabled tools, workflows, telemetry and quarantine state in one call, and `sparda_prove` recompiling and returning the same verdict the CLI emits — inside the edit loop rather than in a later CI run
- Write-safety on that runtime: POST, PUT and DELETE tools ship disabled, you enable them per tool, and an enabled write is never executed on the first call — it returns an `awaiting_confirmation` envelope with a single-use token and a preview, then reads the resource back after committing
- Self-defence with no model on the hot path: a tool returning three consecutive 5xx is quarantined behind a 503 with a retry delay, and latency deviations are flagged locally
- A mirror VM that serves the compiled graph over HTTP with no framework and no source code, so front-end teams can develop against a backend that is not deployed yet
No account and no API key; nothing leaves your machine. Node 18 or newer. Run it straight from npm — `npx sparda-mcp apocalypse` to prove the tree, `npx sparda-mcp prove` for the full verdict — with the package published as `sparda-mcp`. For the MCP runtime, `npx sparda-mcp init` parses your routes, generates a marked `/mcp` router and injects it into your app with a backup, then `npx sparda-mcp dev` starts the bridge; `init` prints a ready-to-paste client config block. Every step is reversible: `npx sparda-mcp remove` restores your code byte-for-byte. The generated router bakes in no secret — it resolves its key at runtime from `SPARDA_LOCAL_KEY` or a gitignored local key file and fails closed with a 503 when neither is present. `SPARDA_FLYWHEEL` and `SPARDA_RECORD_SEQUENCES` are optional. Business Source License 1.1: free to use including in production, no reselling, and each version converts to Apache 2.0 four years after release.
One command — npx sparda-mcp dev