seL4 News

We are thrilled to announce our co-chairs, Martin Dehnel-Wild and Lucy Fletcher, for the seL4 summit 2027, which will be held in Sydney, late Spetember - early October (dates TBC).

• 

  Martin Dehnel-Wild

  Chief Scientist, Kry10

  Dr Martin Dehnel-Wild is Chief Scientist of Kry10, where he leads R&D and heads up Kry10’s UK & European office. He has a DPhil (PhD) in Computer Science from the University of Oxford, where he researched interactive and automated theorem proving for security protocols. Prior to Kry10 he set up and led the UK Government’s formal methods (“provable security”) team, bringing rigorous, automated assurance tooling and techniques to the UK’s most critical and highest security systems. Most of his work over the last 10+ years has focused on pulling formal-methods based tools for software, hardware, and cryptography through to use by regular developers, promoting uptake and use across industry, government, and academia.
• 

  Lucy Fletcher

  Software Engineer, Apple

  Lucy Fletcher is a software engineer at Apple based in Sydney, Australia, working on L4 microkernels and the surrounding ecosystems. Before joining Apple, she studied Computer Science at UNSW and worked with the Trustworthy Systems group, where she focused on the design and development of the seL4 device driver framework. Lucy is passionate about giving back to the seL4 community and supporting its continued growth.

The seL4 Foundation is pleased to welcome the Australian National University (ANU) as an Associate Member. ANU's School of Computing has a longstanding connection to seL4, and ANU researchers have contributed to seL4's original verification efforts and DARPA's HACMS program.

This research contribution continues to grow through a broader concentration of formal methods and programming-languages expertise at ANU. Current work involves the development of programming languages for use with the seL4 Microkit.

The membership strengthens active collaborations between ANU's School of Computing and fellow Australian-based member organisations on the development of secure technology based on the seL4 ecosystem.

Videos of the seL4 Summit 2026 are now available on the seL4 YouTube channel! Links, slides, and posters can be found on the summit Program and Abstracts pages. Thanks to all the speakers for making the seL4 Summit 2026 a great success!

The verification of seL4 on the 64-bit Arm architecture has reached another milestone. After completing the proofs of functional correctness and integrity, Proofcraft has now established the proof that seL4 enforces confidentiality on AArch64, providing a formal mathematical proof that the kernel prevents an application running on top of seL4 from learning information without authorisation.

This milestone completes the formal proof that the seL4 implementation code on AArch64 enforces security isolation of the applications running on top (under the assumptions listed here). This isolation prevents attacks on non-critical applications from propagating to critical applications and compromising them.

The seL4 Foundation thanks UNSW Sydney for becoming a Bronze sponsor of the seL4 Summit 2026.

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.

The seL4 Foundation thanks DornerWorks, sponsor of the seL4 Summit 2026 AM & PM Break.

DornerWorks is an embedded technology partner, a founding member of the seL4 Foundation, and one of its endorsed service providers. Our dedicated team of seL4 experts helps organizations accelerate the integration of seL4 as the trusted software foundation for secure, safety-critical embedded systems and products.

On July 29, 2009, the last "sorry" of the seL4 functional correctness proof was eliminated. A "sorry" is an assumed theorem lacking a complete proof. "0 sorries" meant there was nothing left to prove: the project was finished. We now celebrate this day every year to mark the seL4 day, when the world's first formally verified kernel with a machine-checked code-level proof came into existence.

On July 29, 2014, "seL4 day" became a double-celebratory day: the seL4 code and proofs became open source, paving the way to the widespread use it enjoys today.

A big thank-you to all for your continued support!

Learn more about the history of seL4.

We’re pleased to announce the release of

• seL4 16.0.0: The seL4 microkernel
• Microkit 2.3.0: The seL4 Microkit for building static-architecture systems
• CAmkES 3.13.0: Component Architecture for microkernel-based Embedded Systems
• capDL 0.6.0: Tools for generating, parsing and loading capability distribution specifications
• rust-sel4 5.0.0: Rust support for seL4 userspace. See the Rust section on the seL4 docsite for more information.

seL4 16.0.0 and the corresponding Rust support have breaking changes and will require updates if you are using the seL4 API directly. CAmkES and the capDL tool add units for domain schedules as a new feature, but are backwards compatible. The Microkit release comes with new features and has breaking changes for x86_64 systems.

Enjoy!

We are very fortunate to welcome five industry leaders to participate at the seL4 Summit 2026, in a session on Certification, Compliance and Policies: enabler or barrier to innovation?: Darren Cofer, Peter Davies, Jonathan Marshall, June Andronick, and James Sharp. The panel will be moderated by Martin Dehnel-Wild.

The program of the seL4 Summit 2026 is now available!

The 2026 edition of the seL4 summit features a full first day dedicated to high-level overviews and perspectives, followed by Days 2 and 3 focusing on more technical insights and updates. Have a look at the abstracts from our exciting keynotes and voices-from-nearby presenters, and the great line-up of interesting seL4-related research, development, field reports and technical discussions.

The event will offer an ideal opportunity for people new to seL4 and to formally verified systems to increase their understanding of the landscape and ecosystem, and meet with seL4 developers, adopters and enthusiasts. Don't forget to register and see you soon in Vancouver.

Program at a glance. Go to the full program.

Proofcraft achieved a significant milestone in the seL4 verification roadmap that was years in the making: the MCS configuration of seL4, providing support for mixed-criticality systems, is now proved to be correct on RISC-V.

This configuration is the largest new seL4 feature, indispensable for mixed criticality real-time applications such as automotive use cases. It contains wide-ranging changes to the kernel's implementation and API. Its verification therefore required considerable effort and has been a priority in the seL4 roadmap for a long time.

Proofcraft has now completed the verification of functional correctness for seL4 with MCS. Functional correctness is the largest and most central proof in the seL4 verification stack. The proof targets the RISC-V architecture and will now be ported to the Arm 64-bit architecture, as part of DARPA's PROVERS program.

We are pleased to welcome a new member - Gapfruit - to the seL4 Foundation.

Gapfruit is a Swiss technology company building trustworthy foundations for the systems society depends on - from industrial controls to energy infrastructure. To achieve this, Gapfruit combines microkernel operating systems with capability-based security and hardware-rooted trust - an approach grounded in standards from the Trusted Computing Group. Together, these technologies enable resilient, verifiable device operations for the critical systems that underpin modern infrastructure. By joining the seL4 Foundation, we aim to advance high-assurance computing in critical infrastructure and collaborate with the global seL4 community to make trustworthy systems the standard - not the exception.

Learn more about Gapfruit's work in their contributions to previous seL4 summit panels and talks.

The seL4 Foundation thanks Proofcraft, silver sponsor of the seL4 Summit 2026.

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 2026.

The seL4 Foundation thanks Riverside Research for sponsoring the seL4 Summit 2026 reception.

Riverside Research is a national security nonprofit serving the DOD and Intelligence Community. Through the company's Open Innovation Center (OIC), it invests in multidisciplinary research and development and encourages collaboration. Riverside Research's areas of expertise include Object and Activity Detection; Accelerated AI/ML; Zero Trust; Open Architectures; Computational Electromagnetics; Plasma Physics; Precision Timing; Terahertz Imaging; Commercial Intelligence, Surveillance, and Reconnaissance (ISR); Collection Planning; and more. Learn more at www.riversideresearch.org.

See here if you are interested in sponsoring the seL4 Summit 2026.

We’re pleased to announce the release of

• seL4 15.0.0: The seL4 microkernel
• Microkit 2.2.0: The seL4 Microkit for building static-architecture systems
• CAmkES 3.12.0: Component Architecture for microkernel-based Embedded Systems
• capDL 0.5.0: Tools for generating, parsing and loading capability distribution specifications
• rust-sel4 4.0.0: Rust support for seL4 userspace. See the Rust section on the seL4 docsite for more information.

seL4 15.0.0 and the corresponding Rust support come with new features and will require updates if you are using the seL4 API directly. CAmkES and the capDL tool add domain schedules as a new feature and applications will need updates if they use the seL4 domain scheduler. The Microkit release should not require any update of user code compared to Microkit 2.1.0.

Enjoy!

Keynotes

We are pleased to announce that we have two outstanding keynotes for the seL4 Summit 2026: Anjana Rajan, Former Assistant National Cyber Director at The White House, and Martin Dehnel-Wild, Chief Scientist at Kry10. Abstracts coming soon — stay tuned!

"Voices from Nearby"

This year, the summit will feature a full first day dedicated to applications, overviews, and perspectives on seL4-based systems and formally verified software in the real world. This will include a session on "Voices from Nearby," with industry experts who work in or share their thoughts on areas that are adjacent to the core seL4 areas. Alistair Woodmand, Board Member of the Erlang Ecosystem Foundation, will share his insights on the European Cyber Resiliency Act and implications for open source software, and David Hardin, Associate Director of Systems Engineering at Collins Aerospace, will give an overview on trends in real-world formal verification. Details coming soon!

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.

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

Register here

The early bird cut-off date is 31 July 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.

The seL4 Foundation is pleased to welcome Riverside Research as an Associate Member.

Riverside Research acquired Cog Systems, a founding member of the seL4 Foundation in 2025 and continues their work using seL4 within High Assurance systems. Riverside Research is a national security nonprofit serving the DOD and Intelligence Community. Through the company's Open Innovation Center (OIC), it invests in multidisciplinary research and development and encourages collaboration. Riverside Research's areas of expertise include Object and Activity Detection; Accelerated AI/ML; Zero Trust; Open Architectures; Computational Electromagnetics; Plasma Physics; Precision Timing; Terahertz Imaging; Commercial Intelligence, Surveillance, and Reconnaissance (ISR); Collection Planning; and more. Learn more at www.riversideresearch.org.