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

10:30 PDT

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

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

Plaza A & 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. June has extensive leadership experience towards making the... Read More →

Tuesday September 1, 2026 10:30 - 11:30 PDT
Plaza A & B

General Sessions, Overviews / Insights / Safety / Compliance

11:30 PDT

10 Years of seL4 at NCSC - Adam, NCSC

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

Plaza A & 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

Adam W1

Lead Verification Researcher, NCSC

Tuesday September 1, 2026 11:30 - 12:00 PDT
Plaza A & B

General Sessions, Overviews / Insights / Safety / Compliance

14:30 PDT

Kry10 OS Software Safety Manual - Ihor Kuz, Kry10

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

Plaza A & 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
Plaza A & B

General Sessions, Overviews / Insights / Safety / Compliance

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

Plaza A & 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

Business Development Director, SafeShark

Over a 25+ year career spanning broadcast media, cybersecurity, adtech, and media measurement, Jonathan has bridged the gap between technology and commercial execution. From pioneering BAFTA-winning interactive services at BBC R&D to building multi-million-pound hybrid TV platforms... Read More →

Tuesday September 1, 2026 15:30 - 15:45 PDT
Plaza A & B

General Sessions, Overviews / Insights / Safety / Compliance

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

Plaza A & 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
Plaza A & B

General Sessions, Overviews / Insights / Safety / Compliance

16:00 PDT

Certification, Compliance and Policies: Enabler or Barrier to Innovation? Darren Cofer, Collins Aerospace; Peter Davies, Imperial College; Jonathan Marshall, SafeShark; Anjana Rajan, Atalanta; James Sharp, Dstl & Martin Dehnel-Wild, Kry10

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

Plaza A & B

Formal verification is increasingly recognised as the strongest approach for establishing trust in the correctness, security and safety of software systems. Yet, certification frameworks, compliance schemes, and public policy are still resisting to mandate it in a meaningful way.
As with any innovation not yet widely used, authorities are careful to change a well established requirement for a newer one with less known consequences, thus increasing their responsibility in assessing them. Regulators also face legitimate concerns in mandating an approach where the surrounding ecosystem of tools, training, services and qualified practitioners has not yet reached sufficient maturity.
This can lead to a deadlock where investments in maturing the technology will not happen as long as there is no market for it. The market will not develop as long as the technology is not mandated by authorities. And authorities won’t mandate the technology as long as it is not mature enough.
This panel will explore how this cycle can be broken. Drawing on the experiences of experts in certification, compliance and policy, we will discuss where efforts to influence certification frameworks are most worthwhile, which barriers are realistically addressable and what actions can have the greatest impact.

Speakers

Darren Cofer

Principal Fellow, Collins Aerospace

Darren Cofer is a Principal Fellow at Collins Aerospace. He earned his PhD in Electrical and Computer Engineering from The University of Texas at Austin. His area of expertise is developing and applying advanced analysis methods and tools for verification and certification of high-integrity... Read More →

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... Read More →

Anjana Rajan

CEO & Co-Founder, Atalanta

Anjana Rajan is the co-founder and CEO of Atalanta. She previously served as the Assistant NationalCyber Director for Technology Security at the White House, where she led national security policy onformal methods. She is an applied cryptographer whose prior work focused on human... Read More →

Peter Davies

Director - Security Concepts, Thales

Peter Davies is a Security Expert operating at the convergence of Safety and Security. An honorary Fellow with Imperial College’s Institute for Security Science & Technology and chair of the AESIN Security Workstream. He is a leading expert on countering Cyber Attacks, targeted... Read More →

Jonathan Marshall

Business Development Director, SafeShark

James Sharp

Senior Principal Scientist, Dstl

Dr James Sharp is a Senior Principal Scientist at Defence Science and Technology Laboratory (Dstl), the UK Ministry of Defence’s in-government S&T organisation. He has previously provided independent technical evaluation to UK Defence Aerospace, and has over a decade of experience... Read More →

Tuesday September 1, 2026 16:00 - 17:00 PDT
Plaza A & B

General Sessions, Overviews / Insights / Safety / Compliance

10:30 PDT

11:30 PDT

14:30 PDT

15:30 PDT

15:45 PDT

16:00 PDT

Get help with the event