Prediction

Judged where they'll be,
not where they are.

Snapshot RSS evaluates an object at its current position — and quietly misses the cut-in that hasn't happened yet. Kirra's predictive pass rolls every motion hypothesis forward in time and checks it against the time-matched ego pose. One dangerous future is enough to say no.

Multi-modal RSS · ADR-0017

Worst case over modes, fail-closed per mode

Each tracked object produces predicted modes: constant-velocity always, and constant-turn-rate when the tracker's yaw feed is fresh. A stale yaw degrades gracefully to CV-only — a data quality problem, not a fault. But evaluability is judged per mode: a mode whose samples fall outside the ego trajectory's time span resolves to a minimum-risk fallback, so one object's evaluable hypothesis can never mask another's unevaluable one.

Multi-modal predictive RSS A tracked object spawns two motion hypotheses: constant velocity, straight ahead, and constant turn rate, curving toward the ego lane. Each mode is rolled forward in time and checked against the time-matched ego pose. The curving hypothesis breaches RSS in the future, so the trajectory is refused now. ego trajectory → ego t₀ ego t₁ object t₀ CV mode — stays clear ✓ CTRV mode — cuts in at t₁ ✗ one dangerous hypothesis ⇒ the whole trajectory is refused

crates/kirra-trajectory/src/prediction.rs:199crates/kirra-trajectory/src/validation.rs:999docs/adr/0017-multi-modal-predictive-rss.md

The RSS core

Danger requires both dimensions

A collision needs an object to be unsafe longitudinally and laterally at once — RSS §4's conjunction. The lateral check fires only when abreast or on a closing cut-in, which is what lets the ego calmly hold behind a stopped queue instead of over-rejecting every stationary object on the street.

Published primitives, open code

longitudinal_safe_distance, split lateral distances, opposite-direction terms, and occlusion-limited speed — the formal RSS repertoire implemented in plain Rust, with the §4 conjunction carrying its own written proof note.

parko/crates/parko-core/src/rss.rs:317docs/safety/RFC_2846_SECTION_4_PROOF.md

Machine-checked properties

Kani proves totality of the longitudinal distance over integer-scaled grids (R1), the closing-speed monotonicity the occlusion bisection relies on (R2, weekly deep lane with an exhaustive concrete mirror gating every PR), and exact fail-safe behavior on invalid braking parameters (R3).

verification/kani/src/proofs_rss.rs.github/workflows/kani-deep-weekly.yml

Occlusion is Rule 4

What you cannot see is modeled as the worst thing it could be: approach speed at blind junctions is capped to the assured-clear-distance bound for that lane's sight distance, carried on the map itself.

parko/crates/parko-core/src/rss.rs:454docs/adr/0016-occlusion-aware-junction-speed-bound.md

Interaction models

Gap acceptance without mind-reading

Unprotected turns use explicit gap-acceptance decision records — including a Stackelberg observed-cooperation model where the ego commits only on observed yielding, never assumed politeness. Design decisions, argued in the open, with their limits stated.

docs/adr/0021-unprotected-turn-gap-acceptance.mddocs/adr/0026-stackelberg-interaction-model.mddocs/adr/0022-permitted-vs-protected-turns.md

READ THE SOURCE

Prediction is a bound, not a guess.

Every hypothesis the checker can't evaluate resolves toward stillness — read the per-mode fail-closed logic yourself.

View the repository Browse the documentation