L4マイクロカーネルファミリー
具体的には、従来の「高度な保証」を有するソフトウェアでは1行あたりのコストは1000米ドルであるのに対し、開発中のseL4の1行あたりのコストは400米ドルと見積もられた。
NICTAはアメリカ国防高等研究計画局(DARPA)の高保証サイバー軍事システム計画(High-Assurance Cyber Military Systems(HACMS)の下でプロジェクトパートナーのロックウェル・コリンズ社、ガロア社、ミネソタ大学、ボーイング社と共同でseL4ベースの高保証ドローンを保証ツールとソフトウェアと共に開発した。これはボーイングで開発中の操縦も可能な自律型無人ヘリコプターボーイング AH-6への技術移転も計画されていた。最終的なHACMS技術のデモンストレーションは2017年4月、バージニア州スターリングで行われた。
DARPAはまたジョン・ランチベリー博士の提唱でseL4に関連した中小企業技術革新研究プログラム(SBIR)による出資を行った。seL4によるSBIRを受けた企業にはDornerWorks、Techshot、Wearable Inc、Real Time Innovations、Critical Technologiesなどがある。
OskerはHaskellで書かれたOSで、L4の仕様で作られていた。このプロジェクトはマイクロカーネルの研究ではなく関数型プログラミング言語によるOS開発を目的とした。
CodeZeroは組み込みの仮想化とネイティブOSサービスのためのL4マイクロカーネル。これはGPLライセンス版と開発者によって2010年に分岐したクローズドソース版があった。
F9マイクロカーネルはARM Cortex-M3/M4プロセッサの消費電力、メモリ保護に徹底的に注力したゼロから開発されたBSDライセンスのL4実装。
Fiasco.OCは前身のL4/Fiascoから進化した第3世代マイクロカーネル。Fiasco.OCはcapability basedでマルチコアシステムをサポートし、ハードウェア支援による仮想化に対応する。完全に再設計されたユーザーランド環境はL4 Runtime Environment (L4Re)と呼ばれる。クライアント/サーバ通信フレームワーク、共通サービス機能、仮想ファイルシステム基盤、libstdc++やpthread等の一般的なCライブラリなど、マルチコンポーネントシステムを構築するための環境を提供する。