seL4

Il gruppo australiano di NICTA ha pubblicato la dimostrazione nel 2009: circa 8.700 righe di C, verificate nell'assistente di dimostrazione Isabelle/HOL rispetto a una specifica formale. Sono serviti circa 20 anni-persona, cioè una fatica pari a una ventina di volte quella di scrivere il codice. Dimostrazioni successive hanno provato che il binario compilato corrisponde al sorgente e che il kernel garantisce l'isolamento tra i componenti.

Il kernel in sé fa quasi nulla (thread, spazi di indirizzamento, IPC e capability) e tutto il resto gira come processi isolati a livello utente. È adatto ai sistemi in cui un bug costa più della verifica: nel programma HACMS della DARPA ha volato su un elicottero senza pilota che un red team non è riuscito a prendere in controllo. Il codice è stato rilasciato come open source nel 2014.