seL4

オーストラリアの NICTA のチームが2009年に証明を発表した。約8,700行の C コードを、Isabelle/HOL 証明支援系で形式仕様に対して検証したもので、工数は約20人年、コードを書く労力のおよそ20倍に及んだ。その後の証明で、コンパイル後のバイナリがソースと一致すること、そしてカーネルがコンポーネント間の分離を強制することも示された。

カーネル自体はほとんど何もせず、スレッド、アドレス空間、IPC、ケイパビリティだけを提供し、残りはすべて分離されたユーザーレベルのプロセスとして動く。バグのコストが検証のコストを上回るシステムに向いており、DARPA の HACMS プログラムでは無人ヘリコプターに搭載され、レッドチームに乗っ取られることはなかった。コードは2014年にオープンソース化された。