Determinism
Same inputs.
Same bits. Every time.
A safety verdict you can't reproduce is a safety verdict you can't audit. Kirra treats determinism as an engineering requirement with teeth: time is injected, concurrency is model-checked, floating point is compared bit-for-bit, and the checker core is frozen by hash.
Incident replay
Reconstruction, not simulation
Feed a captured session back through the real checker — the same
functions, the same per-class contract profiles — and every verdict must reproduce exactly:
f64::to_bits equality, no epsilon. If a single bit diverges, the tool exits non-zero.
Time never enters the verdict
The fast-loop verdict is a pure function of its inputs — which is what makes bit-identical replay
possible at all. Time-dependent flows replay through an injected VirtualClock and a
deterministic scenario runner instead.
Honest about the edges
Records without complete context — slow-loop summaries, derate-enabled sessions, locked-out spans,
NaN inputs — are classified, never guessed. And the JSON float parse is exact
(float_roundtrip), because the default parse is one ulp off and one ulp is a divergence.
crates/kirra-replay/src/lib.rsdocs/REPLAY_INCIDENT_RECONSTRUCTION.md
One command away
kirra-replay --class robotaxi session.jsonl — incident reconstruction as a CLI, exit 1 on
divergence. Regulators and integrators run the same tool we do.
Concurrency
The schedules you'll never see in a test run
Race conditions don't show up on demand. So the critical protocols are checked under tools that enumerate schedules rather than hope for them.
Loom — model-checked protocols
Four concurrency models run every interleaving CI can afford: posture generations stay unique and monotone, the cache holds the highest generation under concurrent replacement, a sticky lockout is never downgraded by a racing recalculation, and an accepted seqlock snapshot is never torn.
Miri — the memory model itself
The contract channel — the seqlock the whole enforcement path reads through — runs under Miri with multi-seed scheduling in CI, checking for undefined behavior at the Rust memory-model level, not just observable bugs.
.github/workflows/ci.yml:254crates/kirra-contract-channel/src/seqlock.rs
Formal proofs
Twelve properties, proved on the shipped source
The Kani harnesses #[path]-include the production files verbatim —
the frozen kinematics core is proved unmodified, pinned by git blob hash
ed00f4da…. No proof-friendly rewrites; no divergence between what's proved and what ships.
| Family | Properties | Domain |
|---|---|---|
| L1–L4 · HA lease algebra | TTL split is total & split-brain-safe; promotion only after holder expiry; clock skew fails safe; on-cadence renewal never expires | all u64 |
| K1–K5 · kinematics core | non-finite input always denied; non-positive dt denied; speed-ceiling clamp exact; Degraded re-initiation denied; Degraded speed increase denied | f64 is_finite case splits |
| R1–R3 · RSS primitives | longitudinal distance total; monotone in closing speed (weekly deep lane + exhaustive concrete mirror per PR); invalid brake ⇒ exact fail-safe | integer-scaled grids |
Honest scope: the P6 trigonometric path is excluded from proof (transcendentals) and covered by decision-coverage floors and property tests instead. The repository says exactly where the proofs end.
verification/kani/src/proofs_lease.rsverification/kani/src/proofs_kinematics.rsverification/kani/src/proofs_rss.rs.github/workflows/kani-deep-weekly.yml
READ THE SOURCE
Determinism you can falsify.
Clone the repo, capture a session, flip one bit — and watch the replay tool refuse it.