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
-
23 Jun 2025
Have a look at the program of the seL4 Summit 2025. We have a great line-up of interesting seL4 work, with a combination of technical research and development, experience reports of seL4 in the field, technical discussions and birds-of-a-feather sessions.
Program at a glance. Go to the full program.
Keynotes
We are pleased to announce that the two keynotes for the seL4 Summit 2025 will be John Hatcliff from Kansas State University and Sebastian Jester from Cyberagentur. John will talk about Model-based Development for seL4 Microkit/Rust with Integrated Formal Methods using HAMR and Sebastian about Formally verified IT – Germany’s next cybersecurity paradigm.
Dr. John Hatcliff is a University Distinguished Professor and
Lucas-Rathbone Professor of Engineering at Kansas State University working in
the areas of safety-critical systems, software architectures, and software
verification and certification. He leads the Laboratory on Specification,
Analysis, and Transformation of Software (SAnToS Lab), whose research has been
funded by national funding agencies and companies including Department of
Defense, National Science Foundation, DARPA, Department of Homeland Security,
US Army, NASA, NIH, ARO, Air Force Office of Scientific Research, SEI,
Collins Aerospace, Galois, and Lockheed Martin.
Sebastian Jester is Head of Secure Hardware and Supply Chains
at the Agentur für Innovation in der Cybersicherheit (Cyberagentur), which he
joined in 2022. He is on leave from Germany’s Federal Ministry of Research,
Technology and Space, latterly responsible for microelectronics R&D policy at
the national and EU level. He holds a doctorate in astronomy from the
University of Heidelberg and a Master of Physics from the University of
Oxford. The Cyberagentur funds
high-risk research and development projects with a high disruptive potential
in the field of cybersecurity. The Cyberagentur’s goal is to advance internal
and external security and technological sovereignty. It was created in 2020 by
the German Federal Government and is funded by the Federal Ministry of Defence
and the Federal Ministry of the Interior and Home Affairs. The Cyberagentur is
an associate member of the seL4 Foundation.
-
The seL4 Foundation thanks Proofcraft for becoming a Silver sponsor of the seL4 Summit 2025.
Founded by the seL4 verification leaders, Proofcraft offers commercial support and projects in formal verification in general, and involving seL4 specifically. By applying mathematical machine-checked software verification, Proofcraft increases critical software systems' reliability, safety and security, for a verified future.
See here if you are interested in sponsoring the seL4 Summit 2025.
-
The seL4 Foundation thanks UNSW Sydney for becoming a Bronze sponsor of the seL4 Summit 2025.
seL4 was created by the Trustworthy Systems (TS) team, which is now part of the UNSW, a founding member of the seL4 Foundation.
The team has a track record of designing and implementing systems software for performance and reliability, and using rigorous formal methods to prove that they meet their security and reliability goals. Their aims are to:
- shift the software industry away from ad-hoc, unreliable engineering practices, and towards more principled and trustworthy methods; and
- make verified software a default choice, especially in safety- and security-critical systems.
The team works with government and commercial partners, as well as the broader software engineering community, to drive this change.
See here if you are interested in sponsoring the seL4 Summit 2025.
