seL4

Zespół australijskiego NICTA opublikował dowód w 2009 roku: około 8700 linii C zweryfikowanych w asystencie dowodzenia Isabelle/HOL względem formalnej specyfikacji. Zajęło to ok. 20 osobolat — mniej więcej dwadzieścia razy więcej niż napisanie samego kodu. Późniejsze dowody wykazały, że skompilowany plik binarny odpowiada kodowi źródłowemu i że jądro wymusza izolację między komponentami.

Samo jądro robi niemal nic — wątki, przestrzenie adresowe, IPC i capabilities — a cała reszta działa jako odizolowane procesy w przestrzeni użytkownika. Pasuje to do systemów, w których błąd kosztuje więcej niż weryfikacja: w programie DARPA HACMS jądro latało w bezzałogowym helikopterze, którego zespół red team nie zdołał przejąć. Kod otwarto w 2014 roku.