seL4

seL4 е високопроизводително микроядро от трето поколение от семейството L4, известно като първата операционна система с пълно математическо формално доказателство за коректност (formal verification) от ниво спецификация до бинарен машинен код. Чрез строга изолация на процесите и модел за сигурност, базиран на способности (capability-based security), seL4 гарантира липса на препълване на буфери, непредвидени информационни течове и непозволени повишения на привилегиите, служейки като еталон за критични инфраструктури и пясъчници за автономни системи.