Architecture

Small enough to prove.
Isolated enough to trust.

Kirra's architecture is one long argument for isolation: untrusted doers in their own partition, a minimal verdict core at the boundary, and a control plane that assumes every carrier is hostile. Here is how the pieces fit — with the decision records that shaped them.

Deployment topology

The partition is the safety argument

The decision of record (ADR-0032): the governor runs as the safety-domain payload on QNX Hypervisor 8.0 for Safety, with the entire ROS 2 / Autoware doer stack as an isolated guest VM. The only thing that crosses the boundary is a frozen, pointer-free #[repr(C)] struct.

Deployment topology (ADR-0032) A QNX Hypervisor hosts two partitions: an untrusted guest VM running the ROS 2 or Autoware doer stack, and a safety partition running the no_std verdict core. They communicate only through a frozen repr-C contract in hypervisor shared memory. The safety partition releases Ed25519-signed commands to the actuator bus. A separate fleet lane connects vehicles to the verifier control plane over Zenoh, treated as an untrusted carrier. QNX HYPERVISOR 8.0 FOR SAFETY — certification target (ADR-0032) Guest VM — untrusted doer Ubuntu · ROS 2 · Autoware stack Occy planner · Taj perception Mick LLM intent (Ollama, local) crashes, hallucinations and exploits stay inside this box Safety partition no_std verdict core · zero alloc seqlock snapshot → validate envelope · RSS · posture Ed25519 release token the certified artifact candidate #[repr(C)] frozen contract · SHM Actuator bus verify-before-release Fleet control plane kirra_verifier_service · Linux attestation · posture · OTA · audit Zenoh fleet lane — untrusted carrier, Ed25519 verify-before-use on every ingest trust never comes from the transport

HARDWARE-GATEDQNX-target execution is the recorded remainder: cross-builds are reproducible in CI today; certified timing awaits target hardware.

docs/adr/0032-governor-deployment-platform.mddocs/safety/HYPERVISOR_CONTRACT_CHANNEL.mdcrates/kirra-contract-channel/src/lib.rs.github/workflows/ci.yml:122

Code structure

36 crates, layered by trust

ADR-0035 decomposed a monolith into layers where dependency direction encodes criticality: the checker logic depends on nothing heavy, and nothing heavy can reach into the checker. A CI fence proves the LLM-facing crates have no compile path to actuation.

Layered crate decomposition (ADR-0035) Dependency layers from zero-dependency leaf crates up to adapters: kirra-policy-types and kirra-core at the bottom; kirra-trajectory, kirra-planner, kirra-map in the middle; the ros2 adapter, inline governor and verifier service above; with detached hardening harnesses — loom, kani, fuzz, postgres conformance — alongside. kirra-policy-types · kirra-core zero/lean-dependency leaves — the types everything shares kirra-trajectory · kirra-planner · kirra-map · kirra-taj the checker & doer logic — no ROS, no HTTP, no DB kirra-ros2-adapter · kirra-inline-governor · sidecars integration shells — features gate every heavy dependency kirra-verifier (root) — control plane, HTTP, SQLite Detached hardening harnesses verification/kani — 12 proofs over shipped source kirra-loom-models — 4 concurrency models fuzz/ — 4 targets · kirra-verifier-pg — live PG compile to nothing in a normal build; own CI lanes parko/ — separate workspace ML inference substrate: ONNX · OpenVINO · TensorRT diverse second governor + divergence comparator isolation enforced by CI — runtime deps can't leak in

docs/adr/0035-verifier-crate-decomposition.mdci/check_mick_actuation_fence.pyparko/ci/check-runtime-isolation.shCargo.toml

Memory ownership

Exactly one crate in the enforced path may use unsafe: the SHM carrier, with its unsafe budget enumerated (shm_open/mmap, atomic field access). The contract channel and in-line governor are #![forbid(unsafe_code)].

crates/kirra-hv-carrier/README.mdcrates/kirra-inline-governor/src/lib.rscrates/kirra-contract-channel/src/seqlock.rs

Threading model

The verifier's supervised loops are declared as data — a task manifest with dependencies, criticality, and deadlines — and started in a topologically-sorted order that fails closed on cycles or missing tasks.

src/execution_manager.rs

Storage seams

Persistence is a set of storage traits (epoch fence, node store, federation, posture state, OTA) with SQLite, in-memory, and live-Postgres backends all running the same conformance suites in CI.

crates/kirra-persistencecrates/kirra-verifier-pg.github/workflows/ci.yml:503

Transport lanes

Three lanes, three trust models

There is no single “message bus.” Each lane gets exactly the trust model its criticality demands — and none of them trusts the carrier.

LaneCarrierTrust modelStatus
Enforcement (in-vehicle) POSIX SHM seqlock · frozen #[repr(C)] contract Coherent-snapshot read → validate → Ed25519 over the enforced bytes → verify-before-release LIVE
ROS 2 / DDS (doer side) DDS via r2r (Humble/Iron/Jazzy) · CycloneDDS writer feature-gated Fail-closed QoS: actuator topics must be Volatile — negotiated QoS is read back and a downgraded topic is refused at open LIVE
Fleet (vehicle ↔ ops) Zenoh (ADR-0007) Untrusted carrier: Ed25519 payload signatures verified before use; rejection counters; QM-only, fenced off the safety path SPIKE
Zero-copy candidate iceoryx2 (pinned =0.9.2, isolated workspace) Same frozen contract over a zero-copy channel; 9-class fault matrix passes in full and minimal feature configs SPIKE

src/dds_bridge.rssrc/dds_cyclonedds.rscrates/kirra-fleet-transport/README.mdtools/iceoryx2-spike/README.mddocs/adr/0006-governor-transport-iceoryx2.md

Why this differs from ROS-centric architectures: in a conventional stack, safety rides the same middleware as everything else, and a QoS misconfiguration can silently replay a stale actuator command to a late-joining subscriber. Kirra's actuator QoS is enforced fail-closed in code (TransientLocal is refused, lifespan = deadline), and the enforcement path doesn't ride middleware at all — it's a seqlock over shared memory with a signature over the exact bytes.

Positioning

Where Kirra sits in the landscape

Kirra is not an end-to-end driving stack, and we won't pretend it is. It is the governed layer under one. That makes most comparisons complementary, not competitive — and where the repository gives us no evidence, we make no claim.

Autoware

The decision of record keeps Autoware as the AV-stack doer — Kirra does not reimplement localization or closed-loop control, and the gap analysis says so plainly. What Kirra adds is what the analysis found Autoware has no equivalent of: formal, fail-closed command bounding (RSS conjunction, occlusion caps, decel-to-stop) applied to the doer's output at a frozen contract boundary.

docs/adr/0036-autoware-distro-migration-occy-gap.md

Mobileye RSS

RSS is a published formal model, and Kirra implements it in the open: longitudinal/lateral safe distances as a conjunction, Rule-4 occlusion bounds, opposite-direction terms — with property tests, an exhaustive concrete mirror, and two of the primitives machine-checked by Kani. You can read every line.

parko/crates/parko-core/src/rss.rsverification/kani/src/proofs_rss.rsdocs/safety/KIRRA_RSS_FORMAL_SPECIFICATION.md

NVIDIA DRIVE

Complementary by design: Kirra's certified-timing target is DRIVE-class hardware running QNX for Safety, with Jetson Orin as the doer/dev rig. The repository is explicit that Jetson never hosts the certification target — and neither do we.

docs/hardware/TARGET_PLATFORM_MATRIX.mdtools/qnx-rtm-harness/README.md

Waymo · Wayve · Apollo

Vertically-integrated or end-to-end learned stacks solve a different problem: driving. Kirra solves governing — a doer-invariant safety case that holds whether the doer is geometric, learned, or an LLM. We publish no benchmark against closed systems we cannot measure.

docs/adr/0020-doer-invariant-safety-case.md

READ THE SOURCE

The architecture is the argument.

Every box on this page is a crate you can read, a decision record you can audit, or a CI lane you can re-run.

View the repository Browse the documentation