The Secure Enclave on iOS devices runs sepOS, and earlier fork of the UNSW/NICTA L4 nano kernel work. Obviously Apple has huge resources to verify their own kernel on their own hardware, but seL4 is likely much more secure. With Apple's appetite for architectural security improvements I think they will eventually move to an seL4 derivative with special hardware security add-ons.
There are a number of talks at the upcoming seL4 summit, but see 2025, e.g. Kry10 KOS.
Comments
The Secure Enclave on iOS devices runs sepOS, and earlier fork of the UNSW/NICTA L4 nano kernel work. Obviously Apple has huge resources to verify their own kernel on their own hardware, but seL4 is likely much more secure. With Apple's appetite for architectural security improvements I think they will eventually move to an seL4 derivative with special hardware security add-ons.
There are a number of talks at the upcoming seL4 summit, but see 2025, e.g. Kry10 KOS.
https://sel4.systems/Summit/2025/program.html