seL4's formally verified isolation enforcement enables unique solutions for safely running critical applications alongside uncritical workloads. This capability has a significant impact across critical sectors such as automotive, aerospace, infrastructure, defence, secure communications, and more.
Here are some examples of where seL4 is being used. There are many more — while seL4 is open source, many products or developments on it are not or cannot be public.
If you would like to be added to this list, please contact us at foundation@sel4.systems. See also our list of research organisations conducting seL4-related research and the list of frameworks and languages built on or for seL4.
Global smart electric vehicle company NIO mass-produces the ONVO L60 vehicle, featuring their seL4-based SkyOS-M operating system. This was announced by Ning Qu, NIO's VP of engineering and leader of the SkyOS team, at the seL4 summit 2024. NIO is a Premium Member of the seL4 Foundation, with NIO's Global VP of Digital Systems, Qiyan Wang, sitting on the seL4 Foundation board.
Built on seL4 to enable robust security, DornerWorks' Secure Microkernel Virtual Machine (VM) Composer is a modelling tool and the "easy button" that helps organisations develop and deploy virtualised high-assurance systems using a drag-and-drop interface. DornerWorks, a founding member of the seL4 Foundation and one of its endorsed service providers, has a dedicated team of seL4 experts who help organisations accelerate the integration of seL4 as the trusted software base for their products.
SureVoice Solid is running at the heart of the SureVoice Voice Control System (VCS), used by air traffic and maritime controllers to communicate with pilots and captains of ships. MEP is a company developing and supplying voice communication systems for critical applications in the Maritime and Aviation sectors worldwide. MEP has chosen to run SureVoice on seL4 to guarantee 24/7 availability. The seL4 platform provides the separation of functionalities in the SureVoice Solid to ensure safety and secure operation.
KOS is an Operating System and platform designed from the ground up for mission critical connected devices. Developed by Kry10, KOS leverages the formal verification of seL4 to provide an operating system that is secure, self-healing, and dynamic with minimal downtime, even during upgrades. Kry10 is an seL4 Foundation member, with strong seL4 expertise, contributing three members to the seL4 Technical Steering Committee, Kent McLeod, Ihor Kuz and Matthew Brecknell.
Swiss start-up Neutrality is developing the Atoll hypervisor — a high-assurance platform designed to protect systems that are likely targets of well-resourced attackers. Atoll will leverage the seL4 microkernel, configured as a multikernel, to provide verified isolation between virtualised workloads running on datacenter-class hardware with hundreds of CPU cores. This approach will deliver orders-of-magnitude increases in hardware performance while retaining the benefits of formal verification.
In 2021, DARPA brought the SMACCMcopter, a research vehicle protected by seL4 as part of the HACMS program, to the famous DEF CON hacker convention. DARPA challenged the assembled hacker elite to "steal this Drone", confident in seL4's formally verified security enforcement. As expected, the hackers' efforts to compromise the SMACCMcopter were comprehensively defeated. As DARPA said: "Formal methods FTW!"
In the DARPA-funded HACMS program, seL4 was embedded in a range of autonomous vehicles, ranging from trucks, a land robot, and a quadcopter to Boeing's Unmanned Little Bird helicopter. At the end-of-project demonstration, the HACMS Red Team — a professional team of hackers — was unsuccessful at compromising the security of the helicopter, in flight: they were given full access to the uncritical camera feed, and were even given the keys to crash its virtual machine, but seL4 prevented the cyber attack from compromising the flight mission.
