National ICT Australia (NICTA) hat den Microkernel »seL4« unter eine Open-Source-Lizenz gestellt. Der Kernel zeichnet sich vor allem durch seine Sicherheit aus und wurde unter anderem formal auf Korrektheit geprüft.
Bereits seit 2004 wird von dem National ICT Australia (NICTA) und General Dynamics C4 Systems eine eigene Variante unter dem Namen seL4 (secure embedded L4) entwickelt. Das System wurde speziell an sicherheitskritische Anwendungen im eingebetteten Bereich angepasst. Dazu wurde das System formal auf seine Korrektheit verifiziert. Unter anderem wurde von den Prüfern mathematisch bewiesen, dass die Implementierung die Spezifikation des Kernels erfüllt und der Kernel keinen der verbreiteten Entwurfsfehler (Speicherüberläufe, Zeigerfehler und Speicherlecks) enthält.