![\"SPARDA](\"assets/sparda-readme-banner-dark-1600x480.png\")
\n\nL'IA écrit. SPARDA prouve.
\n\n**The trust layer for AI-written backends.** SPARDA compiles your backend — routes, database queries, state mutations, guards, side-effects — into one deterministic behavior graph, then **statically proves what can and can't break before you ship**: no unguarded mutation, no broken invariant, no non-atomic aggregate write.\n\n[](https://www.npmjs.com/package/sparda-mcp)\n[](https://github.com/zakariagharzouli/sparda/actions/workflows/ci.yml)\n\n\n[](./LICENSE)\n\n100% local · deterministic · zero API key · no cloud account. It fails loudly on a real risk, and when it can only see part of your app it says **PROVEN (PARTIAL)** — never a false green. And when it can prove it was not even looking at your whole app, it says **PREMISE NOT VERIFIED** and claims nothing at all.\n\n## 60-second proof\n\nFrom your Express, FastAPI, Flask, Next.js, NestJS or Medusa app — nothing to configure:\n\n```bash\nnpx sparda-mcp apocalypse # prove the tree is safe to deploy — exit 1 on any real risk, or on an unverified premise\nnpx sparda-mcp prove # the whole verdict: proof + coverage + shareable seal\nnpx sparda-mcp badge # a README badge: proven · coverage% · routes\n```\n\nUnder the hood it compiles your backend into one language-agnostic graph — the **Unified Behavior Graph (UBG)**, serialized as `.sparda/ubg.json` under the **SBIR** specification ([SPARDA Behavior IR](docs/SBIR_SPEC_V1.1.md)) — and every command is a pass over that graph.\n\n## The wedge — catch an AI edit that removes a guard, in the loop\n\nThe one thing a text-diff review and a pattern scanner structurally can't do: prove that **this specific edit** dropped a protection the previous version had. `sparda gate` diffs the behavior graph before/after an edit and blocks a regression — deterministic, offline, sub-second, exit 2 (the Claude Code `PostToolUse` contract that stops the agent's edit loop). See it end-to-end in one command, zero setup:\n\n```bash\nnpm run wedge # (from a clone) — or drive it on your own app with `sparda gate --arm` then `sparda gate --hook`\n```\n\n```\n 1. baseline armed on the guarded code (POST /admin/delete-user · requireAdmin)\n 2. an AI edit \"simplifies\" requireAdmin → a pass-through (still compiles, still 200s)\n 3. sparda gate on the edit:\n ✗ [critical] GUARD_REMOVED — POST /admin/delete-user was guarded in the baseline\n and is now reachable without any guard (src/app.js:11)\n ⏱ ~40 ms · deterministic · offline · no API key\n ⛔ exit 2 on --hook — Claude Code PostToolUse blocks the edit\n```\n\n**Wire it into Claude Code in one line** — the [plugin](integrations/claude-code-plugin) registers a `PostToolUse` hook that runs `npx -y sparda-mcp gate --hook` after every `Edit`/`Write`, so a guard-removing edit is caught before it lands.\n\n> [!IMPORTANT] \n> **The Route-Compilation Proof — reproduce it yourself.** SPARDA compiles real open-source monsters to their behavior graph with **zero crashes**, each in **≈1–2 seconds**: Next.js _Dub_ (579 routes), NestJS _Immich_ (281), _MedusaJS_ (477). It natively resolves deep Dependency Injection, external controllers, and Next.js handlers. One command clones them and re-measures on your machine:\n>\n> ```bash\n> node bench/repro.mjs # → bench/route-proof.json\n> ```\n>\n> Honesty first: _compiling_ a route is a parser result (the number above); _proving_ it safe is a separate per-repo verdict — and most real apps come back **NOT_PROVEN**, which is the true state, not a failure. (Our full 25-repo corpus stress compiles **3,565 routes** at ~150 routes/s; that one needs the corpus checked out.)\n\n**What the graph unlocks — 100% local, deterministic, 4 exact-pinned dependencies, zero API key:**\n\n| Command | What it does |\n| ------------------ | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |\n| **`prove`** | _The whole trust verdict in one gesture_ — proof + coverage + premise check + a shareable seal (`--json` / `--markdown`) |\n| **`apocalypse`** | _Prove the deploy_ — no guard, invariant, transaction or aggregate boundary can be broken (SARIF + CI gate) |\n| **`heal`** | _Self-heal, **proven**_ — the gate Copilot Autofix doesn't have: a fix ships **only if** replay matches, `verify` still passes, and `apocalypse` finds no new risk / no dropped guard. Whoever wrote the fix, the machine judges it. |\n| **`badge`** | _The shareable artifact_ — a self-contained SVG badge + README snippet (verdict · coverage · routes) |\n| **`dossier`** | _The public report_ — one self-contained HTML page: verdict, risks, and SPARDA's own blind spots |\n| **`ubg`** | Compile the codebase to its behavior graph (Express · FastAPI · Flask · Next.js · NestJS · Medusa natively; **any** stack via OpenAPI) |\n| **`timeless`** | _Time-travel_ — record a production request, replay it byte-identically, export the bug as a test |\n| **`mirror`** | _Execute the graph_ — serve the compiled behavior over HTTP with no framework and no source |\n| **`init` / `dev`** | _Runtime, optional_ — expose the graph to AI clients as a live MCP server (+ Twin, Immune, Evolution) |\n\nThe prover is the product. The MCP server is one _output_ of the graph, not the point — SPARDA compiles the whole system's behavior, then proves, replays, heals, and (optionally) serves it.\n\n**Nomenclature:** **SBIR** is the specification (the format, like \"JSON\"); **UBG** is the compiled graph itself (the artifact, `ubg.json`). The MCP server is one _output_ of the graph, not the product.\n\n## Optional: expose the graph to AI clients (MCP runtime)\n\nBeyond proving, SPARDA can turn your running app into a live MCP server — the graph, executable, with write-safety and an immune layer. This is optional and separate from the prover above.\n\n1. **Scan + inject** — run once, from your app's directory:\n\n ```bash\n npx sparda-mcp init\n ```\n\n SPARDA parses your routes (AST), generates a marked `/mcp` router, injects it into\n your app (with a backup), and writes `sparda.json`. Every step is reversible.\n\n2. **Start your app, then start the bridge:**\n\n ```bash\n npx sparda-mcp dev\n ```\n\n3. **Connect your client.** `init` prints a ready-to-paste block for\n `claude_desktop_config.json`, pre-filled with your app's name and path:\n ```json\n {\n \"mcpServers\": {\n \"your-app\": {\n \"command\": \"npx\",\n \"args\": [\"sparda-mcp\", \"dev\"],\n \"cwd\": \"/absolute/path/to/your-app\"\n }\n }\n }\n ```\n Claude Code connects to the same bridge. That's it — your running app is now a set\n of MCP tools your AI can call.\n\n## Try the Standalone Demo\n\nTo see SPARDA in action instantly without modifying your codebase:\n\n```bash\nnpx sparda-mcp demo\n```\n\nThis runs the entire MCP lifecycle (detect → parse → generate → inject → remove) on a bundled demo app in a temporary folder, in about 10 seconds. For the compiler itself, run `npx sparda-mcp ubg` then `apocalypse` on any Express/FastAPI app.\n\n## Black Box Report\n\nSPARDA is designed as a local organism. To see what it remembers and how much compute it has recycled:\n\n```bash\nnpx sparda-mcp report\n```\n\nThis prints a terminal dashboard aggregating your exposed tools, write opt-ins, proof journal decisions, and crystallized composite tools.\n\nTo write a self-contained, offline HTML dashboard at `.sparda/report.html`, append the `--html` flag:\n\n```bash\nnpx sparda-mcp report --html\n```\n\nTo output raw JSON for integration:\n\n```bash\nnpx sparda-mcp report --json\n```\n\n## Deployment Proof: Apocalypse\n\nSPARDA's Behavior Graph is a formal model of your system. Instead of waiting for runtime failures or relying on static analysis vibes, you can statically prove the safety of your backend before any deployment:\n\n```bash\nnpx sparda-mcp apocalypse\n```\n\nThis command reads the compiled `.sparda/ubg.json` (with zero source code parsing at runtime) and discharges five static correctness obligations:\n* **Unguarded Mutation (Critical)**: Flags any mutation path that does not cross a security `guard`.\n* **Non-Atomic Aggregate Write (High)**: Flags when an API writes to multiple tables of the same Consistency Domain (Aggregate) outside a single transaction scope.\n* **Unvalidated Constrained Write (Medium)**: Flags writes into columns with declared invariants (CHECK, NOT NULL, UNIQUE — parsed from your `.sql` DDL **or `schema.prisma`**, Prisma enums included) without prior validation (Zod/Pydantic).\n* **Irreversible Observable Effect (High)**: Flags out-of-process actions (like Stripe charges) that happen alongside state writes without a structural compensation path (like a catch-refund).\n* **Aggregate Member Bypass (Info)**: Flags mutating a member table directly without routing through the aggregate root.\n\nTo save your current graph as a safe baseline:\n\n```bash\nnpx sparda-mcp apocalypse --save-baseline\n```\n\nSubsequent runs will diff the candidate graph against this baseline to detect regression vectors:\n* Deletion of any security `guard` (Critical).\n* Deletion of a database SQL invariant (High).\n* API blast radius expansion (Medium).\n\nIf any Critical or High finding is found, `apocalypse` exits with a non-zero code to block your CI pipeline.\n\n**One step in your workflow — findings land in the GitHub Security tab (SARIF):**\n\n```yaml\n- uses: zakariagharzouli/sparda@main\n with:\n sarif: 'true'\n```\n\n## Time Travel: Timeless\n\nEvery production request is deterministic between its effects — the compiler knows exactly where the nondeterminism lives (db, http, clock, random, uuid: the effect nodes of the graph). Timeless records only those points (a few KB per request) and replays the request **byte-identically** against your current code, with the database, webhooks and clock virtualized from the recording:\n\n```bash\nnpx sparda-mcp timeless # list recorded flights\nnpx sparda-mcp timeless replay![\"SPARDA](\"assets/features-presentation.png\")
\n![\"Leave](\"assets/github-star.png\")
\n