seL4 Summit 2026: Full Schedule

1 - 3 September | Vancouver, Canada BC
View More Details & Registration
The schedule is subject to change, so please check back before the event for the most up-to-date information.

Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.

arrow_back View All Dates

09:00 PDT

Welcome

Tuesday September 1, 2026 09:00 - 09:10 PDT

Georgia Ballroom B

Tuesday September 1, 2026 09:00 - 09:10 PDT
Georgia Ballroom B

General Session

10:30 PDT

seL4: What, Why, Who and Where? - June Andronick, Proofcraft and seL4 Foundation

Tuesday September 1, 2026 10:30 - 11:30 PDT

Georgia Ballroom B

This talk will provide an overview of the seL4 microkernel and its ecosystem, as an introduction to anyone new to the community and to the seL4 summit, and as a refresher and update to existing players. The aim is that everyone is set to follow the rest of the event and contribute to discussions.

The talk will cover what seL4 is, why its formal verification and security properties make it a key platform for high-assurance systems, who is using and contributing to it across industry, academia, and government, and where it is being applied today. It will provide pointers to who to connect with and where to learn more.

Speakers

June Andronick

CEO, Proofcraft and seL4 Foundation

June Andronick is CEO and co-founder of Proofcraft, a company providing commercial support for software verification in general and the seL4 microkernel verification in particular. She is also CEO of the seL4 Foundation, and Adjunct Professor at UNSW Sydney. June has extensive leadership... Read More →

Tuesday September 1, 2026 10:30 - 11:30 PDT
Georgia Ballroom B

General Session

11:30 PDT

10 Years of seL4 at NCSC - Adam, NCSC

Tuesday September 1, 2026 11:30 - 12:00 PDT

Georgia Ballroom B

The UK’s National Cyber Security Centre first started looking at seL4 and its formal security guarantees in 2016. Over the last ten years, we have worked on numerous projects with the goal of using seL4 to help us in our mission to make the UK the safest place to live and work online. We will talk about our early efforts understanding seL4’s security guarantees and how they map onto our assurance processes for security systems. From those early investigations, we will talk about how we view emerging technologies and how these considerations led us to invest in the seL4 ecosystem. Focussing on real world deployments of seL4, we’ll lift the curtain on several projects we’ve been working on over the last few years building products and systems based on seL4.

The aim for this talk will be to provide insight and feedback on the process of seL4 adoption, including views from industry on the design and deployment of real world products based on the technology. Finally we will talk about where we think seL4 based components fit in the landscape of secure system design and speculation on what the future might hold for seL4 and the NCSC.

Speakers

AdamW1

NCSC

Tuesday September 1, 2026 11:30 - 12:00 PDT
Georgia Ballroom B

General Session

14:30 PDT

Kry10 OS Software Safety Manual - Ihor Kuz, Kry10

Tuesday September 1, 2026 14:30 - 15:00 PDT

Georgia Ballroom B

As a step toward building safety certified systems on the seL4-based Kry10 OS (KOS) we have developed a Software Safety Manual for KOS. This safety manual provides procedures and guidelines for using KOS and its features to develop safety critical systems in such a way that they could be certified.

In general, such systems consist of some core functionality (e.g. run a machine) and some safety-related functionality (e.g. stop the machine if a person is too near). The safety-related functionality is “safety critical”, which means that the systems that implement it should be resistant to failure, even in the presence of known and unknown hazards. Software safety certification is concerned with providing assurance that the risk of these safety-related systems failing has been reduced to an acceptable level.

In a KOS system much of that assurance can be gained from the isolation provided by KOS and the underlying, formally verified, seL4 microkernel. Additional assurance is gained from KOS features such as process supervision, process start and restart, process supervision and monitoring, process resource management, etc. Our safety manual walks through the process of creating a safety-related system and then ensuring that the safety functionality is itself safe. The steps for doing this are: 1) develop the core functionality; 2) develop the safety-related functionality; 3) protect the safety-related functionality from hazards including: memory corruption, process corruption, faulty inputs, faulty outputs, etc.

In this presentation we will discuss and describe this process, illustrating with concrete examples how it can be applied to real working systems.

Speakers

Ihor Kuz

Principal Engineer, Kry10

Dr Ihor Kuz is an operating system engineer at Kry10, helping develop the Kry10 OS and Platform. Ihor has previous experience leading the team developing the seL4 microkernel, and has been involved with seL4 for as long as it’s been around. Ihor is a member of the seL4 Foundation's... Read More →

Tuesday September 1, 2026 14:30 - 15:00 PDT
Georgia Ballroom B

General Session

15:30 PDT

Navigating the Cyber Resilience Act: Real-World Lessons in Securing Connected Products - Jonathan Marshall, SafeShark

Tuesday September 1, 2026 15:30 - 15:45 PDT

Georgia Ballroom B

In an increasingly connected world, cybersecurity is no longer just a technical feature, it is a fundamental legal requirement for market access. The EU’s Cyber Resilience Act (CRA) is set to reshape how digital products are designed, developed, and maintained by introducing strict mandatory cybersecurity standards and incident reporting obligations for manufacturers. But beyond the dense regulatory text, what does this actually mean for your business?

Drawing on real-world testing and compliance experience at SafeShark, this session cuts through the legal jargon to deliver a clear, actionable overview of the CRA. We will explore the core requirements of the Act, how it impacts the entire lifecycle of hardware and software products, and the critical timelines you must meet ahead of the 2027 enforcement deadline. Whether you are a business leader, product manager, or developer, you will leave with a pragmatic understanding of how to navigate these new rules, avoid costly penalties, and ensure your connected devices are secure, compliant, and ready for the European market.

Speakers

Jonathan Marshall

SafeShark

Tuesday September 1, 2026 15:30 - 15:45 PDT
Georgia Ballroom B

General Session

15:45 PDT

Formal Verification now in European Cyber Resiliency standard for OS - June Andronick, Proofcraft and seL4 Foundation

Tuesday September 1, 2026 15:45 - 16:00 PDT

Georgia Ballroom B

In this talk I will report on my contributions to add “Formal Verification” as a requirement to mitigate security risks in the new European Harmonised standards, in the context of the Cyber Resilience Act (CRA). Namely, I have submitted 3 contributions to the Operating System harmonised standard, and all three contributions have now been accepted. The standard is still in the finalisation process, but so far no changes have been requested on my contributions.

The Cyber Resilience Act (CRA) is a regulatory framework of the European Union (EU) for hardware and software products that are made available on the EU market. The CRAentered into force in December 2024 and will be fully applicable as of December 2027, with some provisions starting to apply earlier. During that time, the EU has commissioned European standardisation bodies (namely CEN, CENELEC, and ETSI) to define so-called “harmonised standards” for the CRA. Using a harmonised standard gives a “presumption of conformity”, meaning any product that follows the standard will be assumed by the authorities to comply with the CRA’s legal requirements.

For the CRA, the EU has requested the development of 41 harmonised standards, split into horizontal standards (which apply across all products) and vertical standards (product-specific). One of the vertical standards being developed is specific to Operating Systems (standard number EN-304-626). Each standard defines a list of requirements, and proposes a list of mitigations to address these requirements.

Before my contributions, Formal Verification did not appear at all in the OS standard (and most other standards). This had 2 major implications. Firstly, it meant that the standard was not pushing for what is today the demonstrated highest assurance for critical software, with practical and effective impact. For seL4, this meant that being formally verified would not differentiate it from other OSes with lower assurance, when it comes to being compliant with EU regulations. Secondly, it meant that the effort spent on formal verification would actually be penalised. Indeed, a formally verified product, to be compliant, would still require additional effort to produce lower assurance evidence, such as being checked for memory errors using a source code analysis tool, or being implemented in a memory safe language.

My contributions consist of 3 new mitigations where Formal Verification shall be used to establish: (1) functional correctness; (2) integrity; and (3) confidentiality. With these additions to the OS standard, the CRA will be more in-line with the state-of-the-art approach to cyber resiliency, and seL4’s unique differentiator can continue to be a key advantage for a more secure software world.

Speakers

June Andronick

CEO, Proofcraft and seL4 Foundation

Tuesday September 1, 2026 15:45 - 16:00 PDT
Georgia Ballroom B

General Session

16:00 PDT

Panel Session & Speakers To Be Announced

Tuesday September 1, 2026 16:00 - 17:00 PDT

Georgia Ballroom B

Tuesday September 1, 2026 16:00 - 17:00 PDT
Georgia Ballroom B

General Session

seL4 Summit 2026

09:00 PDT

10:30 PDT

June Andronick

11:30 PDT

AdamW1

14:30 PDT

Ihor Kuz

15:30 PDT

Jonathan Marshall

15:45 PDT

June Andronick

16:00 PDT

Get help with the event