CleOS

A capability-based OS written in Rust, built on the seL4 microkernel.

CleOS is a Rust operating system built on the seL4 microkernel. seL4 provides formally verified isolation guarantees at the kernel level; CleOS builds on that foundation to construct a practical, safe OS environment with Rust's memory safety enforced throughout userspace.

The core idea: keep the trusted computing base as small as possible (seL4 is ~10k lines of verified C), then push all complexity — drivers, filesystems, services — into isolated Rust processes that communicate via seL4 IPC and capability passing. No shared memory, no implicit trust.

Architecture

- Kernel: seL4 (C, formally verified, ~10k LoC TCB) - Root task: Rust bootstrap process — initializes the system, manages initial capabilities - System servers: Drivers, filesystems, and services as isolated userspace processes - Applications: Unprivileged processes, all communication via typed IPC

Why seL4 + Rust

seL4 eliminates kernel-level vulnerabilities through formal verification. Rust eliminates memory safety bugs in userspace. Together they push the attack surface toward logic errors — the class of bugs that still requires careful design, not just a safe language.

Status

Early bootstrap phase. Project structure and build toolchain are being established.