Open Source · Active Development

Architecture v2.0 spec complete · M1 boot demo landed · Full compiler M0 in progress

Oxide9

The verified microkernel platform

One nucleus. Three deployment personalities. Structural safety Linux cannot retrofit.

Explore Architecture What Works Today Compare vs Linux / seL4

≤5K

LOC Nucleus

Personalities

<30ms

Unikernel Boot

Demo Landed

ℹ️ Disambiguation: Oxide9 is a Novis9 project and is not affiliated with Oxide Computer Company (the hardware/Rust server company). The "9" suffix is part of the Novis9 product-mark convention.

01 — Overview

What is Oxide9?

Oxide9 is a hybrid capability-based microkernel implemented in Oxide — a systems programming language designed for predictable ownership. One nucleus, three deployment products.

Figure 1 — Oxide9 Platform Architecture

Oxide9 combines a ≤5,000-line capability microkernel with a purpose-built systems language. Deploy the same core as hard-real-time embedded firmware, a sub-30 ms unikernel, or a multi-process server with POSIX compatibility — without rewriting your kernel for each target.

02 — Core Features

Why Oxide9?

Structural safety Linux cannot retrofit. Simpler than seL4. Hot-extensible at the kernel level.

🔐

Capability-Based Security

Native Cap<T> tokens on every nucleus call. No POSIX file descriptors in the nucleus. No ambient authority — ever.

🚀

Verified Hot-Loading

Load .oxext modules into the running kernel at runtime without rebooting. Five-stage pipeline enforces safety before execution.

📦

Three Personalities

Embedded, Unikernel, Server — resolved at link time from one nucleus codebase. No source-tree forks, no #ifdef personality branches.

🛡️

Split-Plane Drivers

Interrupt hot paths in verified kernel extensions. Driver logic in restartable user-space. A crash can never take the nucleus down.

⚙️

Multi-Class Scheduling

Fixed-priority preemptive RT, weighted fair queueing, and adaptive partitioning — all in the nucleus scheduler, switchable per personality.

📊

First-Class Observability

Structured events wired into IPC, capability ops, faults, and scheduling decisions. Tracing is a nucleus primitive, not a bolt-on.

03 — The Oxide Language

A Language Built for Kernels

Oxide is a deliberate systems language for kernel and extension development — no GC, no libc, no runtime. Currently in development (M0 compiler bootstrap in progress).

⚠️ The oxidec compiler today handles an M0 demo subset: it compiles hello.ox → C → runs on host; --verify-extension rejects unsafe raw blocks; --target freestanding-module produces empty stubs. Full language coverage is Milestone M0 (planned, ~7,500 LOC compiler).

Language design choices

Ownership	Exclusive — no hidden aliasing
Sharing	`lend` / `freeze` — lexical scope, not global borrow graphs
Unsafe code	`raw` blocks with mandatory `// SAFETY:` comment
Errors	`Result<T,E>`, `Option<T>`, `try` / `match`
Omitted (MVP)	No traits, inheritance, or async/await
Compile path	Oxide → C → GCC/Clang → native
File ext.	.ox

Working M0 demo (runs today)

// hello.ox — what oxidec can compile TODAY fn main() { let line: [u8; 39] = *b"hello from nucleus (embedded, rp2040)\n"; raw { // SAFETY: stack array, 38 bytes match BUILD_PHASES.md §2 oxide_console_write(&line[0], 38); } } // Output: "hello from nucleus (embedded, rp2040)" // Boots on QEMU x86_64 + Raspberry Pi RP2040

04 — Communication

IPC & Message Passing

Synchronous call as the primary primitive, with priority inheritance. Asynchronous notifications for secondary interactions.

Figure 2 — Synchronous IPC Sequence (call/reply)

📨

send / recv

Async message passing for fire-and-forget patterns

📞

call / reply

Synchronous RPC with priority inheritance — caller blocks until server replies

🔔

notifications

Lightweight async signals for event-driven architectures

05 — Deployment

Three Personalities

Personality differences are link-time, not source-tree forks — one codebase, three products.

🎯

Embedded

ARM Cortex-M · RISC-V RV32

Primary target: Raspberry Pi RP2040

MemoryStatic partitions · MPU · no heap in nucleus

SchedulerRT-only · 32 priority levels

MMUNot required

Use cases

Medical devices · Automotive ECUs · Industrial · IoT

☁️

Unikernel

x86_64 · ARM64

Hypervisor / Firecracker / bare-metal

MemoryVirtual memory · app linked into nucleus

SchedulerRT + Weighted Fair

Cold bootsub-30 ms

Use cases

Serverless · FaaS function platforms · Cloud

🖥️

Server

x86_64 · ARM64

Bare metal or VM

MemoryVirtual memory · multi-process

SchedulerRT + Fair + Adaptive partitioning

POSIXTranslation shim (partial Linux compat)

Use cases

General compute · Legacy Linux apps via POSIX shim

Figure 3 — Personality Trade-off Radar

06 — Extensions

Verified Hot-Loadable Modules

Any Oxide module that passes the compiler and governance verifier can be loaded into the running kernel as a .oxext file — without rebooting. A stronger generalisation of eBPF with full systems programming capability.

Figure 4 — Five-Stage Verification Pipeline

Stage 1

Language Safety

Stage 2

Resource Bounds

Stage 3

Termination

Stage 4

Cap Policy

Stage 5

Attach-Point Match

All five stages must pass atomically — rejection at any stage aborts the load entirely.

What you can do with extensions

🔵 Packet filter in 50 lines

Write a 50-line Oxide packet filter, load it, route traffic through it at kernel speed — no reboot, no kernel patch.

📍 IPC tracing probes

Attach structured tracing probes to any IPC channel without modifying the nucleus.

📋 Custom scheduling classes

Plug in new scheduling policies as verified extensions — experiment without recompiling the kernel.

🔒 Security policy hooks

Add crypto offload or LSM-style security policy hooks at capability call boundaries.

Why not eBPF?

Linux eBPF uses a restricted DSL because C cannot be statically verified. Oxide can be verified at compile time — so Oxide9 extensions use the full language, not a DSL subset.

	Oxide9 ext.	eBPF
Language	Full Oxide	Restricted DSL
Verification	Compile-time + 5-stage	JIT verifier
Scope	Any kernel feature	Network / tracing only

07 — Driver Framework

Split-Plane Architecture

Goal: a new driver in under one day. Describe registers in a DSL, implement cold-plane logic in safe Oxide, attach a verified hot-plane snippet.

🔥

Hot Execution Plane

Verified Kernel Extension

Interrupt entry vectors
DMA direct memory access
MMIO with capability gating
Zero-copy buffer management

Latency: microseconds

❄️

Cold Orchestration Plane

User-Space Task (restartable)

Driver state machine
Error recovery
Dynamic hot-plug handling
Power management

Isolated: reboots on crash — nucleus stays up

08 — Comparison

How Oxide9 Compares

IPC Latency — lower is better (μs)

Boot Time — lower is better (ms, log scale)

Figure 5 — Feature Coverage · Oxide9 vs Linux vs seL4

Platform	Memory Safety	Hot Extensions	Multi-Personality	Cert-Ready	Nucleus Size
Oxide9	✓ Oxide + Cap<T>	✓ Full language (.oxext)	✓ 3 modes (link-time)	✓ TCB-focused (M9)	≤ 5,000 LOC
Linux	✗ C, many CVEs	○ eBPF (DSL only)	✗ Monolithic	✗ Not designed for	~30M LOC
seL4	✓ Formally verified	✗ None	✗ Single mode	✓ Formal proof	~8,700 LOC
Rust kernels	✓ Borrow checker	○ Limited	✗ Varies	○ Partial	Varies
Zephyr RTOS	✗ C/C++	✗ None	✗ Embedded only	○ Some profiles	~300K LOC

Accepted weaknesses — we're honest about this

Smaller driver catalog than Linux for the first several years of development
Workload-specific performance trails tuned Linux paths initially
POSIX shim runs a useful subset of Linux binaries — not the entire Linux universe
Certification (IEC 62304 Class B) is planned at Milestone M9, not yet achieved

"Oxide9 is safer than Linux, simpler than seL4, faster on hot paths than traditional microkernels, and easier to develop on than all of them — accepting a smaller driver catalog and weaker workload-specific performance than Linux for the first five years."

09 — Current Status

What Works Today

Honest, up-to-date status. Oxide9 is in active development — below is exactly what exists right now.

Complete / Landed

v2.0 Hybrid Architecture Specs

13+ specification documents complete

Language Specification v1.0

Full Oxide language spec complete

Kernel Architecture Spec v2.0

Nucleus, IPC, caps, scheduler fully specified

Governance & AI Protocol

Coding standards, AI session protocol v2.0

Decision Log D001–D025

All architecture decisions documented

Brand Identity

Oxide9 under Novis9 — BRAND.md complete

Mechanical Verifier Scripts

tools/verify_integration.py working

Partially Working (demo / bootstrap)

oxidec — Bootstrap Compiler

M0 subset: hello.ox → C → host; --verify-extension rejects bad raw blocks; --target freestanding-module produces stubs

Kernel Boot (M1 bridge)

Boots on QEMU x86_64 and RP2040 via C + assembly bootstrap. Not full Oxide-compiled nucleus yet.

Build Artifacts

make server → build/server/oxide9.elf · make embedded → build/embedded/oxide9.uf2

Boot Demo Messages

QEMU: "hello from nucleus (server, x86_64)" · RP2040: "hello from nucleus (embedded, rp2040)"

Planned (Roadmap)

Full Oxide Compiler (M0)

~7,500 LOC compiler · full language spec coverage

IPC + Capabilities (M2–M3)

Two-task isolation, kill one task other keeps running

Verified Extension Loader (M5)

Hot-load packet filter without reboot

POSIX Shim + WASM (M7–M8)

busybox and redis under capability restrictions

Certification Pack (M9)

IEC 62304 Class B submission · ~23 months total

How it's built today

Under the Hood

Figure 6 — Build Pipeline (current state)

Oxide (.ox)

Tiny snippets

→

oxidec

Bootstrap compiler

→

Generated

C code

C kernel

boot/ logic

Assembly

boot.S / irq0.S

→

Cross-compiler

GCC / Clang

→

Output

.elf / .uf2

Component	Language	Location
Boot / kernel logic	C	boot/m1_qemu_multiboot/
Boot vectors / IRQ	Assembly	boot.S, vectors.S, irq0.S
Bootstrap compiler	C	compiler/oxidec/
Build orchestration	Python + Make	build/build.py, Makefile
Nucleus scaffold	Oxide (.ox)	nucleus/ (layout stubs)
Governance checks	Python	tools/check_*.py

Server (QEMU) cross-compiler

i686-elf-gcc or clang + ld.lld

Embedded (RP2040) cross-compiler

arm-none-eabi-gcc → UF2 via elf_to_uf2_rp2040.py

10 — Roadmap

Milestones M0 – M9

Single developer + AI assistance. Full timeline ~23 months. Minimum viable product (skip unikernel + adoption kit) ~18 months.

Milestone 0

Complete Compiler + Verifier

Full language spec coverage in oxidec (~7,500 LOC compiler). --verify-extension passes all spec tests.

Demo artifact: Full language spec coverage · oxidec compiles all .ox examples

Milestone 1 — Demo Landed ✓

Nucleus Boot on QEMU + RP2040

Same nucleus binary boots on QEMU x86_64 and Raspberry Pi RP2040 hardware. C + assembly bootstrap.

Demo artifact: "hello from nucleus" on both targets

Milestone 2

Two-Task Isolation + IPC

Kill one task, the other keeps running. Basic send/recv/call primitives working end-to-end.

Demo artifact: Two tasks exchanging messages · task fault does not crash system

Milestone 3

Capabilities + Split-Plane Drivers

I2C sensor read via cap-mediated split-plane driver. Cap<T> minting and revocation working.

Demo artifact: I2C sensor via capability-gated driver

Milestone 4

Embedded Personality v1.0

4 tasks, MPU isolation, hard-RT scheduling on RP2040. Embedded personality fully functional.

Demo artifact: 4 MPU-isolated tasks on RP2040 · hard-RT scheduling demo

Milestone 5

Verified Extension Loader

Hot-load an .oxext packet filter into a running kernel without reboot. Five-stage pipeline enforced.

Demo artifact: Live hot-load of packet filter · no reboot · traffic routed through it

Milestone 6

Unikernel Personality

HTTP echo server, sub-30 ms cold boot on Firecracker hypervisor. Single-binary linked app.

Demo artifact: HTTP echo · <30 ms boot on Firecracker

Milestone 7

Server + POSIX Shim

busybox and redis running under capability restrictions via POSIX translation shim.

Demo artifact: busybox + redis under cap restrictions

Milestone 8

WASM Sandbox + Adoption Kit

WASI modules running in WASM sandbox. Sample drivers, package registry, developer tooling.

Demo artifact: WASI modules · sample driver package · registry

Milestone 9

Certification Pack

IEC 62304 Class B submission artifacts. Safety case, traceability matrix, formal test evidence.

Demo artifact: IEC 62304 Class B submission · ISO 26262 / IEC 61508 path

11 — Certification

Safety-Critical Target Markets

Certification path planned for Milestone M9. Oxide9's small TCB and formal governance are designed from day one for regulated industries.

IEC 62304

Medical Device Software

Class B submission planned at M9. Small TCB, full traceability, formal test evidence.

ISO 26262

Automotive Functional Safety

ASIL-B path. Static memory, hard-RT scheduler, capability isolation maps to ASIL requirements.

IEC 61508

Industrial Functional Safety

SIL-2 target. Verified extensions, split-plane drivers, deterministic observability align with SIL requirements.

12 — Developers

Get Started

What you can run today. These commands work against the M1 bootstrap build.

Verify project integrity

py -3 tools/verify_integration.py

Runs all governance and integration checks. Should pass clean on a fresh clone.

Build bootstrap compiler

make bootstrap-compiler

Compiles oxidec (the M0 Oxide compiler written in C) from source.

Run M0 compiler demo

make check-m0

Compiles hello.ox → C → binary on host. Outputs: "hello, oxide"

Build server kernel (QEMU)

make server

Cross-compiles to build/server/oxide9.elf. Run in QEMU to see nucleus boot message.

Build embedded kernel (RP2040)

make embedded

Cross-compiles to build/embedded/oxide9.uf2. Flash to RP2040 via drag-and-drop.

Toolchain bundle

oxidec · tools/check_*.py · build/build.py

Compiler · governance verifiers · build orchestration · five test tiers (unit → HIL).

Oxide9 is open source. We welcome kernel engineers, language designers, and systems researchers.

View on GitHub Read Documentation Join Discussion