seL4

Het team van het Australische NICTA publiceerde het bewijs in 2009: ruim 8700 regels C, geverifieerd in de bewijsassistent Isabelle/HOL tegen een formele specificatie. Het kostte ongeveer 20 manjaar, zo'n twintig keer de moeite van het schrijven van de code zelf. Latere bewijzen toonden aan dat het gecompileerde binaire bestand met de broncode overeenkomt en dat de kernel isolatie tussen componenten afdwingt.

De kernel zelf doet bijna niets (threads, adresruimten, IPC en capabilities) en al het andere draait als geïsoleerde processen in gebruikersruimte. Dat past bij systemen waar een bug meer kost dan de verificatie: in het HACMS-programma van DARPA vloog hij mee in een onbemande helikopter die een red team niet wist over te nemen. De code werd in 2014 open source.