LE PRODUIT
AI WRITES. SPARDA PROVES.
DETERMINISTIC VERIFICATION FOR AI-WRITTEN CODE.
Routes, requêtes de base de données, mutations d’état, gardes, effets de bord : tout est compilé dans un graphe unique, le Unified Behavior Graph. Les vérifications sont ensuite des passes sur ce graphe, pas des motifs cherchés dans le texte du code.
Cent pour cent local, déterministe, sans clé d’API, sans compte. L’outil signale bruyamment un risque réel, et lorsqu’il ne voit qu’une partie de l’application, il le déclare au lieu de conclure.
PAQUET
sparda-mcp — disponible publiquement sur npm
EXÉCUTION
Hors-ligne, sur votre machine. Aucune donnée ne sort.
DÉPENDANCES
Quatre, épinglées à la version exacte
TESTS
1 232 passés, 3 ignorés, sur 136 fichiers — en 31 secondes
LICENCE
Business Source License 1.1 — libre d’usage, production comprise
LE GRAPHE COMPILÉ
Le comportement déclaré devient une structure, et une structure s’inspecte. Chaque nœud est une chose que l’application dit faire ; chaque arête est un chemin qu’elle autorise.
Trois nœuds portent ici un anneau : ce sont ceux dont une obligation a été déchargée. Les autres restent des faits compilés, pas des faits prouvés — la distinction est tenue partout dans l’outil.
CE QU’IL REFUSE DE DIRE
Un outil de vérification qui annonce toujours « tout va bien » n’a aucune valeur. SPARDA distingue quatre verdicts, et le plus courant sur une vraie application n’est pas le premier.
C’est le point qui le sépare des analyseurs statiques : il ne prétend jamais avoir prouvé ce qu’il n’a pas regardé.
PROVEN
L’obligation est démontrée sur le périmètre observé.
PROVEN (PARTIAL)
Une partie seulement de l’application est visible. Jamais présenté comme un vert complet.
PREMISE NOT VERIFIED
SPARDA a prouvé qu’il ne regardait pas l’application entière. Il n’affirme alors rien du tout.
NOT_PROVEN
L’obligation n’est pas démontrée. C’est l’état vrai, pas un échec de l’outil.
LE PLUS FRÉQUENT SUR UNE APPLICATION RÉELLE
SEPT APPLICATIONS RÉELLES, LE VERDICT QU’ELLES REÇOIVENT
Le dépôt garde un instantané de son corpus, épinglé commit par commit, pour repérer ses propres régressions. Il donne aussi la réponse la plus honnête à la question « alors, ça passe ? ».
| DÉPÔT | ROUTES | VERDICT | COMMIT ÉPINGLÉ |
|---|---|---|---|
| dub | 593 | NON PROUVÉ | bbc533e · 2026-07-26 |
| twenty | 579 | NON PROUVÉ | 590ae069 · 2026-07-27 |
| nocodb | 566 | PRÉMISSE NON VÉRIFIÉE | 64bf196 · 2026-07-24 |
| novu | 451 | NON PROUVÉ | 00e7b5c · 2026-07-27 |
| immich | 281 | PARTIEL | 3606144 · 2026-07-26 |
| cal.com | 177 | NON PROUVÉ | 3894f37 · 2026-07-22 |
| ghostfolio | 115 | À RELIRE | ce35588 · 2026-07-26 |
2 762 ROUTES COMPILÉES · 7 DÉPÔTS · 0 PLANTAGE
AUCUN VERDICT « PROUVÉ » — ET C’EST LE RÉSULTAT ATTENDU
ET CE SITE-CI, ANALYSÉ PAR LE PRODUIT QU’IL PRÉSENTE
PROUVÉ
VERDICT
5
ROUTES
35
OBLIGATIONS TENUES
0
ANGLE MORT
Cinq routes d’API, aucune garde déclarée : c’est une cible facile, et le vert n’est pas un trophée. Il ne dit pas que ce site est plus sûr que cal.com. Il dit que SPARDA a vu la totalité de ce qu’on lui a donné — et c’est précisément là que se joue la différence entre les deux blocs de cette section.
seal_c2a66e65bfe91811 · 2026-08-28 · SPARDA 0.71.3 · npx sparda-mcp prove
$ structure de sortie
Aucun verdict de déploiement n’est émis
Ce que l’outil compile, ce qu’il évalue, et surtout ce qu’il ne sait pas — déclaré comme tel plutôt que passé sous silence. La décision de déployer reste au jugement d’ingénierie ; l’outil ne fournit que la matière.
LES OBLIGATIONS ÉVALUÉES
La commande apocalypse lit le graphe compilé, sans relire une ligne de code source, et décharge des obligations de correction formelles.
01
Mutation non gardée
Critique. Tout chemin de mutation qui ne traverse aucune garde de sécurité.
02
Écriture d’agrégat non atomique
Élevé. Une API qui écrit dans plusieurs tables d’un même domaine de cohérence hors d’une seule transaction.
03
Écriture contrainte non validée
Moyen. Écriture dans une colonne à invariant déclaré — CHECK, NOT NULL, UNIQUE — sans validation préalable.
04
Effet observable irréversible
Élevé. Une action hors processus, un paiement par exemple, aux côtés d’une écriture d’état sans chemin de compensation.
05
Analyse de flux teinté
Élevé. Suit les entrées non fiables à travers l’arbre syntaxique jusqu’aux points d’arrivée critiques.
06
Dominance des gardes
Moyen. Établit qu’une garde de haut niveau ne peut pas être contournée par une route imbriquée ou voisine.
07
Contournement de membre d’agrégat
Information. Mutation directe d’une table membre sans passer par la racine de l’agrégat.
LA PREUVE DE COMPILATION
SPARDA compile de véritables monstres open source vers leur graphe de comportement, sans plantage, en une à deux secondes chacun. Une seule commande les clone et refait la mesure sur votre machine.
Compiler une route est un résultat de parseur. Établir qu’elle tient une obligation est un verdict distinct, propre à chaque dépôt — la distinction est faite explicitement, elle n’est pas noyée dans un chiffre unique.
DUB
579 routes compilées en 2,05 s — Next.js
MEDUSAJS
477 routes compilées en 0,67 s
IMMICH
281 routes compilées en 1,15 s — NestJS
TOTAL
1 337 routes, 0 plantage, le plus lent à 2,05 s
BENCH/ROUTE-PROOF.JSON · 2026-07-17 · NODE v22.22.2 · SPARDA 0.71.3
LE REJEU
Un bogue qui ne se reproduit pas n’est pas un bogue résolu. Une requête de production est enregistrée avec ses effets — base, HTTP, horloge — puis rejouée hors ligne.
$ sparda-mcp timeless replay
Un appel enregistré, rejoué à l’octet près
La comparaison porte sur les octets de la réponse, pas sur une ressemblance : soit les empreintes correspondent, soit elles ne correspondent pas. Le rejeu s’exporte ensuite en test.
LES COMMANDES
prove
Le verdict complet en un geste — vérification, couverture, contrôle de prémisse et sceau partageable
apocalypse
Évaluer les obligations avant déploiement : gardes, invariants, frontières transactionnelles. Sortie SARIF et blocage d’intégration continue.
gate
Comparer le graphe avant et après une édition, et bloquer la régression dans la boucle de l’agent
heal
Réparation vérifiée : un correctif ne passe que si le rejeu correspond, que le contrôle tient et qu’aucun risque nouveau n’apparaît
timeless
Enregistrer une requête de production, la rejouer à l’octet près, exporter le bogue en test
mirror
Exécuter le graphe — servir le comportement compilé en HTTP, sans framework et sans code source
ubg
Compiler la base de code vers son graphe de comportement
badge
Un badge SVG autonome pour le README — verdict, couverture, nombre de routes
dossier
Le rapport public : une page HTML autonome, risques et angles morts compris
CE QU’IL LIT, ET COMMENT
Un outil qui refuse le faux vert doit aussi refuser le faux « compatible ». Le périmètre est donc écrit ici au même rang que le reste, avec la profondeur de chaque extracteur mesurée sur le dépôt.
LU EN PROFONDEUR — LE CODE EST COMPILÉ
Routes, gardes, écritures, effets et frontières transactionnelles sont extraits du code lui-même. C’est le périmètre sur lequel un verdict veut dire quelque chose.
NESTJS
Injection de dépendances, contrôleurs externes, décorateurs
EXPRESS 4 ET 5
Routeurs imbriqués, fabriques, points d’entrée enfouis
NEXT.JS APP ROUTER 13 À 15
Gestionnaires de route et actions serveur
STRAPI
Types de contenu, contrôleurs cœur et routes personnalisées
MEDUSAJS
Bâti sur l’extracteur Express
LU PARTIELLEMENT
Le code est parcouru, la profondeur de la famille Node n’y est pas encore.
FASTAPI
Extraction Python séparée — le périmètre reste plus étroit que la famille Node
LU PAR DÉCLARATION
C’est la spécification qui est lue, pas l’implémentation. La surface est connue ; ce qui se passe derrière ne l’est pas, et rien ne prétendra le contraire.
OPENAPI 3
Go, Java, Rails, Laravel, .NET — la surface déclarée, pas l’implémentation
BASES DE DONNÉES
Prisma, TypeORM, Kysely, Drizzle, Knex, Sequelize, Mongoose et SQL brut
EFFETS EXTERNES
fetch, axios, Stripe, Twilio, SendGrid, Resend, nodemailer, AWS SDK v3
LE PLAFOND, EN CLAIR
La profondeur se tient aujourd’hui sur la famille Node — 3 982 lignes d’extraction, contre 70 pour FastAPI. Ailleurs, SPARDA lit une surface déclarée et le dit. Le moteur ne dépend pas du cadre ; les extracteurs, si — et ils s’écrivent un par un. C’est un travail, pas une limite de conception.
SOIXANTE SECONDES
Depuis votre application, sans rien configurer :
$ npx sparda-mcp apocalypse évaluer les obligations avant un déploiement $ npx sparda-mcp prove le verdict complet : vérification, couverture, sceau $ npx sparda-mcp badge un badge README : verdict · couverture · routes