　一方、UNSWではL4 Kernelを64ビットに移植し、「L4/MIPS」や「L4/Alpha」などを開発したものの、L4Ka::Pistachioのリリースを受けていったん自分たちのL4 Kernelを放棄。あらためて、L4Ka::Pistachioをベースにx86やARM、MIPSで稼働するL4 Linuxを開発している。

　このUNSWの開発グループは、その後NICTA（オーストラリア国立ICT：National ICT Australia Ltd）という国立研究所に移り、ここでL4Ka::Pistachioから「NICTA::L4-embedded」という新しいL4 Kernelをフォークした。これは名前の通り商用向けの組み込みシステム向けL4 Kernelで、メモリフットプリントを減らすとともにオーバーヘッドを削減したことで、かなりのリアルタイム性を確保した。このNICTA::L4-embeddedは、2005年にQualcommのモデムに採用が発表され、2006年から広く商用での利用が行われることになった。そうしたこともあってか、UNSWの教授を兼任しつつNICTAでERTOS（Embedded RTOS）チームリーダーとしてNICTA::L4-embeddedの開発を率いてきたGernot Heiser（ゲルノート・ハイザー）氏は、Open Kernel Labs（OKLabs）という会社を設立、ここで商用向けのL4-Embeddedを「OKL4」として発売するとともに、そのサポートを請け負うビジネスを開始する。

　このOKL4は、引き続きQualcomm向けに採用された他、車載向けの一部や、変わったところではAppleの「A7」以降のプロセッサ内部のセキュアエレメントに採用されている。ただしこのOKL4は、名前に反してオープンソースの形で提供されたのは2008年10月にリリースされたOKL4 3.0が最後で、その後はクローズドソースに切り替わった。OKLabs自体が2012年9月にGeneral Dynamicsに買収され、2014年にはOKLabsがあったシドニーのオフィスは閉鎖されている。旧OKLabsの社員がその後Cog Systemsという会社を立ち上げて、そこでOKL4の開発を続けるが、2019年にGeneral Dynamicsから訴えられ、最終的に閉鎖を余儀なくされる（同名の企業がやはり2014年に設立されて現在も営業中であるが、こちらはオハイオ州に本社を置く米国の会社であり、シドニーに拠点を置いたCog Systems Pty Ltd.とは別である）。

　そんなわけでOKL4は尻すぼみに終わってしまった形だが、NICTAではOKLabsが設立された2006年に、OKL4とは別にコンピュータセキュリティの国際規格であるコモンクライテリア（CC：ISO/IEC 15408）などが要求するセキュリティ要件を満たす、高セキュリティ、高信頼性システム向けのプラットフォームを新規に開発することを決定する。特徴的なのはCCを満たすためにカーネルの形式的検証を行うことを目的に掲げており、実際に2009年にはカーネルの実装に対しての形式的検証を完了している。この検証は、カーネルの実装が仕様に対して正しく行われていることや、Dead-Lock／Live-Lock、Buffer Overflow／Underflow、演算例外、未初期化変数の利用といった実装上の問題がないことを担保している。この高信頼性プラットフォームは、L4同様にマイクロカーネルベースで実装され、seL4と名付けられた。世代としては第3世代マイクロカーネルに分類されるOSである（ちなみに資料によれば、もともとの開発はこれもOKLabsで行われたそうだ）。Haskellを使って開発、というのもちょっと独特である。

　さてこのseL4もまた広範に利用された。NICTAはDAPRA（米国防高等研究計画局）の「HACMS」というプロジェクトにseL4を提供。最終的には自律型無人ヘリコプターの制御などにも使われたそうだ。そして2014年9月に、NICTAとGeneral DynamicsはこのseL4をオープンソースの形で公開した。カーネルと検証コードはGPL v2で、ほとんどのライブラリとツールはBSD2条項ライセンスの形で提供されている。そして2020年4月に、このseL4の開発やメンテナンスを行うseL4 Foundationが、Linux Foundationのプロジェクトの一つとして発足しており、現在はこのseL4 FoundationがseL4の管理を行っている（図1）。