Компания General Dynamics C4 Systems и австралийский исследовательский центр NICTA открыли под свободными лицензиями исходные тексты микроядра seL4 (Secure Embedded L4), компоненты математического доказательства его надёжности и сопутствующий код для построения высоконадёжных операционных систем. Ядро открыто под лицензией GPLv2, а утилиты и работающий в пространстве пользователя код содержит как элементы под лицензией GPLv2, так и компоненты под лицензией BSD.