Verdict playground

The real checker.
Running in your browser.

This is not a demo that imitates the checker — it IS the checker. The frozen kinematics-contract source (git blob ed00f4da…) is included verbatim, compiled to 54 KB of WebAssembly, and loaded into this page. The same file the Kani proofs verify. Propose a command; the envelope decides.

Propose a command

Values accept NaN and Infinity — the checker certainly does not.

loading checker…

Try an attack:

What you're running

The WASM module #[path]-includes crates/kirra-core/src/kinematics_contract.rs verbatim — the same fidelity pattern the Kani proofs use, so the frozen file is never modified. The shim only marshals numbers across the boundary; the class profiles mirror the normative table in docs/CONTRACT_PROFILES.md, and Degraded runs the talisman's own MRC fallback profile (ADR-0012). The crate's native test suite runs the talisman's 47 embedded unit tests plus shim mirrors of everything this page demonstrates.

tools/wasm-verdict/src/lib.rscrates/kirra-core/src/kinematics_contract.rsverification/kani/src/proofs_kinematics.rs

Honest scope: this page runs the kinematic envelope and Degraded decel-to-stop gate — one layer of the full checker. In production the same command would also face posture routing, RSS and containment over the whole trajectory, and the Ed25519 verify-before-release chain at the actuator. The playground shows the innermost wall, not the whole fortress.

Verified fidelity

Don't trust the page. Diff the blob.

The talisman's git blob hash is pinned in CI — the file this page compiles is bit-identical to the one the fleet runs and the proofs verify.

Read the talisman Why determinism matters