SeL4

seL4 is a formally verified microkernel in the L4 family, designed to provide strong isolation and security guarantees for high-assurance systems. Developed principally at the Australian research organization NICTA (now part of Data61) and its collaborators, seL4 descends from the L4 microkernel lineage and emphasizes a minimal, capability-based kernel surface and message-passing inter-process communication. The project seeks to enable certifiable systems by proving properties about the implementation against a formal specification.

A defining feature of seL4 is its formal verification. The kernel's C and assembly code has been proven correct with machine-checked theorems in the Isabelle/HOL proof assistant, establishing functional correctness and refining an abstract model into executable code. Subsequent work extended proofs to important security properties and cross-architectural correctness, supporting assurance claims for deployed systems.

The kernel provides core services such as capability-based memory management, fine-grained access control, scheduling, and IPC. Its design aims for a small, auditable codebase, making formal verification tractable and enabling secure builds for safety-critical domains. seL4 runs on several architectures, notably ARM and x86, with ports extending to 64-bit variants and ongoing work for other platforms.

Since its inception, seL4 has been used in research and industrial contexts that demand high assurance, including aerospace, automotive, and defense applications. It is distributed under a permissive open-source license, reflecting its emphasis on transparency and collaboration in the verification of kernel correctness.