The governed layer of autonomy

Every machine gets a model.
Every model needs an envelope.

AI capability is outrunning verification — and no amount of training makes a model certifiable. Kirra is the fail-closed runtime layer that closes that gap: planners, learned policies, and LLMs only ever propose, while a deterministic, machine-checked envelope decides what reaches the actuators. The models will keep changing. The envelope is forever.

Where autonomy is heading Read the source ↗

3,305 tests across 330 files 12 machine-checked Kani proofs 27 blocking CI gates bit-identical incident replay open source · Rust

Where it sits

Where Kirra sits in the stack Untrusted proposers — an LLM or agent, a planner, and perception — emit a proposed action. Kirra, the fail-closed checker, sits between them and the actuator bus and emits a clamped, approved, or denied command carrying an Ed25519 release token. The actuator transports — ROS 2 and DDS, CAN and serial, and shared memory — verify the token before anything moves. UNTRUSTED · SWAPPABLE LLM / agent Planner Perception proposed action KIRRA — the checker posture · envelope · RSS fail-closed · deny by default Ed25519 release token verdict target 100 µs (host-indicative) governed command VERIFY-BEFORE-RELEASE ROS 2 / DDS CAN / serial Shared memory

An un-bypassable checker between untrusted intent and the actuator bus. If trust can't be proven, nothing moves. ≈65 µs p50 · ≈116 µs p99.9 measured (host)

crates/kirra-trajectory/src/validation.rssrc/wcet_gate.rs:92crates/kirra-release-token/src/lib.rs

The world of tomorrow

Autonomy will be won by whoever
can prove safety at runtime.

Three forces make the governed layer inevitable — and every technical decision on this site exists to build it.

AI is outrunning verification

Foundation models are entering planners and language is becoming a robot interface. You can't test a distribution into being safe — but you can bound what any of it is permitted to do.

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

Regulation demands runtime assurance

UL 4600, SOTIF, ASTM F3269, and the emerging AI-safety standards all converge on the same architecture: an untrusted complex function behind a verifiable monitor. Kirra maintains open, versioned mappings to each.

docs/safety/ASTM_F3269_RTA_MAPPING.mddocs/safety/UL4600_SAFETY_CASE.md

Platforms need a decision layer

Certified hypervisors and safety-rated silicon solve isolation and compute — not whether a command is safe. Kirra is built as the decision layer for exactly those platforms, as an SEooC designed for integration.

docs/adr/0032-governor-deployment-platform.md

The one durable interface

Models will keep changing. Sensors will keep changing. The interface that endures is the envelope between intent and actuation — proven, portable, and built to sit inside certified platforms rather than compete with them.

The full vision

The stakes today

Machines make mistakes.
Kirra makes them survivable.

The same checker, holding very different machines to their physics — each of these is a real failure mode with a real mechanism behind it.

Autonomous vehicles

After a fault, the only admissible commands converge to a stop — designed against the 2023 San Francisco dragging incident. And standing water is non-drivable by policy, because lidar can't see a flood — only the absence where a road should be.

How AVs are governed

Robots around people

A pedestrian sensor that goes silent stops the robot — because a machine that can't prove the sidewalk is clear shouldn't keep driving on stale confidence. Proven on physical hardware.

How robots are governed

Industrial control

Oldsmar, 2021: a water plant's lye setpoint was raised 111× on valid credentials, caught only by an operator watching the screen. Kirra decodes the write on the wire and denies on magnitude — identity doesn't excuse physics.

How OT is governed

LLM-driven machines

The model hallucinates a 999 m/s command? Language becomes motion through exactly one typed, fail-closed door — and a CI gate proves the conversational code can't reach the actuators at all.

How LLMs are fenced
All solutions, including fleet operations

How we get there

The AI proposes.
Kirra bounds it.

The mechanism that delivers the vision: every autonomy stack has a component that decides what the vehicle does next, and Kirra assumes that component is wrong — hallucinating, compromised, or simply buggy. Doers are swappable; the checker is the invariant — a separate, smaller, provable layer that no doer can bypass.

Kirra doer–checker architecture Three untrusted doers — Mick, an LLM intent layer; Occy, a planner; and Taj, perception — send typed proposals into the Kirra checker, which applies the posture gate, kinematic envelope, RSS and containment. Accepted commands receive an Ed25519 release token verified by the actuator. Denied commands become minimum-risk maneuvers and are recorded in a hash-chained audit ledger. Mick — LLM intent typed MickIntent · fail-closed parse Occy — planner geometric · learned · proposes only Taj — perception corridor · objects · redundancy UNTRUSTED DOERS — swappable, never safety authorities typed claims KIRRA — the checker posture gate · fail-closed kinematic envelope P0–P6 RSS ∧ conjunction · occlusion containment · predictive modes sole safety authority Release Ed25519 token Motor verify first Deny → MRC + audit ledger SHA-256 hash-chained · verdict id

Deny is the default: no registered proof, no posture, no envelope fit — no motion.

README.mdcrates/kirra-planner/src/lib.rscrates/kirra-trajectory/src/validation.rscrates/kirra-release-token/src/lib.rssrc/audit_chain.rs

Never trusted for safety

An LLM can invent a 999 m/s velocity or an action type that doesn't exist. Both die at the typed parse or the envelope — and the attempt is permanently recorded in the hash-chained audit ledger.

README.md:40crates/kirra-planner/src/mick_llm.rs

One safety authority

validate_trajectory_slow composes containment, per-pose kinematics, and RSS into a single verdict: Accept, Clamp, or MRCFallback. First rejection wins.

crates/kirra-trajectory/src/validation.rs:206

Frozen where it matters

The kinematics checker core is pinned by git blob hash ed00f4da… — CI asserts the exact bytes survive every change, and the Kani proofs run against the shipped source verbatim.

verification/kani/.github/workflows/ci.yml:182

Interactive — fleet posture

Three postures. No exceptions.

Fleet trust state collapses to Nominal, Degraded, or LockedOut, derived from a dependency-graph traversal over every node's attested state. Flip the posture and watch what the gateway does to each command class — this table is the real should_route_command decision, not an illustration.

Command routing under fleet posture A command flows through classification, the posture gate, and the degraded decel-to-stop gate before reaching the actuator. Which stages pass depends on the selected fleet posture. Command HTTP · ROS 2 · SHM Classify allowlist · Unknown⇒deny Posture gate stale cache ⇒ deny Decel gate Degraded ⇒ stop & hold Act denied writes → 503 · MRC · audit
Command classExample routeVerdict
ReadTelemetryGET /fleet/posture
ActuatorMotionPOST /actuator/motion/command
WriteStatePOST /federation/reports/submit
SystemMutationPOST /fleet/dependencies
Unknownanything unclassified

Observability GETs are posture-exempt so operators can distinguish “locked out” from “down” — a read cannot actuate. A stale posture cache (>5 s) fails closed exactly like LockedOut. Degraded is not a crawl: it is a controlled decel-to-stop-and-hold; the governor never authors re-acceleration.

src/posture_cache.rssrc/posture_engine_v2.rssrc/gateway/policy_layer.rsdocs/safety/SAFE_STATE_SPECIFICATION.md

The full safety model

Data flow

The life of one command

From an AI's proposal to a verified actuator release — every stage is a separate, testable function, and every stage can say no.

Runtime internals

  1. 01 · Propose

    A doer emits a typed claim

    Occy plans a trajectory; Mick grounds an LLM utterance into a typed MickIntent through one fail-closed parse. Free text never reaches the control path.

    crates/kirra-planner/src/mick.rscrates/kirra-planner/src/mick_llm.rs

  2. 02 · Classify

    Total, pure classification

    classify_http_command is a fail-closed allowlist — anything it doesn't recognize is Unknown, and Unknown is denied in every posture, including Nominal.

    crates/kirra-policy-types/src/lib.rs

  3. 03 · Posture

    The fleet gate

    should_route_command(cache, now_ms, command) — a stale cache (>5,000 ms) is treated as LockedOut. Trust is recomputed from a cycle-safe DAG traversal over attested nodes.

    src/posture_cache.rscrates/kirra-safety-authority/src/dag.rs

  4. 04 · Envelope

    Hard boundary first

    validate_vehicle_command clamps to the absolute kinematic boundary before any rate limit — the envelope cap always wins. NaN or Inf anywhere is an immediate deny, proved for all 2⁶⁴ bit patterns.

    crates/kirra-core/src/kinematics_contract.rsverification/kani/src/proofs_kinematics.rs:84

  5. 05 · RSS

    Formal distance keeping

    Longitudinal and lateral safety evaluated as a conjunction, extended with occlusion-aware speed bounds at blind junctions and multi-modal prediction rolled forward in time.

    parko/crates/parko-core/src/rss.rs:317crates/kirra-trajectory/src/validation.rs:999

  6. 06 · Verdict

    Accept · Clamp · MRC

    A denial mints a verdict id, binds the exact inputs into the audit chain, and returns an operator-readable explanation at GET /verdicts/{id}.

    src/verdicts.rs

  7. 07 · Release

    Sign the enforced bytes

    The governor signs an Ed25519 release token over exactly the bytes it validated. The crypto rides the actuation path — never inside the verdict's timing budget.

    crates/kirra-release-token/src/lib.rsdocs/adr/0031-release-token-on-the-actuation-path.md

  8. 08 · Verify-before-release

    The actuator checks everything

    Token → strict signature over the presented bytes → strictly-advancing release sequence (equal = replay) → decode. A refusal never poisons the watermark.

    crates/kirra-inline-governor/src/lib.rs

  9. 09 · Record

    Tamper-evident memory

    Every decision lands in a SHA-256 hash-chained ledger that survives SIGKILL mid-append as a valid prefix — proven by a power-loss drill in CI — and ships off-box to WORM storage.

    src/audit_chain.rstests/audit_chain_prefix_on_kill.rssrc/audit_shipper.rs

  10. 10 · Replay

    Bit-identical reconstruction

    Any captured session re-runs through the real checker and must reproduce every verdict to the exact bit (f64::to_bits, no epsilon). Incidents are reconstructed, not approximated.

    crates/kirra-replay/src/lib.rsdocs/REPLAY_INCIDENT_RECONSTRUCTION.md

The enforced path

No HTTP between verdict and motor.

On the enforcement path the governor reads commands from shared memory through a seqlock, decides, signs, and releases — in-process, allocation-free, with the memory model checked under Miri and the concurrency protocol model-checked under Loom.

Transport read latency — p50

Host-indicative measurements from the repository's own benches. Not certified WCET.

In-process floor28 ns
Shared-memory seqlock60 ns
iceoryx2 zero-copy309 ns
UDP + serde proxy976 ns

tools/iceoryx2-spike/src/bin/latency_bench.rscrates/kirra-hv-carrier/README.md

The frozen contract

GovernorContractView is a #[repr(C)], pointer-free struct whose byte layout is pinned by compile-time asserts — “the freeze is the safety claim.” A seqlock generation protocol (odd = write in progress) guarantees the checker only ever judges a coherent snapshot; torn headers are eliminated by construction.

The verdict core is no_std, panic-free by policy, and gated for purity in CI — no allocation, no clock, no crypto inside the decision.

crates/kirra-contract-channel/src/lib.rsdocs/safety/HYPERVISOR_CONTRACT_CHANNEL.mdci/check_verdict_core_purity.py

LIVE cross-process over POSIX SHM, in CI

Assembled in-line loop — read → validate → decide → sign → verify → release

p99.9 over 10,000 release-build iterations on CI hardware (Ed25519-dominated). The gate asserts p99.9, not mean.

measured ≈116 µs p99.9 (host) 100 µs deployment target (SG9) 1,000 µs CI regression ceiling

Certified WCET is defined as QNX-target-under-FIFO measurement and has not been produced yet — the repository says so explicitly, and so do we. Host numbers are regression tripwires, not claims.

src/wcet_gate.rs:92crates/kirra-inline-governor/README.mddocs/safety/WCET_MEASUREMENT_METHODOLOGY.md

Assurance, measured

Trust is a number you can check.

Every figure below is computed from the repository and links to where it lives. If we can't cite it, we don't claim it.

0

test functions across 330 files, run on every push

ci.yml · Test

0

Kani proof harnesses — model-checked over all inputs, not sampled

verification/kani

0

blocking CI lanes: Miri, Loom, fuzz, mutation, coverage floors, supply chain

ci.yml

0

scenario KPI corpus + 71 perception frames; 40k-sample Monte-Carlo nightly

kirra-kpi-gate

Adversarial by default

4 fuzz targets run on every push and 90 minutes each, weekly. PR diffs to the checker face mutation testing: if a mutant survives your tests, the gate fails.

fuzz/fuzz_targets/.github/workflows/ci.yml:636

Coverage that can't regress

Gated decision-coverage floors on the checker crates (77–79%, measured ≈80%) plus a Codecov ratchet: any PR dropping workspace coverage by >0.5% fails.

.github/workflows/ci.yml:379codecov.yml

Supply chain, pinned

cargo-deny + cargo-audit gate every dependency; GitHub Actions are pinned to 40-hex commit SHAs; container images are digest-pinned and keyless-signed with cosign.

deny.tomlscripts/pin-actions.sh.github/workflows/docker.yml

All benchmarks & gates, with numbers

The platform

Explore every subsystem

Runtime

The verifier service: posture engine, attestation, HA failover with epoch fencing, OTA campaigns, WAL-mode persistence.

Runtime

Safety

Postures, decel-to-stop Degraded, MRC, recovery hysteresis, watchdogs, and the safe-state specification.

Safety

Planning

Occy the geometric planner, a learned Hydra-MDP-shaped planner, and Mick's typed LLM intent seam.

Planning

Perception

Taj's corridor pipeline, true-redundancy cross-checking, and fail-closed perception derates.

Perception

Prediction

Multi-modal predictive RSS: constant-velocity and turn-rate hypotheses rolled forward against the ego plan.

Prediction

Determinism

Bit-identical replay, injected clocks, seqlock snapshots under Loom and Miri, machine-checked proofs.

Determinism

Security

Per-node attestation, TPM quotes, scoped RBAC, Ed25519 federation, hash-chained audit, signed releases.

Security

Performance

WCET budgets and gates, the timing substrate, and honestly-scoped latency measurements.

Performance

Architecture

The layered crate decomposition, transport decisions, partition boundaries, and deployment topology.

Architecture

Verdict Playground

The frozen checker, compiled to WebAssembly, running in your browser. Throw a 999 m/s hallucination at it and watch the envelope answer.

Try it live

From thesis to metal

The vision, driving a real robot

ROSMASTER R2 · Jetson Orin NX

LIVE

An Ackermann-steer robot on a Jetson Orin NX 16 GB is the physical testbed — first governed motion validated July 2026, with a TG30 lidar feeding the perception path.

docs/adr/0014-rosmaster-r2-orin-nx-kirra-integration.mdrobot/install/README.md

Clean-room MCU firmware

LIVE

A from-scratch STM32F103 firmware foundation: jerk-limited PID, a fail-closed safety state machine, and COBS + CRC32C framing on the frozen SBC↔MCU wire protocol. Built in CI for Cortex-M3.

firmware/rosmaster-r2/README.md.github/workflows/rosmaster-r2-firmware.yml

QNX 8.0 target lane

HARDWARE-GATED

The certification target is a QNX Hypervisor 8.0 safety partition. Today: reproducible cross-builds for x86_64 and aarch64 QNX in CI, and a shim→judge fault harness with committed VM results.

docs/adr/0032-governor-deployment-platform.mdtools/qnx-rtm-harness/results/qnx800-x86_64-vm-kvm.txt

Certification posture

Engineered toward ASIL-D.
Claimed only when assessed.

Kirra is designed in alignment with ISO 26262 ASIL-D and IEC 61508 SIL 3 requirements, with a UL 4600 safety case, HARA, SOTIF analysis, and a CI-gated requirements-traceability matrix maintained in the open. Independent third-party assessment has not yet been performed — and nothing on this site will imply otherwise.

Read the certification posture

README — the claim, verbatimdocs/safety — 65 artifacts

Field Notes

Engineering, written down

All notes

Dispatches from the build — governed bring-ups, proof engineering, and fail-closed design.

Subscribe on Substack ↗

Open source

Don't take our word for it.
Take the repository's.

Clone it, run the 3,305 tests, kill the process mid-write, replay an incident bit-for-bit. The evidence is the product.

kirra-runtime-sdk on GitHub Getting started