seL4 Summit 2026

seL4 Summit 2026

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.

08:00 PDT

Registration & Badge Pick-up

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

Georgia Ballroom Foyer

Tuesday September 1, 2026 08:00 - 17:00 PDT
Georgia Ballroom Foyer

Registration / Breaks / Special Events

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

09:10 PDT

Keynote: The Age of Software Understanding - Anjana Rajan, CEO & Co-Founder, Atalanta

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

Georgia Ballroom B

The emergence of formally verified building blocks across the stack, from memory-safe languages to verified microkernels like seL4, represents a hard-won foundation. But it raises a deeper challenge: local correctness does not translate to system reliability. Each component may behave exactly as proven, while the system as a whole remains unpredictable.This talk introduces Software Understanding...
See More →

Speakers

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 →

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

Keynote Sessions

10:00 PDT

Break

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

Tuesday September 1, 2026 10:00 - 10:30 PDT
Georgia A

Registration / Breaks / Special Events

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

Speakers

A

AdamW1

NCSC

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

General Session

12:00 PDT

Lunch

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

Tuesday September 1, 2026 12:00 - 13:30 PDT
Georgia A

Registration / Breaks / Special Events

13:30 PDT

Talk Title To Be Announced - Alistair Woodman, Erlang Ecosystem Foundation (EEF)

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

Georgia Ballroom B

Speakers

Alistair Woodman

Board Member, Erlang Ecosystem Foundation (EEF)

Alistair has been working in the networking space since the 1980s. Product management jobs at Apple and Cisco kept him busy for over 20 years. For the last 10+ years he has been providing business development support for several open-source projects. His relationship to the Erlang... Read More →

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

Voices From Nearby

14:00 PDT

Trends in Formal Verification for Real-World Applications and Their Implications for the seL4 Ecosystem - David Hardin, Collins Aerospace

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

Georgia Ballroom B

The formal methods community has made great progress in the past two decades to mature mathematically-precise techniques in order to tackle real-world design and analysis problems. In areas as diverse as hardware design, finance, systems engineering, software development, and law, increasingly the question is not, “Why would you use formal methods?” but rather “Why wouldn’t you?”...
See More →

Speakers

David Hardin

Chief Technologist, Applied Research and Technology, Collins Aerospace

David S. Hardin has made contributions in the areas of formal methods, computer architecture for High Assurance systems, as well as memory-safe programming languages. He is currently Chief Technologist for the Trusted Cyber team in the Applied Research and Technology organization... Read More →

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

Voices From Nearby

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

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:00 PDT

Break

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

Tuesday September 1, 2026 15:00 - 15:30 PDT
Georgia A

Registration / Breaks / Special Events

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

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

17:00 PDT

Closing Remarks

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

Georgia Ballroom B

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

Keynote Sessions

18:30 PDT

Attendee Reception

Tuesday September 1, 2026 18:30 - 20:30 PDT

TBA

Tuesday September 1, 2026 18:30 - 20:30 PDT
TBA

Registration / Breaks / Special Events

08:00 PDT

Registration & Badge Pick-up

Wednesday September 2, 2026 08:00 - 17:00 PDT

Georgia Ballroom Foyer

Wednesday September 2, 2026 08:00 - 17:00 PDT
Georgia Ballroom Foyer

Registration / Breaks / Special Events

09:00 PDT

Keynote: From Proof to Product: Why Formal Methods Is Finally Ready - Martin Dehnel-Wild, Chief Scientist, Kry10

Wednesday September 2, 2026 09:00 - 09:50 PDT

Georgia Ballroom B

For most of its history, formal methods has been a discipline of proof rather than product: rigorous, powerful, and largely confined to academia. That is changing rapidly. I'll argue that FM is finally ready to deliver secure, resilient systems in the real world, and that the obstacles left are largely self-inflicted: a history of over-promising, tools that are painful to use and barely...
See More →

Speakers

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 →

Wednesday September 2, 2026 09:00 - 09:50 PDT
Georgia Ballroom B

Keynote Sessions

09:50 PDT

Announcements - June Andronick, Proofcraft & seL4 Foundation

Wednesday September 2, 2026 09:50 - 10:00 PDT

Georgia Ballroom B

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 →

Wednesday September 2, 2026 09:50 - 10:00 PDT
Georgia Ballroom B

Keynote Sessions

10:00 PDT

Break

Wednesday September 2, 2026 10:00 - 10:30 PDT

Wednesday September 2, 2026 10:00 - 10:30 PDT
Georgia A

Registration / Breaks / Special Events

10:30 PDT

Cyber-Hardened Satellite Software (CHSS) VMM - Robert VanVossen, Dornerworks

Wednesday September 2, 2026 10:30 - 11:00 PDT

Georgia Ballroom B

MIT Lincoln Laboratory and the Space Cyber-Resiliency group at Air Force Research Laboratory-Space Vehicles Directorate (AFRL/RV) have created a software platform called Cyber-Hardened Satellite Software (CHSS). “CHSS is a mission-agnostic spaceflight software platform whose functionality was inspired by NASA’s core Flight System but with an emphasis on cyber-resiliency. Most notably, CHSS...
See More →

Speakers

Robert VanVossen

seL4 Technical Lead, Dornerworks

Wednesday September 2, 2026 10:30 - 11:00 PDT
Georgia Ballroom B

General Session

11:00 PDT

Throwing seL4 on the Throwbot 3 Robot - Nathan Studer, Dornerworks

Wednesday September 2, 2026 11:00 - 11:15 PDT

Georgia Ballroom B

The Throwbot® 3 Robot by ReconRobotics is a ruggedized, throwable micro-robot designed for rapid and covert reconnaissance in high-risk and dynamic environments. It is used by law enforcement and military personnel for real-time intelligence gathering, situational awareness, and remote investigation under control of a remote operator. Their light weight makes them ideal for many forward...
See More →

Speakers

Nathan Studer

Technical Strategy Lead, Dornerworks

Wednesday September 2, 2026 11:00 - 11:15 PDT
Georgia Ballroom B

General Session

11:15 PDT

Assured Robotics Embedded Systems and Applications in Ground Vehicles (ARSENAL) - Dave Lide, Trusted Science and Technology with Additional Speakers To Be Announced

Wednesday September 2, 2026 11:15 - 11:30 PDT

Georgia Ballroom B

The Robot Operating System (ROS) is widely adopted on various robotic platforms, including military robotic ground vehicles. However, it was not designed for performance and determinism requirements or for the safety and security required for the execution of critical missions. The Robotic Technology Kernel (RTK) is a ROS-based autonomy software library for S&T development that provides a set of...
See More →

Speakers

Dave Lide

Trusted Science and Technology

Wednesday September 2, 2026 11:15 - 11:30 PDT
Georgia Ballroom B

General Session

about <br>

11:30 PDT

Evolving Legacy Systems Towards Strong Spatial and Temporal Isolation with seL4 - Philipp Scholl, ABB Corporate Research

Wednesday September 2, 2026 11:30 - 11:45 PDT

Georgia Ballroom B

ABB develops protection and control systems for safety-critical infrastructure in energy and transportation sectors. These systems operate under hard real-time constraints, require security and safety assurances, and incorporate legacy software developed over decades by multiple teams across heterogeneous operating systems. Recently, regulatory requirements like the EU Cyber Resilience Act [1]...
See More →

Speakers

Philipp Scholl

ABB Corporate Research

Wednesday September 2, 2026 11:30 - 11:45 PDT
Georgia Ballroom B

General Session

11:45 PDT

tSDX - Reference Architecture for Software Defined X - Nils Brand, Fraunhofer IESE

Wednesday September 2, 2026 11:45 - 12:00 PDT

Georgia Ballroom B

The demand for software-defined systems among businesses is growing rapidly. The software-defined paradigm has been known since the 1990s, originating in the telecommunications industry with software-defined radio. Since around 2021, innovation in the automotive industry has focused on implementing the software-defined vehicle paradigm. This led to the creation of COVESA, and in Europe, automakers...
See More →

Speakers

Nils Brand

Research & Business Development, Fraunhofer IESE

Wednesday September 2, 2026 11:45 - 12:00 PDT
Georgia Ballroom B

General Session

12:00 PDT

Lunchtime Poster Presentations

Wednesday September 2, 2026 12:00 - 13:30 PDT

Georgia Ballroom Foyer

1. TCCoE Overview & Update 2026 - Stuart Card, Critical Technologies, Inc. 2. Binary Verification for seL4 - Nick Spinale, Colias Group 3. VM Composer Poster - Robert VanVossem Dornerworks 4. Updates on Confidential Computing with seL4 - Alexander Weidinger, Fraunhofer AISEC 5. Rethinking seL4 Multicore Architecture: SMP vs. Multikernel - Guangtao Zhu & Julia...
See More →

Speakers

Stuart Card

Critical Technologies Inc.

Nick Spinale

Colias Group

Robert VanVossen

seL4 Technical Lead, Dornerworks

Alexander Weidinger

Research Associate, Fraunhofer AISEC

Guangtao Zhu

Student, UNSW Sydney

Julia Vassiliki

UNSW Sydney

Wednesday September 2, 2026 12:00 - 13:30 PDT
Georgia Ballroom Foyer

Poster Sessions

12:00 PDT

Lunch

Wednesday September 2, 2026 12:00 - 13:30 PDT

Wednesday September 2, 2026 12:00 - 13:30 PDT
Georgia A

Registration / Breaks / Special Events

13:30 PDT

seL4's Security Proofs - Ryan Barry, Proofcraft Systems

Wednesday September 2, 2026 13:30 - 14:00 PDT

Georgia Ballroom B

seL4’s flagship proof is functional correctness, which states that the C code behaves according to its abstract specification. This talk introduces the next layer in the assurance stack– seL4’s security proofs. We will present an overview of what they are, how they are structured, and where they fit into past, present, and future work at Proofcraft.The CIA triad of properties–...
See More →

Speakers

Ryan Barry

Proofcraft Systems

Wednesday September 2, 2026 13:30 - 14:00 PDT
Georgia Ballroom B

General Session

14:00 PDT

Trustworthy Systems R&D Update - Gernot Heiser, UNSW Sydney

Wednesday September 2, 2026 14:00 - 14:30 PDT

Georgia Ballroom B

This talk will give an overview of the (systems) research and development activities at UNSW Sydney’s Trustworthy Systems (TS) group. It will provide the context for the other TS talks that follow, and will provide details of the activities not covered by separate talks, including:- Microkit, driver framework and LionsOS progress- performance analysis of the seL4 SMP kernel vs the multikernel-...
See More →

Speakers

Gernot Heiser

Scientia Professor, UNSW Sydney

Wednesday September 2, 2026 14:00 - 14:30 PDT
Georgia Ballroom B

General Session

14:30 PDT

Where are we with Time Protection? Verification and Cross-domain Communication Update - Rob Sison, UNSW Sydney

Wednesday September 2, 2026 14:30 - 15:00 PDT

Georgia Ballroom B

This talk will give an update on the past two years’ advances at Trustworthy Systems in (1) our ongoing efforts to verify time protection for seL4, as well as (2) our implementation in seL4 of new time-protected cross-domain communication mechanisms on RISC-V Cheshire. On the formal verification front, I will present our results so far, thanks to a crucial rethink of our approach to verifying a...
See More →

Speakers

Rob Sison

Senior Research Associate, UNSW Sydney

Rob is a postdoc at UNSW Sydney who researches and develops formal methods, primarily for proving absences of information flow in systems for high-assurance use cases. In the past, their focus was on complications arising from concurrency and refinement to enable secure compilation... Read More →

Wednesday September 2, 2026 14:30 - 15:00 PDT
Georgia Ballroom B

General Session

15:00 PDT

Break

Wednesday September 2, 2026 15:00 - 15:30 PDT

Wednesday September 2, 2026 15:00 - 15:30 PDT
Georgia A

Registration / Breaks / Special Events

15:30 PDT

Pancake Updates - Miki Tanaka, UNSW

Wednesday September 2, 2026 15:30 - 16:00 PDT

Georgia Ballroom B

Pancake is a verification-friendly, imperative low-level language for systems programming, which the Trustworthy Systems group at UNSW has been working on to produce verified LionsOS components. Since first introduced in 2024 seL4 Summit, TS continued with Pancake development and Pancake is now mature enough for our systems engineers to take up and port various components originally written in C...
See More →

Speakers

Miki Tanaka

UNSW

Wednesday September 2, 2026 15:30 - 16:00 PDT
Georgia Ballroom B

General Session

16:00 PDT

Verifying seL4 device drivers with CN - Michal Podhradsky, Galois

Wednesday September 2, 2026 16:00 - 16:15 PDT

Georgia Ballroom B

While sDDF provides a framework for verification of new drivers with the Pancake language, and driver synthesis, the vast majority of current systems relies on proprietary hardware, and existing drivers written in C.In our project with DORNERWORKS we were tasked with verifying an ethernet driver for a deployed system. The ethernet device was similar to Intel e100 hardware. Given the relatively new...
See More →

Speakers

Michal Podhradsky

Galois

Wednesday September 2, 2026 16:00 - 16:15 PDT
Georgia Ballroom B

General Session

16:15 PDT

Formalising Device Protocols for sDDF Driver Verification - Liam Murphy, UNSW Sydney

Wednesday September 2, 2026 16:15 - 16:45 PDT

Georgia Ballroom B

Device drivers are a major source of bugs in operating systems, making them a primary target for formal verification. However, many of these bugs come from violations of the device’s protocol or faults in the device’s design, which cannot be prevented without a formal model of the device’s protocol. Such a model would traditionally be derived from the device’s datasheet, but the accuracy...
See More →

Speakers

Liam Murphy

UNSW Sydney

Wednesday September 2, 2026 16:15 - 16:45 PDT
Georgia Ballroom B

General Session

16:45 PDT

Verification of a UDP Implementation: Challenges and Solutions - Alain Kägi, Lewis & Clark College

Wednesday September 2, 2026 16:45 - 17:00 PDT

Georgia Ballroom B

In prior work, we have verified the correctness of a C implementation of UDPv6 using AutoCorres2, a tool to facilitate the verification of C programs in Isabelle/HOL. To achieve high performance, it is common practice for implementations of such network layers to make repeated small mutations to heap state, using typed pointers with overlapping address ranges. This approach to network...
See More →

Speakers

Alain Kägi

Assistant Professor, Lewis & Clark College

Wednesday September 2, 2026 16:45 - 17:00 PDT
Georgia Ballroom B

General Session

17:00 PDT

Closing Remarks

Wednesday September 2, 2026 17:00 - 17:10 PDT

Georgia Ballroom B

Wednesday September 2, 2026 17:00 - 17:10 PDT
Georgia Ballroom B

Keynote Sessions

08:30 PDT

Registration & Badge Pick-up

Thursday September 3, 2026 08:30 - 17:00 PDT

Georgia Ballroom Foyer

Thursday September 3, 2026 08:30 - 17:00 PDT
Georgia Ballroom Foyer

Registration / Breaks / Special Events

09:00 PDT

Ask Me Anything' with the TSC - Speakers To Be Announced

Thursday September 3, 2026 09:00 - 09:30 PDT

Georgia Ballroom B

Thursday September 3, 2026 09:00 - 09:30 PDT
Georgia Ballroom B

Keynote Sessions

09:30 PDT

Simplifying Microkit System Composition with Acacia - Lesley Rossouw, UNSW Sydney

Thursday September 3, 2026 09:30 - 10:00 PDT

Georgia Ballroom B

The seL4 Microkit has a problem: composing systems becomes very difficult when working with modular code or large code bases. The Microkit Acacia tool (formerly SDFgen) solves this problem by offering a higher-level abstraction for generating Microkit system files, capable of inserting modules with minimal effort. Acacia has been used extensively as a component of LionsOS and the seL4 Device...
See More →

Speakers

Lesley Rossouw

UNSW Sydney

Thursday September 3, 2026 09:30 - 10:00 PDT
Georgia Ballroom B

Walkthrough / Tutorial

10:00 PDT

Break

Thursday September 3, 2026 10:00 - 10:30 PDT

Thursday September 3, 2026 10:00 - 10:30 PDT
Georgia A

Registration / Breaks / Special Events

10:30 PDT

A Policy-free Boot Process for seL4 - Daniel Schwyn, Neutrality

Thursday September 3, 2026 10:30 - 11:00 PDT

Georgia Ballroom B

In its current form, the initialization code of the seL4 kernel dictates the policy of how resources are discovered and what capabilities are created at boot time, making it hard to integrate into existing boot infrastructure. Wepropose to delegate this policy to a pre-boot component and introduce both an interface and mechanisms for pre-boot infrastructure to communicate resources to the kernel...
See More →

Speakers

Daniel Schwyn

Senior Engineer, Neutrality

Thursday September 3, 2026 10:30 - 11:00 PDT
Georgia Ballroom B

General Session

11:00 PDT

Carrels: Secure, High-performance Microservice on seL4 - Guangtao Zhu, UNSW Sydney

Thursday September 3, 2026 11:00 - 11:30 PDT

Georgia Ballroom B

seL4, the world’s first formally verified microkernel, has demonstrated exceptional reliability in security- and safety-critical systems. However, its use in large-scale, server-class environments remains underexplored, especially for dynamic workloads such as microservices.In this talk, we present Carrels, a secure and high-performance platform for lightweight, dynamic applications on seL4....
See More →

Speakers

Guangtao Zhu

Student, UNSW Sydney

Thursday September 3, 2026 11:00 - 11:30 PDT
Georgia Ballroom B

General Session

11:30 PDT

Single Kernel Multicore seL4 - Scott Brookes, Riverside Research

Thursday September 3, 2026 11:30 - 11:45 PDT

Georgia Ballroom B

Riverside Research presents an seL4 prototype called SKMS: Single Kernel Multicore seL4. SKMS is a proof-of-concept implementation of a previously proposed multicore microkernel architecture [1] for seL4 microkernel on x86. The current POC implements three basic elements of seL4 functionality: memory isolation, remote system calls, and remote scheduling. Memory isolation puts usperspace processes...
See More →

Speakers

Scott Brookes

Riverside Research

Thursday September 3, 2026 11:30 - 11:45 PDT
Georgia Ballroom B

General Session

11:45 PDT

Booting Windows on an x86-64 seL4-based VMM - Bill Nguyen, UNSW Sydney

Thursday September 3, 2026 11:45 - 12:00 PDT

Georgia Ballroom B

Historically, open-source Virtual Machine Monitors (VMMs) built on seL4 have focused largely on Linux guest OS support. Booting a closed-source operating system like Windows on a custom x86-64 VMM introduces a unique set of development hurdles.This talk details the engineering effort behind LionsOS to achieve a fully functional x86-64 VMMcapable of running modern Windows and desktop Linux...
See More →

Speakers

Bill Nguyen

UNSW Sydeny

Thursday September 3, 2026 11:45 - 12:00 PDT
Georgia Ballroom B

General Session

12:00 PDT

Lunch

Thursday September 3, 2026 12:00 - 13:30 PDT

Thursday September 3, 2026 12:00 - 13:30 PDT
Georgia A

Registration / Breaks / Special Events

12:30 PDT

Lunchtime Poster Presentations

Thursday September 3, 2026 12:30 - 13:30 PDT

Georgia Ballroom Foyer

1. TCCoE Overview & Update 2026 - Stuart Card, Critical Technologies, Inc.2. Binary Verification for seL4 - Nick Spinale, Colias Group3. VM Composer Poster - Robert VanVossem Dornerworks4. Updates on Confidential Computing with seL4 - Alexander Weidinger, Fraunhofer AISEC5. Rethinking seL4 Multicore Architecture: SMP vs. Multikernel - GuangtaoZhu & Julia Vassiliki, UNSW...
See More →

Speakers

Stuart Card

Critical Technologies Inc.

Nick Spinale

Colias Group

Robert VanVossen

seL4 Technical Lead, Dornerworks

Alexander Weidinger

Research Associate, Fraunhofer AISEC

Guangtao Zhu

Student, UNSW Sydney

Julia Vassiliki

UNSW Sydney

Thursday September 3, 2026 12:30 - 13:30 PDT
Georgia Ballroom Foyer

Poster Sessions

13:30 PDT

Rigorous Agentic Systems Engineering for seL4 using HAMR - John Hatcliff, Kansas State University

Thursday September 3, 2026 13:30 - 14:00 PDT

Georgia Ballroom B

The Collins Aerospace INSPECTA project (part of the DARPA PROVERS program) aims to provide a model-based development tool chain for seL4 with integrated formal methods. The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) framework, whose development is led by researchers at Kansas State University, is a key part of the INSPECTA tool chain. HAMR supports modelbased...
See More →

Speakers

John Hatcliff

Professor, Kansas State University

Thursday September 3, 2026 13:30 - 14:00 PDT
Georgia Ballroom B

General Session

14:00 PDT

Accessible Formal Methods – Building on a Strong sel4 Foundation Nick Tudor, D-RisQ Ltd.

Thursday September 3, 2026 14:00 - 14:15 PDT

Georgia Ballroom B

While sel4 provides a sound foundation upon which to build, it remains the case that applications can be built that are on their own unsound, insecure and unsafe. The work to develop applications needs rigorous, accessible tool support in order to more quickly build and deploy assured software systems. For decades, formal methods have been acknowledged as a very powerful set of techniques with...
See More →

Speakers

Nick Tudor

D-RisQ Ltd

Thursday September 3, 2026 14:00 - 14:15 PDT
Georgia Ballroom B

General Session

14:15 PDT

Efficient User-level Physical Memory Management on seL4 - Guangtao Zhu, UNSW Sydney

Thursday September 3, 2026 14:15 - 14:30 PDT

Georgia Ballroom B

seL4 gives user-level systems a great deal of control over hardware resources through capability-protected kernel abstractions. This is powerful, but it also means that performance depends heavily on how user-level resource management is designed.In this talk, we use physical memory management as a case study. We show that the wrong design can make dynamic memory allocation expensive by placing...
See More →

Speakers

Guangtao Zhu

Student, UNSW Sydney

Thursday September 3, 2026 14:15 - 14:30 PDT
Georgia Ballroom B

General Session

14:30 PDT

Modeling and Performance Analysis of Ethernet on LionsOS - Lesley Rossouw, UNSW Sydney

Thursday September 3, 2026 14:30 - 14:45 PDT

Georgia Ballroom B

Performant networking is critical for many practical computer systems. Since 2022, the seL4 Device Driver Framework (sDDF) has included an Ethernet driver capable of strong performance without compromising on trustworthiness. Under LionsOS, the sDDF has been shown to be capable of supporting a variety of intensive use cases such as a firewall and webserver.In this talk we will discuss ongoing...
See More →

Speakers

Lesley Rossouw

UNSW Sydney

Thursday September 3, 2026 14:30 - 14:45 PDT
Georgia Ballroom B

General Session

15:00 PDT

BoF Session: Details To Be Announced

Thursday September 3, 2026 15:00 - 15:45 PDT

Georgia Ballroom B

Thursday September 3, 2026 15:00 - 15:45 PDT
Georgia Ballroom B

BoF Sessions

15:45 PDT

Break

Thursday September 3, 2026 15:45 - 16:15 PDT

Thursday September 3, 2026 15:45 - 16:15 PDT
Georgia A

Registration / Breaks / Special Events

16:15 PDT

BoF Session: Details To Be Announced

Thursday September 3, 2026 16:15 - 16:45 PDT

Georgia Ballroom B

Thursday September 3, 2026 16:15 - 16:45 PDT
Georgia Ballroom B

BoF Sessions

16:45 PDT

BoF Wrap-up

Thursday September 3, 2026 16:45 - 17:00 PDT

Georgia Ballroom B

Thursday September 3, 2026 16:45 - 17:00 PDT
Georgia Ballroom B

BoF Sessions

17:00 PDT

Closing Remarks

Thursday September 3, 2026 17:00 - 17:10 PDT

Georgia Ballroom B

Thursday September 3, 2026 17:00 - 17:10 PDT
Georgia Ballroom B

Keynote Sessions