Runtime

A control plane that
refuses to guess.

The verifier service is the fleet's source of truth: who is attested, what posture the fleet is in, which artifact every node should be running. Every one of those answers is derived, persisted, and fenced — never assumed.

Posture engine

One worker, coalesced bursts, monotonic generations

Posture recalculation is serialized through a single worker fed by a typed trigger channel. When five sensors fault at once, the worker drains all buffered triggers and recomputes once — no thundering herd, no torn intermediate states.

Cycle-safe DAG traversal

Fleet posture derives from a gray/black two-set traversal over the dependency graph. A cycle locks the fleet out with CYCLE_DETECTED; a depth blowout locks out with MAX_DEPTH_EXCEEDED. A locked-out dependency propagates LockedOut upward — never merely Degraded.

crates/kirra-safety-authority/src/dag.rssrc/verifier.rs

Generations survive restarts

The posture generation counter persists to SQLite and is restored at boot, so generation numbers never travel backward across restarts — federation peers depend on that monotonicity, and a conditional-upsert keeps it race-safe on both SQLite and Postgres.

src/posture_engine.rscrates/kirra-persistence

Structured lockout reasons

Fail-closed decisions carry typed reasons — DagLockedOut, PostureCacheStale — not strings. The cache snapshot is atomic: posture, generation, timestamp, and TTL move together.

src/posture_engine_v2.rssrc/posture_cache.rs

High availability

Failover without split brain

Heartbeats detect failure; they never grant authority. Authority is a durable epoch claimed by compare-and-swap, and a revived old primary is fenced — its writes refused — the moment a standby has claimed the next epoch. The whole drill runs as a deterministic test in CI, plus a real two-process drill.

HA failover with epoch fencing A primary verifier holds a durable epoch and writes heartbeats. A standby promotes by claiming the next epoch through a compare-and-swap. A revived old primary is fenced: its stale epoch is refused, so there is exactly one writer at a time. Primary — Active holds epoch N · heartbeats 2 s lease renew at half-life (EP-03) Standby — Passive watches heartbeat + lease Durable store try_claim_epoch — CAS single source of authority Revived old primary epoch N < N+1 ⇒ FENCED stale re-claim refused

Lease-based failover (≤5 s, EP-03) is opt-in behind KIRRA_HA_LEASE_ENABLED; the epoch CAS remains the sole takeover authority either way.

tests/ha_failover.rstests/ha_two_process_drill.rssrc/lease.rssrc/standby_monitor.rsverification/kani/src/proofs_lease.rs

The lease timing algebra — renew at half-life, promote only after holder expiry, clock-skew fails safe — is machine-checked by Kani proofs L1–L4 over all 64-bit inputs, not sampled ones.

Persistence

Disk before memory, always

WAL-mode SQLite with a strict ordering invariant: state is saved to disk before it is inserted into memory, so a crash can lose an in-flight request but never invent one. Schema migrations are versioned and refuse to open a database written by a newer binary.

Kill-tested durability

A CI drill SIGKILLs a child process mid-append and asserts the audit chain reopens as a valid, intact prefix — an abrupt power loss can never leave a torn or forked chain.

tests/audit_chain_prefix_on_kill.rstests/audit_row_durability_on_abort.rs

Backend-agnostic contracts

Storage is a family of traits — epoch fence, node store, federation, posture state, OTA campaigns — and the same conformance suites run against SQLite, in-memory, and a live Postgres 16 service container in CI. Corrupt rows decode fail-closed on every backend.

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

Config that fails at boot

Every KIRRA_* variable lives in one canonical registry; unknown vars warn at startup, and a malformed value in a migrated var aborts boot rather than silently defaulting at use. The effective config's SHA-256 digest is committed to the audit chain, so drift is detectable.

src/env_config.rs

Fleet rollout

OTA that halts before it hurts

Governor artifacts roll out through staged campaigns with a hard rule: advance is fail-closed on fleet posture. If the fleet is anything but Nominal, a campaign halts — it never rolls. A background sweep auto-halts active campaigns on a confirmed regression between advances.

Dual-slot A/B installs

Node-side, a device-agnostic installer stages, trials, and health-gates every artifact — automatic rollback on failed probes — with both app-level slots and the Jetson bootloader's native A/B slots via nvbootctrl. Verified end-to-end by a two-node rollout harness in CI.

crates/kirra-ota-installertests/two_node_rollout.rscrates/kirra-ota-installer/src/nvbootctrl.rs

Uptane, end to end

An anchored node verifies the full signed metadata set — root-keyed role signatures, freshness, rollback floors — before it downloads anything. A re-served older set (rollback attack) or a stripped set (downgrade-by-omission) is refused. The verifier is just an untrusted carrier.

crates/kirra-ota-installerdocs/ota/UPTANE_ROLES.md

Attested adoption

Nodes report the digest they're actually running; reports can be Ed25519-signed against the node's registered attestation key, making adoption counts unforgeable. Campaign lifecycle mutations are audit-chained.

crates/kirra-ota-campaignsrc/campaign_monitor.rs

Execution model

Supervised loops, declared as data

The runtime's seven supervised loops — watchdogs, monitors, shippers — are declared in a task manifest with dependencies, criticality, and deadlines. Startup order is a topological sort that fails closed on a cycle, a missing dependency, or a duplicate.

LoopCadenceFail-closed behavior
Telemetry watchdog100 ms sweep2 s of sensor silence ⇒ node faulted, posture recomputed
Campaign monitor1 s sweepConfirmed posture regression ⇒ active campaigns auto-halt
Heartbeat writer2 sPrimary silence ⇒ standby promotes via epoch CAS
Audit shipper5 sShip-then-advance cursor; at-least-once to WORM sink
Cert-expiry monitor1 h censusLapsed mTLS principal ⇒ warn + audit (auth already fail-closes)

src/execution_manager.rssrc/telemetry_watchdog.rssrc/campaign_monitor.rssrc/audit_shipper.rssrc/cert_expiry_monitor.rs

READ THE SOURCE

Run it yourself in five minutes.

docker compose up brings up the verifier, dashboard, and an optional HA standby — then kill the primary and watch the fence hold.

View the repository Browse the documentation