seL4 is an open-source microkernel whose implementation is mathematically proven correct against its specification, with machine-checked proofs that guarantee, in its verified configurations, that the kernel does exactly what it says and isolates the components running on top of it. No version of Linux offers that kind of guarantee, which raises a recurring question: could seL4 be a more robust and secure alternative? The short answer is yes in its own territory, critical systems, and no as a general-purpose operating system.
seL4 vs Linux key facts in 20 seconds
- seL4 is a microkernel with formal correctness and security proofs.
- It is 10,000 to 16,000 lines of code depending on architecture.
- It is not a full OS and does not replace Linux on desktops or servers.
- It can run Linux inside isolated virtual machines.
The project was born at the Australian lab NICTA, now part of CSIRO’s Data61, which in 2009 published the first formal proof of functional correctness for a general-purpose kernel. The code was open-sourced in 2014 and since 2020 it has been driven by the seL4 Foundation, hosted by the Linux Foundation. The latest release is seL4 17.0.0, published at the end of October 2026 and focused on fixing issues in unverified configurations and auditing code that falls outside the scope of the proofs. The code lives on GitHub, where the kernel repository has more than 4,500 stars, alongside the proofs repository (l4v), written in Isabelle.
What seL4 is, and what it is not
A microkernel does the bare minimum in the processor’s privileged mode: virtual memory, threads, inter-process communication (IPC) and permissions. Everything else, from device drivers to file systems and the network stack, runs as isolated user-level processes. Linux does the opposite: it is a monolithic kernel in which drivers, file systems and networking share an address space with the rest of the kernel, so a bug in one driver can compromise the whole system.
According to the project FAQ, the verified 64-bit RISC-V kernel is about 10,000 lines of code; the AArch64 version with hypervisor support, about 12,600; and x86-64, about 16,000. Linux runs to tens of millions. Access control is capability-based: a process can only use resources for which it holds an explicit, unforgeable permission. The project also claims seL4 is the fastest microkernel for cross-address-space IPC on the processors it supports.
What seL4 is not: a ready-to-use operating system. It has no files, POSIX-style processes or sockets. To build something useful you need frameworks such as CAmkES, the seL4 Microkit (designed for static-architecture systems), LionsOS, an operating system for embedded and IoT environments developed at UNSW, or third-party options such as Genode or Kry10’s KOS.
What exactly the proofs guarantee
The central proof is functional correctness: the C code faithfully implements the abstract specification, ruling out whole classes of bugs such as buffer overflows or memory leaks. Security proofs build on it: integrity (nobody modifies data without authorisation), confidentiality (nobody reads it) and availability. On ARMv7 there is also a binary correctness proof, extending the guarantee to the machine code produced by the compiler. According to the verified configurations documentation, the current status is:
| Architecture | Functional correctness (C) | Integrity and availability | Confidentiality | Binary | Verified hypervisor |
|---|---|---|---|---|---|
| ARMv7 (32-bit) | Yes | Yes | Yes | Yes | Functional correctness only |
| AArch64 | Yes | Yes | Yes | No | Yes (EL2) |
| RISC-V 64 | Yes | Yes | Yes | No | No |
| x86-64 | Yes | No | No | No | No |
The AArch64 confidentiality proof, completed by Proofcraft in 2026 with support from the UK’s NCSC, closed the security proof stack for 64-bit Arm. The MCS configuration, for mixed-criticality real-time systems, now has a functional correctness proof on RISC-V and is being ported to AArch64.
The proofs have explicit limits. They assume that assembly code, boot code, hardware and DMA behave as expected; device address translation (SMMU or IOMMU) is not verified in any configuration, and the multicore (SMP) kernel, built around a big lock, is not verified. Verification of a multikernel model is under way, with the roadmap targeting the third quarter of 2028. It is also worth remembering that the guarantee covers the kernel: a badly written driver or application can still fail, although the failure stays contained in its compartment.
Comparison: seL4, Linux and other kernels
| Aspect | seL4 | Linux |
|---|---|---|
| Type | Microkernel | Modular monolithic |
| Kernel size | 10,000-16,000 lines | Tens of millions of lines |
| Correctness assurance | Formal proof in verified configurations | Review, testing and fuzzing |
| Drivers | In user space, isolated | Inside the kernel |
| Access control | Fine-grained capabilities | Unix permissions, LSM (SELinux, AppArmor) |
| Hardware support | Specific boards and platforms | Practically everything |
| Multicore | SMP unverified; multikernel under verification | Mature, scalable SMP |
| Applications | Needs its own framework or Linux in a VM | Full ecosystem |
| Kernel licence | GPLv2 | GPLv2 |
The project itself compares seL4 with other high-assurance kernels. In its view, QNX and INTEGRITY are widely deployed in critical environments but are closed source, older designs and lack a functional correctness proof; CertiKOS is the only kernel with comparable proofs, but it is not general-purpose or deployed; and FreeRTOS, aimed at microcontrollers, lacks full proofs and fine-grained access control. On Linux, the seL4 Foundation argues that monolithic kernels are too large to provide high assurance and that SELinux does not change that, and it also counts Xen and KVM among solutions with a large attack surface. These are the project’s own assessments.
An alternative to Linux? Where it really fits
For a web server, a database or a desktop, seL4 is not a practical alternative: there is no distribution, hardware support is limited and a verified multicore model is not yet available. Where it does make a difference is in systems where failure is unacceptable and the feature set is bounded: aviation, defence, automotive, medical devices, critical infrastructure or security gateways.
The most common pattern combines both worlds. seL4 acts as the hypervisor and runs Linux in a virtual machine for everything that needs its ecosystem, while critical components run directly on seL4, isolated with formal guarantees. If Linux crashes or is compromised, the rest of the system stays protected. The FAQ says Linux can run as a guest on Arm v7 and v8 and on x86 with Intel VT-x.
There are real deployments. According to the project website, DARPA’s HACMS programme used it with Boeing on the Unmanned Little Bird helicopter and other autonomous vehicles; Chinese carmaker NIO integrates it in SkyOS-M on the ONVO L60; MEP uses it in a voice system for air traffic and maritime communications; and companies such as Kry10 and DornerWorks build products on it. Neutrality is developing Atoll, a datacentre hypervisor based on seL4.
For a sysadmin the takeaway is practical: seL4 will not replace Linux across your server fleet, but it is a serious option when highly sensitive components need provably strong isolation, such as a key manager, an industrial gateway or a device controller. Anyone wanting to try it can start with the official tutorials and the Microkit on QEMU or a supported board such as the Raspberry Pi 4.
Frequently asked questions
Is seL4 an operating system?
No. It is a microkernel that provides minimal mechanisms; full systems are built with frameworks such as CAmkES, Microkit or LionsOS, or by running Linux in a virtual machine.
Does formal verification mean seL4 has no bugs?
In verified configurations the code meets its specification, provided the proof’s assumptions about hardware, boot, assembly and DMA hold. Unverified configurations, such as SMP, can still contain bugs.
Can I run Linux applications on seL4?
Yes, by running Linux as a guest in a virtual machine on seL4, which acts as a hypervisor on Arm v7, Arm v8 and x86 with VT-x.
What licence does seL4 use?
The kernel is licensed under GPLv2; most user-level tools and libraries use BSD-2-Clause.
Sources: