a microkernel
/ MY-kroh-ker-nel /
If putting the whole OS in one privileged program is risky because any bug can crash everything, the opposite idea is to keep the privileged core as small as possible. A microkernel does exactly that: the part running with full hardware privilege is reduced to a tiny essential minimum — basically just address spaces, thread scheduling, and inter-process communication (IPC) — while the file systems, device drivers, and network stack run as ordinary user-space processes (servers). Think of a minimalist government that handles only courts, roads, and the postal service, and contracts everything else out to independent companies; if one contractor fails, the government and the other contractors keep running.
Concretely, in a microkernel a request that a monolithic kernel handles with direct function calls becomes a conversation by message passing. To read a file, your program sends a message (via the kernel's IPC) to the file-system server, which may send a message to the disk-driver server, and replies come back the same way. Each server lives in its own protected address space, so a crash or compromise in, say, the network server cannot reach into the file-system server's memory; the system can often even restart a failed server while the rest keeps running. Famous microkernels include Mach (which influenced macOS), L4 and its descendants, QNX (used in cars and medical devices), and seL4, which has been formally verified to be free of large classes of bugs.
It matters because it is the other pole of the structural debate. The microkernel's strengths are robustness (a faulty driver cannot crash the kernel), security, and small enough size to be verifiable. The honest cost is performance: replacing in-kernel function calls with message passing across protection boundaries adds overhead, which is why early microkernels felt slow and why modern ones work hard to make IPC fast. A common misconception is that microkernel automatically means better — it is a deliberate trade of IPC cost for isolation and verifiability, the right choice for high-assurance systems but not always for raw throughput.
On a QNX-based car system, the disk driver, the network stack, and the file system each run as separate user-space servers. If the network server hits a bug and dies, the kernel can restart just that server while the engine-control and display tasks keep running — a level of fault containment a monolithic design cannot easily match.
A tiny privileged core; drivers and services run as isolated user-space servers talking via IPC.
seL4's claim to fame is formal verification — a mathematical proof that the kernel meets its specification — which is feasible precisely because the kernel is tiny. That kind of proof is essentially impossible for a multi-million-line monolithic kernel; small size is what buys verifiability, and it is part of why the IPC-cost trade-off can be worth it for safety-critical systems.