jidō
Jidō OS is a safety-oriented AArch64 microkernel that separates the critical domain — control, actuators, real-time — from the cognitive domain — AI, perception, Linux and accelerators — on the same SoC, with mediated boundaries, explicit validation and analyzable temporal predictability on the critical paths.
Autonomous systems need to run heavy AI and deterministic control at the same time. The challenge is letting Linux, GPU and perception frameworks coexist with a control path that must be predictable, isolated and ready to evolve toward a safety case.
Control, actuators, sensor fusion, braking and safe-stop. Requires bounded latency, spatial/temporal isolation and analyzable behavior. A failure here can lead to an unsafe condition.
Perception, SLAM, neural networks, memory and exploratory decision-making. Needs Linux, CUDA/ONNX and large runtimes — unsuitable for a high-ASIL critical path without rigorous isolation.
▼ the boundary between these domains is the central problem of modern autonomous systems ▼
Jidō OS runs in EL2 as a hypervisor and hosts the cognitive domain as an isolated guest. The critical path runs in minimal modules, with capabilities, IPC, priority ceiling and drivers in EL0. The cognitive domain never accesses the critical one directly: every exchange crosses a mediated, validated and traceable boundary.
J I D Ō O S — microkernel AArch64 bare metal · RPi 4 / A72 (silicon) + QEMU virt mmu: stage-1 online, caches enabled [ a72 ] sched: preemptive, priorities, inheritance [ a72 ] cap: capabilities per endpoint/mem/device [ a72 ] ipc: priority ceiling + transitive inheritance [ a72 ] loop: critical EL0 + safe-stop actuator 3.0 µs @600 MHz [ a72 ] fs: JidoFS persistent on SD/EMMC [ a72 ] smp: 4 cores online (BCM2711 spin-table) [ a72 ] japp: Ed25519 signature verified [qemu] smmu: SMMUv3 — DMA confined by stream table [qemu] accel: queues by criticality + watchdog [qemu] can: control bus, priority ceiling [qemu] hyp: stage-2 active — isolated guest in EL1 [qemu] hyp: vGICv3 emulated — GIC mediated by EL2 [qemu] jido> boot-real [ 0.000000] Booting Linux 6.1 — interactive shell under EL2 jido> perc-guest 100 perception: obstacle nearby → ESTOP actuator: motor_stop,0 [ a72 ] silicon · [qemu] emulation/CI
Every component runs with the least privilege possible. Drivers and applications live in EL0, capabilities control authority, and the microkernel keeps only what truly requires privilege.
The result is a foundation for autonomous systems where a perception, driver, or cognitive module failure doesn't have to compromise the control path responsible for keeping the vehicle in a safe state.
This isn't a thesis on slides. The deterministic core runs on Raspberry Pi 4 (silicon): 110 automated tests, CI green, the critical loop with safe-stop, WCET measured on the A72 and persistent storage (JidoFS on SD/EMMC) validated on real hardware (v1.3.0). The cognitive domain — EL2 hypervisor and Linux guest — is validated in QEMU.
Explicit authority for endpoints, shared memory and device MMIO. Least privilege by construction.
Drivers and apps run in EL0. Failures stay contained in the component, without bringing down the whole system.
Priority inversion is bounded and analyzable, improving predictability at critical-path endpoints.
Modules are authenticated with an Ed25519 signature before loading. Tampered code is rejected.
Control proposes; safety validates freshness, obstacles, speed and decides OK/WARN/ESTOP.
A mainline Linux boots to an interactive shell as an isolated cognitive domain, over a GIC emulated by the microkernel — proven on QEMU.
DMA confined by stream table (SMMUv3): the accelerator only reaches authorized memory. Submissions in critical/best-effort queues with a watchdog — the accelerator does not block the control loop. Validated in QEMU: the RPi 4 has no SMMU; silicon validation depends on the pilot's target.
Each device capability declares its ASIL level; the loader rejects grants incompatible with the module's priority.
Parser and syscall-boundary fuzzing, reproducible WCET, static analysis of the kernel and 100% MC/DC on the pure functions and on the scheduler, IPC, capability and MMU paths — in CI on every commit. The safety case starts here.
The Raspberry Pi 4 is no longer "roadmap": Jidō OS runs end to end on silicon — boot EL2→EL1, MMU, GICv2, interactive shell, the isolated critical loop in EL0 (control → SafetyMonitor → actuator/servo) with safe-stop, WCET measured on the A72 (multi-core, with controlled priority inversion) and persistent storage (JidoFS on SD/EMMC). QEMU remains the regression baseline; hardware is now the anchor.
Jidō OS is a functional prototype validated on silicon — it is not a certified product. The deterministic core and persistent storage run on the Raspberry Pi 4; the EL2 hypervisor and the Linux guest are validated in QEMU. The safety case has Phase 1 closed and Phase 2 in progress: static analysis of the kernel, parser and syscall-boundary fuzzing, 100% MC/DC on the pure functions and on the scheduler, IPC, capability and MMU paths, and reproducible WCET run in CI on every push — with traceability, an FMEA of the TCB, tool classification and the first sealed baseline. The fault-injection campaign and MC/DC for IPC and MMU are now closed and run in CI; still missing is a pre-assessment by an independent certification body — until then the safety case is self-declared. The WCET figures hold for the BCM2711 and revert to “pending” on any other silicon. We do not claim completed certification.
Technical preprint: "Bounding Priority Inversion at IPC Endpoints in an AArch64 Microkernel for Autonomous-Vehicle Control Loops: A Silicon Evaluation on Cortex-A72" · submitted to SBESC 2026 · DOI 10.5281/zenodo.20767672.
Jidō OS already runs end to end on Raspberry Pi 4 (silicon) — including the critical loop with safe-stop. A ready-to-flash .img.gz SD card image is generated with every release (v1.3.0), so partners can test without compiling or setting up a toolchain.
A FAT32 .img.gz image with kernel, firmware and config.txt already configured. Flash it with the Raspberry Pi Imager or dd and Jidō OS boots directly.
Port with a written design roadmap and zero code so far: the Jetson Nano (Tegra X1, 4× Cortex-A57) as the bare-metal critical domain and the Orin Nano as the cognitive domain, physically separated. It gets queued if it is the pilot customer's target.
Validation of the flow on Raspberry Pi 4 is complete: bare-metal boot, PL011 console, SD-flashing roadmap and WCET measurement on real hardware. The .img.gz image is already available for download in the jido_osi repository.
seL4 is the state of the art in formally verified microkernels. It took ~200 person-years of mathematical proof at NICTA/CSIRO. No startup gets there alone in its first year. What sets Jidō OS apart is having gotten the architecture right from the start — which is exactly what seL4 also did before everything else.
| Property | seL4 | Jidō OS today | Jidō OS — roadmap |
|---|---|---|---|
| Spatial isolation (capabilities + per-AS MMU) | formally proven | implemented · tested · not proven | incremental formal analysis |
| Formal correctness verification | complete proof (Isabelle/HOL) | none | priority critical properties |
| Analyzable kernel WCET | proven in some configs | QEMU -icount + RPi 4 A72 (single-core and 4 cores) + inspection-based analysis | formal WCET (MISRA/MC-DC) · Jetson (v2.x) |
| Temporal isolation · priority inversion | fixed priority, no inheritance · MCS outside the verified configs | transitive inheritance + ICPP · protected 2.28 µs on the A72 (p99 2351 ns) vs. ~1.003 ms baseline | re-run the campaign on the pilot's silicon |
| EL2 hypervisor + isolated Linux guest | via additional layers (CAmkES) | native · real Linux to interactive shell | incremental maturity |
| Ready critical↔cognitive pipeline | you build it from scratch | SafetyMonitor · IPC · integrated caps | real hardware + real sensors |
| SMMU / accelerator DMA isolation | supported on specific targets | SMMUv3 + critical/best-effort QoS — in QEMU; the RPi 4 has no SMMU | validate on the pilot's silicon |
| Certification (Common Criteria / ISO 26262) | no CC or ISO 26262 certificate · proof argued as beyond EAL7 | SEooC under construction · Phase 1 of the safety case closed | incremental · ASIL-B → ASIL-D as goal |
| Integration time for autonomous systems | months to years | pipeline and drivers ready · ARM64 port exercised 1× (RPi 4) | a 2nd silicon target confirms the stated lead time |
Complete formal verification, refinement proof down to the binary on specific configurations, and decades of production use in defense and avionics. That can't be replicated without massive investment and time. Whoever says otherwise is lying.
The right architecture from day one — capabilities, isolation by construction, critical↔cognitive separation and an incremental safety case. seL4 also started this way before proving everything. We're at that stage, with clarity about what's missing.
Technical preprint: "Bounding Priority Inversion at IPC Endpoints in an AArch64 Microkernel for Autonomous-Vehicle Control Loops: A Silicon Evaluation on Cortex-A72" · DOI 10.5281/zenodo.20767672 · submitted to SBESC 2026. The paper documents the architecture and WCET measurements of the functional prototype — without claiming completed certification.
Jidō OS can serve as an R&D platform, reference architecture, or integration base for mobile robotics, AGVs, experimental vehicles, drones and embedded physical AI systems.
Technical diagnosis to map the critical↔cognitive boundary, architecture risks and an isolation roadmap.
Functional demonstration on QEMU, Raspberry Pi or a simple target hardware, with isolated modules and SafetyMonitor.
Port to real hardware, drivers, control bus, sensor/actuator integration and technical documentation.
Software-defined vehicles, autonomous robotics and ECU consolidation are pushing the industry to run control, AI and Linux on the same silicon without letting one domain compromise the other.
| Capability | Mature automotive RTOS | Linux / DriveOS | seL4 | Jidō OS |
|---|---|---|---|---|
| Commercial maturity/certification | strong | depends on the stack | strong as a formal base | roadmap |
| Critical↔cognitive isolation with Linux guest | possible / product-specific | strong on the cognitive side | possible | main focus |
| Physical AI / light autonomy orientation | generic | strong AI ecosystem | research/defense base | designed for this |
| Open to R&D, porting and co-development | usually closed | broad ecosystem | open | partnership model |
Positioning: a safety-oriented platform for autonomous systems that combines microkernel, capabilities, hypervisor and a critical↔cognitive boundary in one R&D and embedded-integration product.
For technology partners, investors, labs and companies that need to separate critical control, AI, Linux and accelerators with a clear isolation architecture evolving toward a safety case.