Компанията General Dynamics C4 Systems и австралийският изследователски център NICTA откриха със свободен лиценз сорс-кодовете на микроядрото seL4 (Secure Embedded L4). Това ядро е предназначено за създаване на изключително надеждни операционни системи. Сорсът на seL4 е достъпен с GPLv2 лиценз, а помощните програми за работа с него съдържат компоненти както с лиценз GPLv2, така и с BSD.
Според много онлайн-източници, коректността на микроядрото seL4 е доказана по математичен път, което предполага, че софтуерните решения, базирани на seL4 могат да бъдат считани за най-надеждните в света. Микроядрото seL4 изцяло покрива заложените в него спецификации и не допуска грешки от типа на препълване на буфера, блокиране на адресни блокове, неинициализирани променливи и други. Ядрото е предназначено за създаване на критично важни компютърни системи, използвани в авиацията, медицината, финансовия сектор, енергетиката и други области, за които се гарантира, че няма да има непредвидени прекъсвания и грешки.На програмистите се предлага комплектът за разработка на софтуер CAmkES, позволяващ моделиране и създаване на системи, базирани на seL4. Включени са примери и прототипи. Поддържат се архитектурите ARMv6 (ARM11), ARMv7 (Cortex A8, A9, A15) и x86.Върху микроядрото seL4 може да бъде стартирано Linux-ядро, като в този случай seL4 изпълнява ролята на хипервайзор.