SPARDA

SPARDA

🇫🇷 Français — _L'IA écrit. SPARDA prouve._ Un gate déterministe et hors-ligne qui détecte quand une modif d'IA retire une garde, expose une route ou casse un invariant — sans clé API, directement dans la boucle d'édition de l'agent. Pour tout comprendre en 10 minutes (douleur, architecture, vision) : SPARDA-EXPLIQUE.md.

AI writes. SPARDA proves. L'IA écrit. SPARDA prouve.

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.

100% 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.

60-second proof

From your Express, FastAPI, Flask, Next.js, NestJS or Medusa app — nothing to configure:

npx sparda-mcp apocalypse   # prove the tree is safe to deploy — exit 1 on any real risk, or on an unverified premise

npx sparda-mcp prove # the whole verdict: proof + coverage + shareable seal npx sparda-mcp badge # a README badge: proven · coverage% · routes

Under 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) — and every command is a pass over that graph.

The wedge — catch an AI edit that removes a guard, in the loop

The 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:

npm run wedge     # (from a clone)  — or drive it on your own app with `sparda gate --arm` then `sparda gate --hook`

  1. baseline armed on the guarded code   (POST /admin/delete-user · requireAdmin)

1. an AI edit "simplifies" requireAdmin → a pass-through (still compiles, still 200s)
2. sparda gate on the edit: ✗ [critical] GUARD_REMOVED — POST /admin/delete-user was guarded in the baseline and is now reachable without any guard (src/app.js:11) ⏱ ~40 ms · deterministic · offline · no API key ⛔ exit 2 on --hook — Claude Code PostToolUse blocks the edit

Wire it into Claude Code in one line — the 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.

[!IMPORTANT]

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:

`bash

node bench/repro.mjs # → bench/route-proof.json

`

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.)

What the graph unlocks — 100% local, deterministic, 4 exact-pinned dependencies, zero API key:

The 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.

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.

Optional: expose the graph to AI clients (MCP runtime)

Beyond 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.

1. Scan + inject — run once, from your app's directory:

   npx sparda-mcp init

SPARDA parses your routes (AST), generates a marked /mcp router, injects it into your app (with a backup), and writes sparda.json. Every step is reversible.

1. Start your app, then start the bridge:

   npx sparda-mcp dev

1. Connect your client. init prints a ready-to-paste block for claude_desktop_config.json, pre-filled with your app's name and path:

   {

"mcpServers": { "your-app": { "command": "npx", "args": ["sparda-mcp", "dev"], "cwd": "/absolute/path/to/your-app" } } }

   Claude Code connects to the same bridge. That's it — your running app is now a set

of MCP tools your AI can call.

Try the Standalone Demo

To see SPARDA in action instantly without modifying your codebase:

npx sparda-mcp demo

This 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.

Black Box Report

SPARDA is designed as a local organism. To see what it remembers and how much compute it has recycled:

npx sparda-mcp report

This prints a terminal dashboard aggregating your exposed tools, write opt-ins, proof journal decisions, and crystallized composite tools.

To write a self-contained, offline HTML dashboard at .sparda/report.html, append the --html flag:

npx sparda-mcp report --html

To output raw JSON for integration:

npx sparda-mcp report --json

Deployment Proof: Apocalypse

SPARDA'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:

npx sparda-mcp apocalypse

This command reads the compiled .sparda/ubg.json (with zero source code parsing at runtime) and discharges five static correctness obligations:

• Unguarded Mutation (Critical): Flags any mutation path that does not cross a security guard.
• Non-Atomic Aggregate Write (High): Flags when an API writes to multiple tables of the same Consistency Domain (Aggregate) outside a single transaction scope.
• 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).
• 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).
• Aggregate Member Bypass (Info): Flags mutating a member table directly without routing through the aggregate root.

To save your current graph as a safe baseline:

npx sparda-mcp apocalypse --save-baseline

Subsequent runs will diff the candidate graph against this baseline to detect regression vectors:

• Deletion of any security guard (Critical).
• Deletion of a database SQL invariant (High).
• API blast radius expansion (Medium).

If any Critical or High finding is found, apocalypse exits with a non-zero code to block your CI pipeline.

One step in your workflow — findings land in the GitHub Security tab (SARIF):

- uses: zakariagharzouli/sparda@main

with: sarif: 'true'

Time Travel: Timeless

Every 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-iden