Award-winning technology backed by ground-breaking research
seL4 is both the world's most highly assured and the world's fastest operating system kernel. Its uniqueness lies in the formal mathematical proof that it behaves exactly as specified, enforcing strong security boundaries for applications running on top of it while maintaining the high performance that deployed systems need.
seL4 is grounded in research breakthroughs across multiple science disciplines. These breakthroughs have been recognised by international acclaimed awards, from the MIT Technology Review Award, to the ACM Hall of Fame Award, the ACM Software Systems Award, the DARPA Game changer award, and more.
Protecting critical systems around the globe
seL4 protects critical systems from software failures and cyber-attacks. It allows non-critical functionality to run securely alongside critical payloads by enforcing strong isolation and controlled communication.
seL4 is used in a wide range of critical sectors, from automotive, aerospace and IoT to data distribution, military and intelligence. It has been successfully retrofitted into complex critical systems and has demonstrably prevented cyber-attacks. Government organisations on several continents have funded further development of seL4 and its ecosystem.
Supported by commercial service providers
seL4 is the leading choice for building highly reliable software. Commercial support is available to help you build or migrate your product to run on seL4 and benefit from its unparalleled security.
A number of Trusted Service Providers have been endorsed by the seL4 Foundation for their expertise and experience in systems and/or formal verification at various levels: kernel, kernel platform ports, user-level Operating Systems components, and applications.
Backed by an Open Source Foundation
seL4 is open source, supported by the seL4 Foundation, an open, transparent and neutral organisation. The seL4 Foundation's goal is to ensure that seL4 continues to be the most highly-assured operating-system technology, readily deployable with a diverse and stable ecosystem of supporting services and products.
seL4 is free to use; its maintenance and development cost are funded by the seL4 Foundation memberships.
Contributions from a strong ecosystem
seL4 and its related technologies receive contributions from developers around the world.
The microkernel code itself evolves through a tightly controlled process, safeguarded by the Foundation's Technical bodies, to preserve its security, high assurance, and mathematical proofs.
Frameworks, tools and components that run on top of seL4 can use seL4's formally verified protection mechanisms and are therefore easier to assess for correctness. This means they can evolve more rapidly and accept community contributions at a higher pace, increasing the ease of adoption of seL4.
Annual gathering at the seL4 Summit
The seL4 Summit is the annual international conference on the seL4 microkernel and all seL4-related technology, tools, infrastructure, products, projects, and people.
It brings together the entire seL4 community to learn about the seL4 technology, its latest advances, uses, successes, challenges and plans. The event showcases exciting seL4 development, research, real world applications and experiences, offering an opportunity to connect with other seL4 developers, users, providers, customers, supporters, potential partners and enthusiasts.
Development Roadmap
With an active, public development roadmap, seL4 continues to solidify its position as the leading secure operating system and the industry standard for verified software. Evolution drives every level of the seL4 ecosystem:
seL4 itself is expanding its support for an increasing range of platforms, architectures, configurations and features.
The ecosystem is expanding with the development of frameworks, tools, components and language support to facilitate the production of seL4-based systems.
The formal proofs, which make seL4 unique, evolve alongside seL4. They are constantly maintained, improved, and kept in lock-step with the seL4 code.
Documentation and learning material
Eager to learn how to use and build on seL4 or its related frameworks and tools like Microkit, CAmkES, and Rust language support?
Explore the wide range of learning material for seL4, from hands-on tutorials and comprehensive documentation to research articles and university courses.
Latest News
-
13 Mar 2026
We are pleased to welcome a new member - Neutrality - to the seL4 Foundation.
Designed for organisations that cannot compromise on trust, Neutrality is building Atoll, a formally-verified, secure, European-sovereign virtualisation and cloud hosting platform. Atoll provides a mathematical proof of isolation between customer workloads, delivering a new level of assurance. Atoll builds on the foundation provided by the formally-verified seL4 microkernel, extending its formal correctness proof and platform support to securely run colocated commercial workloads handling sensitive data on commodity hardware.
Neutrality combines cutting-edge research in Systems, Formal Methods, and Security with a world class engineering team to provide organisations unprecedented levels of trust in their most critical systems.
Joining the seL4 Foundation enables the team at Neutrality to collaborate with the global community advancing the seL4 microkernel and formally verified, high-assurance computing.
-
23 Feb 2026
We have an exciting new format for 2026! A full first day dedicated to applications, overviews, and perspectives on seL4-based systems and formally verified software in the real world. Followed by two days of technical talks and discussion on development, research, and experience reports.
If you're new to seL4 or still developing your familiarity with the technology, this is an ideal opportunity to get a high-level view of the landscape and ecosystem.
The seL4 summit 2026 will be in Vancouver, Canada, on 1 - 3 September 2026.
Come hear about:
- vision, lessons-learned, roadmaps for verified software deployments;
- use-cases, deployments, experiences;
- walk-throughs and demos of tools, frameworks, systems;
- early work, crazy ideas, out-of-the-box thinking;
- technical progress, updates, breakthroughs.
And join us for one of the informal social activities on Monday 31 August 2026, for a fun gathering before the event starts!
If you have any cool work/idea/project/product related to seL4, don't forget to submit a talk proposal.
Tickets include:
- Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions
- Networking with other seL4 experts and enthusiasts
- Dinner
The early bird cut-off date is 31 July 2026.
-
28 Jan 2026
The seL4 Foundation is pleased to welcome the Fraunhofer Institute for Applied and Integrated Security AISEC as our latest Associate Member.
Fraunhofer AISEC is considered one of the world-leading institutions for applied research in cybersecurity. Around 230 highly qualified researchers develop customized security concepts and solutions for commercial businesses and the public sector, boosting the overall competitiveness of clients and partners. Fraunhofer AISEC designs solutions for enhanced data security and effective defense against cybercrimes such as corporate espionage and tampering attacks. The institute's portfolio ranges from embedded and hardware security, automotive and mobile security to security solutions for industry and automation.
Fraunhofer AISEC is exploring the use of the seL4 microkernel and its ecosystem to build strictly separated, resilient embedded and IoT systems.
