The seL4 Summit 2026

seL4 Summit 2026 Program

The seL4 Summit 2026 will feature a combination of technical research and development, real-world seL4 deployment insights, in-depth interactive discussions, thought-provoking keynotes, "voices from nearby", panel discussions, as well as informal social activities. Videos will be made available on the seL4 YouTube channel after the event.

New!

The 2026 edition of the seL4 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 be followed by Days 2 and 3 focusing on more technical development, research, reports, and discussions. The event will offer an ideal opportunity for people new to seL4 or who are still developing their familiarity to gain a high-level view of the landscape and ecosystem.

Program-at-a-glance

Dinner Development, Research, Reports  & Discussions Tue Sep 1 Mon Aug 31 Wed Sep 2 Thu Sep 3 Informal Social Activities Day 1 Day 2 Day 3 Development, Research, Reports  & Discussions Applications, Overviews & Perspectives

Main Program

All times are local time in Vancouver, Canada (GMT-7).

See the Schedule on LF Events.

Timing of sessions and room locations are subject to change.

Day 1 1 September 2026
Keynote
9:00 - 9:10
Welcome
Robbie VanVossen, Dornerworks
9:10 - 10:00
Keynote
The Age of Software Understanding
Anjana Rajan, Atalanta
Break
Overviews, insights, safety, compliance
10:30 - 11:30
seL4: What, Why, Who and Where?
June Andronick, Proofcraft and seL4 Foundation
11:30 - 12:00
10 Years of seL4 at NCSC
Adam W1, NCSC
Lunch
13:30 - 14:00
Voices from Nearby
To be announced
Alistair Woodman, Erlang Ecosystem Foundation
Trends in Formal Verification for Real-World Applications and Their Implications for the seL4 Ecosystem
David Hardin, Collins Aerospace
14:30 - 15:00
Kry10 OS Software Safety Manual
Ihor Kuz, Kry10
Break
15:30 - 15:45
Navigating the Cyber Resilience Act: Real-World Lessons in Securing Connected Products
Jonathan Marshall, SafeShark
15:45 - 16:00
Formal Verification now in European Cyber Resiliency standard for OS
June Andronick, Proofcraft and seL4 Foundation
16:00 - 17:00
Panel
Panel (topic to be announced)
17:00 - 17:10
Concluding Remarks
Reception @ Chambar, 18:30
Day 2 2 September 2026
Keynote
9:00 - 9:50
Keynote
From Proof to Product: Why Formal Methods Is Finally Ready
Martin Dehnel-Wild, Kry10
9:50 - 10:00
Announcements
June Andronick, Proofcraft and seL4 Foundation
Break
seL4 in use
10:30 - 11:00
Cyber-Hardened Satellite Software (CHSS) VMM
Robbie VanVossen, Dornerworks
11:00 - 11:15
Throwing seL4 on the Throwbot 3 Robot
Nathan Studer, Dornerworks
11:15 - 11:30
Assured Robotics Embedded Systems and Applications in Ground Vehicles (ARSENAL)
Dave Lide, Jason H. Li, KJ Kwak, Trusted Science and Technology (Trusted ST)
Paul Pazandak, Real-Time Innovations (RTI)
11:30 - 11:45
Evolving Legacy Systems Towards Strong Spatial and Temporal Isolation with seL4
Philipp Scholl, ABB Corporate Research
11:45 - 12:00
tSDX - Reference Architecture for Software Defined X
Nils Brand, Fraunhofer IESE
Lunch with Poster Session
Advances in seL4 security verification and R&D
13:30 - 14:00
seL4's Security Proofs
Ryan Barry, Proofcraft
14:00 - 14:30
Trustworthy Systems R&D Update
Gernot Heiser, UNSW Sydney
14:30 - 15:00
Where are we with Time Protection? Verification and cross-domain communication update
Rob Sison, UNSW Sydney
Break
OS components (implementation and verification)
15:30 - 16:00
Pancake Updates
Miki Tanaka, UNSW Sydney
16:00 - 16:15
Verifying seL4 device drivers with CN
Michal Podhradsky, Galois
16:15 - 16:45
Formalising device protocols for sDDF driver verification
Liam Murphy, UNSW Sydney
16:45 - 17:00
Verification of a UDP Implementation: Challenges and Solutions
Alain Kägi, Lewis & Clark College
17:00 - 17:10
Concluding Remarks
Day 3 3 September 2026
Learning from the TSC and walk-through
9:00 - 9:30
Panel
'Ask Me Anything' with the TSC
9:30 - 10:00
Walk-through
Simplifying Microkit System Composition with Acacia
Lesley Rossouw, UNSW Sydney
Break
seL4 explorations and proposals
10:30 - 11:00
A policy-free boot process for seL4
Daniel Schwyn, Neutrality
11:00 - 11:30
Carrels: Secure, high-performance microservice on seL4
Guangtao Zhu, UNSW Sydney
11:30 - 11:45
Single Kernel Multicore seL4
Scott Brookes, Gordon Stewart, David Swasey, Riverside Research
11:45 - 12:00
Booting Windows on an x86-64 seL4-based VMM
Bill Nguyen, UNSW Sydney
Lunch with Poster Session
Frameworks and analyses
13:30 - 14:00
Rigorous Agentic Systems Engineering for seL4 using HAMR
John Hatcliff, Kansas State University
14:00 - 14:15
Accessible Formal Methods – Building on a Strong sel4 Foundation
Nick Tudor, D-RisQ Ltd
14:15 - 14:30
Efficient User-level Physical Memory Management on seL4
Guangtao Zhu, UNSW Sydney
14:30 - 14:45
Modelling and performance analysis of Ethernet on LionsOS
Lesley Rossouw, UNSW Sydney
Break
Discussions
15:00 - 15:45
BoFs
Break
16:00 - 16:45
BoFs
16:45 - 17:00
BoF wrap-up
17:00 - 17:10
Concluding Remarks
Lucy Fletcher, Apple

Social Activities

A number of informal social activities are being organised for Monday Aug 31, prior to the summit. The idea is that at least one person (whose name is mentioned below) will do this activity at the set time. You're welcome to book yourself directly using the link provided, and do the activity at the same time. Please note that some activities are free, and others are available for purchase either online or onsite.