sparda_prove
Compile source behavior, discharge static proof obligations, and return a deterministic verdict with coverage. Optionally filter findings by route and compare against a saved baseline to detect regressions.
Instructions
Prove this app is safe to deploy — NOW, before you commit. Compiles the current source to its behavior graph and discharges the static proof obligations (unguarded mutation, non-atomic aggregate write, unvalidated constrained write). If a baseline was saved (sparda apocalypse --save-baseline), it ALSO diffs against it: any finding flagged regression:true means your edit removed a guard, dropped a route, or grew the blast radius vs the last proven state — the check an LLM cannot do to itself by re-reading code. Returns a deterministic verdict (PROVEN / PARTIAL / SURFACE / NO_PROOF / RISKY / NOT_PROVEN), the coverage % it resolved, and every finding with its route. The verdict is the exact word sparda apocalypse and the badge emit; it never over-claims (a low-coverage clean app reads SURFACE/PARTIAL, never a bare PROVEN). Pass route (e.g. "DELETE /orders") to focus the finding list on the route you just edited — the verdict still reflects the whole app.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| route | No | Optional. Substring of a route label (method + path, e.g. "POST /invoices") to filter the findings to the route you just edited. Omit to see the whole app. |