Safety model

Fail closed.
Recover deliberately.

Kirra's safety model is three postures and a promise: when anything is unproven — a node unattested, a sensor silent, a cache stale, a command unclassified — the system moves toward stillness, and it never talks itself back into motion.

Posture state machine

Three states. Asymmetric exits.

Getting into a safe state is automatic and fast. Getting out is slow and evidence-gated: Degraded recovers only after five consecutive healthy reports inside a ten-second window, and LockedOut recovers only through a human. Down is easy; up requires proof.

Fleet posture state machine Nominal transitions to Degraded on a sensor fault or confidence drop, and recovers automatically after five consecutive healthy reports inside a ten-second window. Nominal or Degraded transition to LockedOut on attestation failure, dependency cycle, or stale posture. LockedOut requires operator clearance to exit — recovery is never a timer. NOMINAL all classified commands admitted DEGRADED decel-to-stop-and-hold LOCKED OUT every command denied fault · low confidence 5 healthy reports / 10 s window attestation fail · cycle · stale trust violation ⇒ direct lockout operator clearance only — never a timer

src/recovery_hysteresis.rssrc/verifier.rsdocs/safety/SAFE_STATE_SPECIFICATION.md

The Degraded contract

Degraded is not a crawl.
It is a controlled stop.

Motivated by the October 2023 Cruise incident — a post-collision pullover executed at ~3 m/s under a 5 m/s “crawl ceiling” — Kirra's Degraded posture admits a command only if it converges to a stop. The governor never authors re-acceleration.

Three conditions, all required

(a) inside the minimum-risk decel envelope; (b) non-increasing speed — |proposed| ≤ |current|; (c) no re-initiation: once at rest (≤0.05 m/s), any command to move again is denied and the vehicle holds. A reversal through zero counts as re-initiation.

crates/kirra-core/src/kinematics_contract.rsdocs/safety/SAFE_STATE_SPECIFICATION.md

Enforced at four points

The same decel-to-stop gate runs at the HTTP actuator gateway, the fabric asset governor, the ROS 2 trajectory validator, and the parko MRC profile — which also gates the independent angular-velocity channel for differential drive.

docs/adr/0011-degraded-http-actuator-503-vs-decel-gate.mdtests/posture_gate_integration.rs

Machine-checked

Kani proofs K4 and K5 verify — over exhaustive f64 case splits — that Degraded re-initiation and speed increases are denied. Not tested on samples: proved on the domain.

verification/kani/src/proofs_kinematics.rs:166

Two meanings of “MRC,” kept deliberately distinct: Degraded's MRC is a decel-to-stop envelope that bounds a converging command; LockedOut's MRC is a safe-stop maneuver while all commands are denied. The safe-state specification (KIRRA-SSS-001) assigns each to a fault-severity class, with a 5.0 m/s MRC velocity ceiling.

Liveness

Silence is a fault

A safety system that only reacts to bad messages misses the worst failure of all: no message. Kirra's watchdogs treat absence as evidence.

SignalThresholdConsequence
AV telemetry silence1,000 ms warn · 2,000 ms faultNode marked untrusted; posture recomputed (sweep every 100 ms)
Posture cache age> 5,000 msRouting fails closed — treated as LockedOut
Attestation nonce age> 30,000 msChallenge expires; proof must restart
Federation report age> 5,000 msReport rejected (replay window)
Armed-but-silent VRU channelfreshness budgetMRC-floor speed cap — the ego stops rather than drives blind

src/telemetry_watchdog.rssrc/posture_cache.rscrates/kirra-trajectory/src/vru_channel.rs

Per-class envelopes

No default vehicle class

A sidewalk courier and a robotaxi must not share an envelope. The vehicle class is mandatory configuration — unset, empty, or unknown aborts startup, because a wrong class would select another class's physics. Every number below is normative in the repository and marked validation-pending until signed off.

LimitCourier (sidewalk)Delivery AV (road pod)Robotaxi (frozen ref.)
Max speed3.0 m/s12.0 m/s35.0 m/s
ODD speed cap2.5 m/s11.0 m/s22.35 m/s
Braking decel3.0 m/s²4.0 m/s²4.5 m/s²
Lateral accel1.5 m/s²2.5 m/s²3.5 m/s²
RSS lateral band0.6 m2.0 m4.0 m

docs/CONTRACT_PROFILES.mdsrc/gateway/contract_profiles.rsdocs/adr/0028-sidewalk-courier-odd.mddocs/adr/0001-occy-odd-speed-cap.md

Invariants

Rules that have survived being attacked

The repository maintains a list of security invariants that submissions have repeatedly tried to weaken — and that are rejected outright. A few of the load-bearing ones:

Envelope cap beats rate limits

The governor clamps to the absolute hard boundary first, then applies rate-of-change limits. The envelope always wins.

Unknown is denied everywhere

The Unknown command class is denied in all postures — including Nominal. The early return is never removed.

Attestation is never mocked

Trust requires a per-node Ed25519 proof over a fresh challenge, checked against the registered key. No registered key, malformed proof, bad signature — rejected.

Actuator topics never replay

DDS actuator topics must use Volatile durability, so a reconnecting subscriber can never receive a stale command as if it were fresh.

SECURITY.mddocs/v1_security_invariants.mdsrc/startup_sentinel.rs

READ THE SOURCE

Read the safe-state specification.

KIRRA-SSS-001 assigns a safe state to every fault-severity class — and the repository's tests hold the code to it.

View the repository Browse the documentation