A developer who has spent a decade working on a side project is showing off an operating system that runs unmodified Linux and Windows kernel drivers as unprivileged userspace processes on a formally verified microkernel. The project, called Neptune OS, challenges a fundamental assumption about how modern operating systems are structured.
What Neptune OS Actually Is
Neptune OS is a Windows NT-like operating system built on top of the seL4 microkernel. Its creator, who goes by cl91, has been developing it for roughly ten years. The latest v0.4 release reached a significant milestone: it can run non-trivial, unmodified or minimally modified Windows and Linux kernel drivers as native, unprivileged userspace processes. These are not virtual machines. They are regular programs executing in an isolated environment where a crash does not bring down the entire system.
A demonstration on the project's YouTube channel shows the amdgpu and i915 drivers from the Linux kernel's DRM subsystem successfully performing mode-setting on Haswell-era hardware paired with a Radeon RX560 graphics card for hotplugged monitors. Additional demos covering storage, networking, and power management drivers are available on the same channel.
The Historical Argument Behind the Project
The motivation for Neptune OS traces back to the early history of Windows NT. According to the project's creator, NT was originally intended to be a microkernel operating system, with system services running as user-mode servers communicating through Mach-style port-based inter-process communication. Late 1980s computing hardware could not support this architecture in practice, and Microsoft abandoned the approach. The result is a modern Windows system where nearly everything runs in kernel space, including components like an HTTP server, which the creator notes has contributed to long-standing stability and security problems.
When seL4 was open-sourced in 2014, the creator saw an opportunity to realize what NT could have been. By building a personality on top of seL4 that implements NT system call services as a userspace process, the project creates an architecture where device drivers run in isolated user processes and communicate through the formally verified IPC mechanism of seL4. A crash in any driver becomes a contained failure rather than a system-wide crash.
The Linux Driver Subsystem
Beyond native Windows drivers, the latest release introduces a Linux Driver Subsystem. This allows unmodified or minimally modified Linux kernel drivers to run as native user processes on seL4. The technical approach mirrors existing projects like User-Mode Linux and the Linux-kernel-as-a-library effort. The project adds a new architecture port to the Linux kernel. When compiled for this port, a reduced Linux kernel binary runs as a regular program that requests resources from the underlying host through seL4 inter-process communication.
The creator notes that the communication interface defined for this subsystem is not specific to seL4. The same approach could theoretically be reused for other NT-like operating systems, including Windows itself, or even non-NT-like operating systems with additional effort.
The Environment Subsystem Idea
The project extends beyond just driver isolation. The creator draws attention to an NT architectural feature called Environment Subsystems, which sit atop the native system call services and expose them as more accessible user-facing APIs like Win32 and POSIX. Microsoft largely abandoned this concept, and the creator sees Neptune OS as an opportunity to revive and expand it. By running drivers in userspace where they conceptually belong, the project treats device drivers as another category of environment subsystem rather than as integral parts of the kernel.
Why This Matters
The core claim is straightforward: an operating system where drivers and system services run as isolated, unprivileged userspace processes on a formally verified microkernel would be dramatically more stable and secure than current mainstream alternatives. A buggy graphics driver or networking stack would crash as a userspace process and restart without triggering a system-wide failure. The formal verification of seL4 provides mathematical guarantees about the correctness of the IPC and memory management mechanisms that mediate all of these interactions.
Whether Neptune OS can move beyond a hobby project into something with industrial relevance remains an open question. The creator acknowledges that the project is ten years old and still in active development, and the question of practical applications and commercial viability is part of what the project is seeking feedback on.
What is clear is that the project demonstrates a viable path toward running unmodified kernel drivers in a userspace isolation model, and the technical architecture it has defined could have applications beyond its own operating system.