seL4 (secure embedded L4) ist ein Mikrokernel, der ursprünglich der L4-Familie entstammt. Der Kernel bietet unter anderem eine synchrone IPC (Interprozesskommunikation), Interrupt- und Thread-Management sowie eine Speicherverwaltung. Das System wurde speziell an sicherheitskritische Anwendungen im eingebetteten Bereich angepasst. Dazu wurde das System formal auf seine Korrektheit verifiziert. In seL4 werden Objektreferenzen und Zugriffsrechte ausschließlich durch sogenannte Fähigkeiten (capabilities) repräsentiert, und Kernel-Ressourcen unterliegen denselben Zugriffsmechanismen wie Nutzerobjekte. (non)