seL4 (Microkernel)

seL4 is a microkernel in the L4 microkernel family that became, in 2009, the first general-purpose operating system kernel with a machine-checked proof of functional correctness against its formal specification. The proof, written in Isabelle/HOL, establishes that the C implementation refines an abstract specification and is therefore free of whole classes of implementation bugs -- buffer overflows, null-pointer dereferences, arithmetic overflows, undefined behaviour, deadlocks, and use of uninitialised memory. The project began in 2004 at NICTA (the Australian national ICT research centre, later folded into CSIRO's Data61) in Sydney, with Gerwin Klein leading the verification effort and Kevin Elphinstone the kernel design, under the supervision of Gernot Heiser. A central engineering goal was that formal verification should not cost performance: seL4 was designed so its measured IPC fast path is comparable to or faster than other L4 kernels, dispelling the assumption that high-assurance kernels must be slow. On July 29, 2014 NICTA and General Dynamics C4 Systems released seL4's source and proofs under the GNU General Public License version 2. The seL4 Foundation was established in April 2020 under the Linux Foundation umbrella to coordinate industrial use. Production deployments include autonomous vehicle stacks, telecommunications equipment, defence avionics (notably DARPA's HACMS programme demonstrators), and IoT security devices. seL4 is widely cited as the strongest counter-example to the 1990s consensus that microkernels were a dead end: it delivers both verified isolation and competitive performance, just in markets where those properties matter more than ecosystem size.