Skip to content
← Projects

RamenOS

In Progress

A capability-based Rust microkernel exploring a post-Unix system built around typed contracts, user-space drivers, and explicit authority boundaries.

RamenOS is a from-scratch operating system built on a capability-based microkernel in Rust. The architecture is organized around three pillars: Core (the kernel and capability system), Foundry (build and contract tooling), and Store (persistence and package management).

The project starts from the view that a lot of mainstream operating-system structure is historical inheritance rather than necessity. Instead of ambient authority, loosely typed boundaries, and syscall surfaces that grow by convention, RamenOS tries to make authority and interfaces explicit from the start.

The three pillars

The architecture is split into three parts that are meant to stay conceptually distinct:

  • Core is the kernel, capability system, and the minimal runtime machinery the rest of the system depends on.
  • Foundry is the tooling layer for building components and defining the contracts between them.
  • Store is the persistence and package-management side of the system.

That separation is important because the project is not just “a kernel in Rust.” It is an attempt to shape the whole system around a cleaner authority model.

Contracts instead of convention

RamenOS uses typed IDL contracts for IPC, with user-space drivers communicating through the capability system rather than a traditional syscall-heavy model.

The idea is that if two parts of the system need to talk, the boundary between them should be declared and checked explicitly. Interfaces should be part of the architecture, not an accumulation of ad hoc integer codes and opaque buffers.

Current posture

This is still a long-range systems project rather than something pretending to be near-finished.

What makes it worth listing now is the architectural thesis: capability-based structure, typed contracts, and a post-Unix split between kernel, tooling, and storage concerns. Lean 4 formal verification is planned for the kernel’s core invariants once that lower-level shape is stable enough to deserve it.