SeL4

seL4 (security enhanced L4) is an open-source, high-assurance, capability-based microkernel. It inherits the performance and design characteristics of the L4 microkernel lineage but is implemented using high-assurance methods. seL4 uses formal mathematical verification to prove the system's confidentiality, integrity, availability among other properties. The initial paper outlining seL4's verification was inducted into the 2019 ACM SIGOPS Hall of Fame. The kernel is extremely minimal, handling only memory management, process isolation, and scheduling. Its Inter-Process Communication (IPC) acts as a protected procedure call for cross-domain invocation rather than general-purpose message passing. seL4 was developed as a from-scratch microkernel design influenced by the L4 microkernel family, with an explicit goal of enabling comprehensive formal verification while maintaining high performance. In 2009, the seL4 project reported a machine-checked proof of functional correctness spanning from formal specification to C implementation. In July 2014, the seL4 kernel sources and verification artifacts were released as open source by NICTA with industry partners. On 7 April 2020, the seL4 Foundation was launched to support governance, ecosystem development and long-term stewardship; it was initially hosted as a project of the Linux Foundation. seL4 is extremely minimal, even compared to prior L4 kernels: it only handles memory management/process isolation and process scheduling - everything else is handled outside of kernel mode. At boot time, the seL4 kernel statically allocates enough memory for itself and then hands over all remaining memory and capabilities to an initial user space process. seL4 is more akin to a CPU driver than other microkernels like Mach, QNX, or Minix. The primary motivation was to enable policy and architectural freedom for system builders, but it also helps make verification easier and minimizes cache misses. seL4 uses a capability-based model to control all access to memory and kernel resources.