Loading…
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.
Tuesday, September 1
 

08:00 PDT

Registration & Badge Pick-up
Tuesday September 1, 2026 08:00 - 17:00 PDT

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

09:00 PDT

Welcome - Robert VanVossen, seL4 Technical Lead, DornerWorks
Tuesday September 1, 2026 09:00 - 09:10 PDT

Speakers
avatar for Robert VanVossen

Robert VanVossen

seL4 Technical Lead, DornerWorks

Tuesday September 1, 2026 09:00 - 09:10 PDT
Plaza A & B

09:10 PDT

Keynote: The Age of Software Understanding - Anjana Rajan, CEO & Co-Founder, Atalanta
Tuesday September 1, 2026 09:10 - 10:00 PDT
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
avatar for Anjana Rajan

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

10:00 PDT

Break
Tuesday September 1, 2026 10:00 - 10:30 PDT
  • Spiced and Sweet Loaves (Veg): All Homemade Lemon Poppy Seed, Banana, Carrot
  • Seasonal Yogurt Parfait
  • Individual Coconut Yogurt Cups
  • Seasonally Inspired Sliced Fruit

  • Tuesday September 1, 2026 10:00 - 10:30 PDT
    Plaza C

    10:30 PDT

    seL4: What, Why, Who and Where? - June Andronick, Proofcraft and seL4 Foundation
    Tuesday September 1, 2026 10:30 - 11:30 PDT
    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
    avatar for June Andronick

    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

    11:30 PDT

    10 Years of seL4 at NCSC - Adam, NCSC
    Tuesday September 1, 2026 11:30 - 12:00 PDT
    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
    AW

    Adam W1

    Lead Verification Researcher, NCSC

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

    12:00 PDT

    Lunch
    Tuesday September 1, 2026 12:00 - 13:30 PDT
    Tossed Green Salad (GF, Vegan): Seasonal Shaved Vegetables, Fresh Berries, Black Pepper and Berry VinaigrettePotato Street Corn Salad (GF, Veg): Baby Potato, Green Onion, Lime, Pepperoncini, Chili, FetaBread: Focaccia Bun, Organic Ancient Grain Sliced Bread, and Gluten Free BreadCondiments: Mayonnaise, Pesto Aioli, Dijon Mustard (GF, DF, Veg)Protein: Smoked Turkey (GF, DF), Shaved Homemade Roasted...
    See More →
    Tuesday September 1, 2026 12:00 - 13:30 PDT
    Plaza C

    13:30 PDT

    “Staying in the Red Queen's Race”: Organizing Small and Medium Sized FOSS Communities in a World of Regulations and AI - Alistair Woodman, Erlang Ecosystem Foundation (EEF)
    Tuesday September 1, 2026 13:30 - 14:00 PDT
    In this 'Voices from Nearby' session, I will provide thoughts and insights into how the Erlang Ecosystem Foundation (EEF) has been self-organizing to survive and thrive for the foreseeable future.The EEF was founded in 2019 as a not-for-profit primarily focused on community marketing and outreach to the next generation of programmers to get involved with functional programming and the BEAM...
    See More →
    Speakers
    avatar for Alistair Woodman

    Alistair Woodman

    Board Member, Erlang Ecosystem Foundation (EEF)
    Alistair Woodman, High-tech plumber.
    I've been doing community/business development work for FOSS projects for the last 15 years. A physicist by education and doer by inclination, I worked in the networking and communications space since the 1980s. Product management jobs at Apple and Cisco kept me busy for over 25 years
    ... Read More →
    Tuesday September 1, 2026 13:30 - 14:00 PDT
    Plaza A & B

    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
    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
    avatar for David Hardin

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

    14:30 PDT

    Kry10 OS Software Safety Manual - Ihor Kuz, Kry10
    Tuesday September 1, 2026 14:30 - 15:00 PDT
    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
    avatar for Ihor Kuz

    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

    15:00 PDT

    Break
    Tuesday September 1, 2026 15:00 - 15:30 PDT
  • Popcorn Station (Vegan): Truffle Sea Salt, Togarashi, Salt and Vinegar
  • Freshly Baked Home-Style Cookies: Chocolate Chip Chunk, White Chocolate Macadamia, Oatmeal Raisin

  • Tuesday September 1, 2026 15:00 - 15:30 PDT
    Plaza C

    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
    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
    avatar for Jonathan Marshall

    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

    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
    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
    avatar for June Andronick

    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 15:45 - 16:00 PDT
    Plaza A & B

    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
    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...
    See More →
    Speakers
    avatar for Darren Cofer

    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 →
    avatar for Martin Dehnel-Wild

    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 →
    avatar for Anjana Rajan

    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 →
    avatar for Peter Davies

    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 →
    avatar for Jonathan Marshall

    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 →
    avatar for James Sharp

    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

    17:00 PDT

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

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

    18:30 PDT

    Conference Dinner - Sponsored by Riverside Research
    Tuesday September 1, 2026 18:30 - 20:30 PDT
    Join us at Chambar - 
    Tuesday September 1, 2026 18:30 - 20:30 PDT
    Chambar 568 Beatty St, Vancouver, BC V6B 2L3
     
    Wednesday, September 2
     

    08:00 PDT

    Registration & Badge Pick-up
    Wednesday September 2, 2026 08:00 - 17:00 PDT

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

    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
    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
    avatar for Martin Dehnel-Wild

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

    09:50 PDT

    Announcements - June Andronick, Proofcraft & seL4 Foundation
    Wednesday September 2, 2026 09:50 - 10:00 PDT

    Speakers
    avatar for June Andronick

    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 →
    Wednesday September 2, 2026 09:50 - 10:00 PDT
    Plaza A & B

    10:00 PDT

    Break
    Wednesday September 2, 2026 10:00 - 10:30 PDT
  • Today's Fresh Bakery (Strudels)
    • Leek Parmesan
    • Tomato Olive
    • Spinach Feta
  • Mango Tapioca Pudding (GF, Vegan)
    • Berry Compote

  • Wednesday September 2, 2026 10:00 - 10:30 PDT
    Plaza C

    10:30 PDT

    Cyber-Hardened Satellite Software (CHSS) VMM - Robert VanVossen, Dornerworks
    Wednesday September 2, 2026 10:30 - 11:00 PDT
    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
    avatar for Robert VanVossen

    Robert VanVossen

    seL4 Technical Lead, DornerWorks

    Wednesday September 2, 2026 10:30 - 11:00 PDT
    Plaza A & B

    11:00 PDT

    Throwing seL4 on the Throwbot 3 Robot - Nathan Studer, Dornerworks
    Wednesday September 2, 2026 11:00 - 11:15 PDT
    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
    avatar for Nathan Studer

    Nathan Studer

    Technical Strategy Lead, Dornerworks

    Wednesday September 2, 2026 11:00 - 11:15 PDT
    Plaza A & B

    11:15 PDT

    Assured Robotics Embedded Systems and Applications in Ground Vehicles (ARSENAL) - Dave Lide & Biruk Sintayehu, Trusted Science and Technology
    Wednesday September 2, 2026 11:15 - 11:30 PDT
    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
    BS

    Biruk Sintayehu

    Trusted Science & Technology

    DL

    david lide

    director of engineering, trusted science and technology
    David Lide is Director of Engineering at Trusted Science and Technology and has spent the last 6 years working in the area of secure embedded systems. Prior to that, he spent many years with Texas Instruments, working for the Embedded Systems Division on a wide range of projects... Read More →
    Wednesday September 2, 2026 11:15 - 11:30 PDT
    Plaza A & B

    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
    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
    PS

    Philipp Scholl

    ABB Corporate Research
    Wednesday September 2, 2026 11:30 - 11:45 PDT
    Plaza A & B

    11:45 PDT

    tSDX - Reference Architecture for Software Defined X - Nils Brand, Fraunhofer IESE
    Wednesday September 2, 2026 11:45 - 12:00 PDT
    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
    avatar for Nils Brand

    Nils Brand

    Research & Business Development, Fraunhofer IESE
    Wednesday September 2, 2026 11:45 - 12:00 PDT
    Plaza A & B

    12:00 PDT

    Lunchtime Poster Presentations
    Wednesday September 2, 2026 12:00 - 13:30 PDT
    1. Rethinking seL4 Multicore Architecture: SMP vs. Multikernel - Guangtao Zhu, UNSW Sydney2. Binary Verification for seL4 - Nick Spinale, Colias Group 3. Updates on Confidential Computing with seL4 - Alexander Weidinger, Fraunhofer AISEC 4. VM Composer Poster - Robert VanVossem Dornerworks5. TCCoE Overview & Update 2026 - Stuart Card, Critical Technologies Inc.6....
    See More →
    Speakers
    avatar for Guangtao Zhu

    Guangtao Zhu

    Research Student, UNSW Sydney
    NS

    Nick Spinale

    Colias Group
    AW

    Alexander Weidinger

    Researcher, Fraunhofer AISEC
    avatar for Robert VanVossen

    Robert VanVossen

    seL4 Technical Lead, DornerWorks

    SC

    Stuart Card

    Critical Technologies Inc.
    YS

    Yanyan Shen

    Software Architect, NIO

    avatar for Martin Dehnel-Wild

    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 →
    avatar for June Andronick

    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 →
    Wednesday September 2, 2026 12:00 - 13:30 PDT
    Plaza Hallway
      Poster Sessions
    • Presentation Attached Yes

    12:00 PDT

    Lunch
    Wednesday September 2, 2026 12:00 - 13:30 PDT
    Chopped Salad (GF, VEG): Romaine Salad, Jalapeno Pepper, Cherry Tomato, Chickpeas, Parmesan, Champagne Parsley VinaigretteFingerling Potato Salad (GF, VEGAN): Cornichons, Capers, Green Onion, Shallots & Lemon VinaigretteRotini Pasta Salad (VEGAN): Pepperoncini, Red Onion, Sundried Tomato, Artichoke, Red Pepper, Parsley, Mint, Red Wine Oregano VinaigretteRoasted Garlic Sweet...
    See More →
    Wednesday September 2, 2026 12:00 - 13:30 PDT
    Plaza C

    13:30 PDT

    seL4's Security Proofs - Ryan Barry, Proofcraft Systems
    Wednesday September 2, 2026 13:30 - 14:00 PDT
    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
    RB

    Ryan Barry

    Proof Engineer, Proofcraft

    Wednesday September 2, 2026 13:30 - 14:00 PDT
    Plaza A & B

    14:00 PDT

    Trustworthy Systems R&D Update - Gernot Heiser, UNSW Sydney
    Wednesday September 2, 2026 14:00 - 14:30 PDT
    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
    avatar for Gernot Heiser

    Gernot Heiser

    Scientia Professor, UNSW Sydney

    Wednesday September 2, 2026 14:00 - 14:30 PDT
    Plaza A & B

    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
    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
    avatar for Rob Sison

    Rob Sison

    Senior Research Associate, UNSW
    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
    Plaza A & B

    15:00 PDT

    Break
    Wednesday September 2, 2026 15:00 - 15:30 PDT
  • Seasonally Inspired Sliced Fruit
  • Clif Organic Energy Bars (CN, VEG): Chocolate Chip, Chocolate Almond Fudge
  • Gluten Free Bars (GF): Gluten Free Chocolate Brownie, Gluten Free Nanaimo Bars, Gluten Free Quinoa & Date Bar

  • Wednesday September 2, 2026 15:00 - 15:30 PDT
    Plaza C

    15:30 PDT

    Pancake Updates - Miki Tanaka, UNSW
    Wednesday September 2, 2026 15:30 - 16:00 PDT
    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
    MT

    Miki Tanaka

    Senior Proof Engineer, UNSW
    Wednesday September 2, 2026 15:30 - 16:00 PDT
    Plaza A & B

    16:00 PDT

    Verifying seL4 device drivers with CN - Peter "Gus" O'Hanley, Galois
    Wednesday September 2, 2026 16:00 - 16:15 PDT
    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
    avatar for Peter

    Peter "Gus" O'Hanley

    Research Engineer, Galois
    Gus earned his bachelor's degree in computer science from the University of Minnesota. There, he was introduced to Haskell, became interested in programming language theory and type theory, and began his journey towards working with systems software.  

    Before coming to Galois, he co-founded his own firmware development company and worked at HPE on specialized server firmware... Read More →
    Wednesday September 2, 2026 16:00 - 16:15 PDT
    Plaza A & B

    16:15 PDT

    Formalising Device Protocols for sDDF Driver Verification - Liam Murphy, UNSW Sydney
    Wednesday September 2, 2026 16:15 - 16:45 PDT
    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
    LM

    Liam Murphy

    MPhil Student, UNSW Sydney

    Wednesday September 2, 2026 16:15 - 16:45 PDT
    Plaza A & B

    16:45 PDT

    Verification of a UDP Implementation: Challenges and Solutions - Daniel Neshyba-Rowe, Independent
    Wednesday September 2, 2026 16:45 - 17:00 PDT
    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
    DN

    Daniel Neshyba-Rowe

    Lewis & Clark

    Wednesday September 2, 2026 16:45 - 17:00 PDT
    Plaza A & B

    17:00 PDT

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

    Wednesday September 2, 2026 17:00 - 17:10 PDT
    Plaza A & B
     
    Thursday, September 3
     

    08:30 PDT

    Registration & Badge Pick-up
    Thursday September 3, 2026 08:30 - 17:00 PDT

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

    09:00 PDT

    Ask Me Anything' with the TSC - Speakers To Be Announced
    Thursday September 3, 2026 09:00 - 09:30 PDT

    Thursday September 3, 2026 09:00 - 09:30 PDT
    Plaza A & B

    09:30 PDT

    Simplifying Microkit System Composition with Acacia - Lesley Rossouw, UNSW Sydney
    Thursday September 3, 2026 09:30 - 10:00 PDT
    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
    LR

    Lesley Rossouw

    Operating Systems Engineer, UNSW Sydney (Trustworthy Systems)
    I am an OS engineer at the Trustworthy Systems Group, a research group @ The University of New South Wales. I am a maintainer for the seL4 Device Driver Framework and several other internal projects.

    I am a computer engineer by training.
    Thursday September 3, 2026 09:30 - 10:00 PDT
    Plaza A & B

    10:00 PDT

    Break
    Thursday September 3, 2026 10:00 - 10:30 PDT
  • Chocolate Brioche
  • Seasonal Yogurt Parfait (CN, Veg): Wild Blossom Honey Greek Yogurt, Chef's Selection Fruit Compote, House Made Granola
  • Individual Coconut Yogurt Cups

  • Thursday September 3, 2026 10:00 - 10:30 PDT
    Plaza C

    10:30 PDT

    A Policy-free Boot Process for seL4 - Daniel Schwyn, Neutrality
    Thursday September 3, 2026 10:30 - 11:00 PDT
    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. We propose 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
    avatar for Daniel Schwyn

    Daniel Schwyn

    Senior Engineer, Neutrality
    Thursday September 3, 2026 10:30 - 11:00 PDT
    Plaza A & B

    11:00 PDT

    Carrels: Secure, High-performance Microservice on seL4 - Guangtao Zhu, UNSW Sydney
    Thursday September 3, 2026 11:00 - 11:30 PDT
    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
    avatar for Guangtao Zhu

    Guangtao Zhu

    Research Student, UNSW Sydney
    Thursday September 3, 2026 11:00 - 11:30 PDT
    Plaza A & B

    11:30 PDT

    Single Kernel Multicore seL4 - David Swasey & Scott Brookes, Riverside Research
    Thursday September 3, 2026 11:30 - 11:45 PDT
    Riverside Research presents a seL4 prototype called SKMS: Single Kernel Multicore seL4. SKMS is a proof-of-concept implementation of a previously proposed multicore microkernel architecture [1] for the 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 userspace...
    See More →
    Speakers
    avatar for Scott Brookes

    Scott Brookes

    Associate Director, Riverside Research
    Dr. Scott Brookes is an Associate Director in the Secure and Resilient Systems group at Riverside Research. He earned his Ph.D. from Dartmouth College in 2018, where he studied secure operating system and hypervisor architectures. He has worked in software targeting security ISAs... Read More →
    avatar for David Swasey

    David Swasey

    Senior Research Scientist – Formal Methods, Riverside Research
    David Swasey is a senior research scientist in Secure and Resilient Systems at Riverside Research. He has conducted research in program logics, robust safety, and proof-carrying authorization and has extensive experience verifying low-level systems code.
    Thursday September 3, 2026 11:30 - 11:45 PDT
    Plaza A & B

    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
    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
    BN

    Bill Nguyen

    Operating Systems Engineer, University of New South Wales
    Thursday September 3, 2026 11:45 - 12:00 PDT
    Plaza A & B

    12:00 PDT

    Lunch
    Thursday September 3, 2026 12:00 - 13:30 PDT
    Artisan Buns with Fresh ButterAsian Chopped Salad (GF, DF, VEG): Rainbow Cabbage, Edamame, Quinoa, Peppers, Cilantro, Green Onion, Tamari-Sesame VinaigretteThai Tofu Salad (GF, DF, VEG): Japanese Eggplant, Chive, Tomato, Romaine, Cilantro with Ginger-Lime DressingSweet Corn & Sweet Potato Salad (GF, DF, VEGAN): Garbanzo Beans, Red Onion, Mint, Cilantro with Yuzu VinaigretteWhite Rice (GF, DF,...
    See More →
    Thursday September 3, 2026 12:00 - 13:30 PDT
    Plaza C

    12:30 PDT

    Lunchtime Poster Presentations
    Thursday September 3, 2026 12:30 - 13:30 PDT
    1. Rethinking seL4 Multicore Architecture: SMP vs. Multikernel - Guangtao Zhu, UNSW Sydney2. Binary Verification for seL4 - Nick Spinale, Colias Group3. Updates on Confidential Computing with seL4 - Alexander Weidinger, Fraunhofer AISEC 4. VM Composer Poster - Robert VanVossem Dornerworks5. TCCoE Overview & Update 2026 - Stuart Card, Critical...
    See More →
    Speakers
    avatar for Guangtao Zhu

    Guangtao Zhu

    Research Student, UNSW Sydney
    NS

    Nick Spinale

    Colias Group
    AW

    Alexander Weidinger

    Researcher, Fraunhofer AISEC
    avatar for Robert VanVossen

    Robert VanVossen

    seL4 Technical Lead, DornerWorks

    SC

    Stuart Card

    Critical Technologies Inc.
    YS

    Yanyan Shen

    Software Architect, NIO

    avatar for Martin Dehnel-Wild

    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 →
    avatar for June Andronick

    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 →
    Thursday September 3, 2026 12:30 - 13:30 PDT
    Plaza Hallway
      Poster Sessions
    • Presentation Attached Yes

    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
    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
    JH

    John Hatcliff

    Professor, Kansas State University
    Thursday September 3, 2026 13:30 - 14:00 PDT
    Plaza A & B

    14:00 PDT

    Efficient User-level Physical Memory Management on seL4 - Guangtao Zhu, UNSW Sydney
    Thursday September 3, 2026 14:00 - 14:15 PDT
    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
    avatar for Guangtao Zhu

    Guangtao Zhu

    Research Student, UNSW Sydney
    Thursday September 3, 2026 14:00 - 14:15 PDT
    Plaza A & B

    14:15 PDT

    Modeling and Performance Analysis of Ethernet on LionsOS - Lesley Rossouw, UNSW Sydney
    Thursday September 3, 2026 14:15 - 14:30 PDT
    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
    LR

    Lesley Rossouw

    Operating Systems Engineer, UNSW Sydney (Trustworthy Systems)
    I am an OS engineer at the Trustworthy Systems Group, a research group @ The University of New South Wales. I am a maintainer for the seL4 Device Driver Framework and several other internal projects.

    I am a computer engineer by training.
    Thursday September 3, 2026 14:15 - 14:30 PDT
    Plaza A & B

    14:30 PDT

    Building Safe Display Diodes with seL4 - Andrew Ruef, Institute for Defense Analyses
    Thursday September 3, 2026 14:30 - 14:45 PDT
    A critical part of secure system design is isolating data plane connectivity between different sensitivity domains. This is sound security practice because crossing data planes is tricky for attackers, however it also makes life difficult for end users - sometimes you want to connect to the Internet without walking to a different terminal. We have implemented a software based architecture that...
    See More →
    Speakers
    AR

    Andrew Ruef

    Institute for Defense Analyses

    Thursday September 3, 2026 14:30 - 14:45 PDT
    Plaza A & B

    14:45 PDT

    Break
    Thursday September 3, 2026 14:45 - 15:15 PDT

    Thursday September 3, 2026 14:45 - 15:15 PDT
    Plaza C

    15:15 PDT

    BoF Session: Details To Be Announced
    Thursday September 3, 2026 15:15 - 16:00 PDT

    Thursday September 3, 2026 15:15 - 16:00 PDT
    Plaza A & B

    16:00 PDT

    Break
    Thursday September 3, 2026 16:00 - 16:15 PDT
  • Tarts (CN, Veg): Maple Pecan, Chocolate Salted Caramel and Lemon
  • Popcorn Station (Vegan): Truffle Sea Salt (Vegan), Togarashi (Vegan), Salt and Vinegar (Vegan)
  • Vegan Power Bars (GF, CN, Vegan): Cranberry Nut & Seed, Coconut & Almond

  • Thursday September 3, 2026 16:00 - 16:15 PDT
    Plaza C

    16:15 PDT

    BoF Session: Details To Be Announced
    Thursday September 3, 2026 16:15 - 17:00 PDT

    Thursday September 3, 2026 16:15 - 17:00 PDT
    Plaza A & B
      BoF Sessions
    • Presentation Attached Yes

    17:00 PDT

    BoF Wrap-up
    Thursday September 3, 2026 17:00 - 17:15 PDT

    Thursday September 3, 2026 17:00 - 17:15 PDT
    Plaza A & B

    17:15 PDT

    Closing Remarks
    Thursday September 3, 2026 17:15 - 17:25 PDT

    Thursday September 3, 2026 17:15 - 17:25 PDT
    Plaza A & B
     
    • Filter By Date
    • Filter By Venue
    • Filter By Type
    • Presentation Attached
    • Timezone

    Share Modal

    Share this link via

    Or copy link

    Filter sessions
    Apply filters to sessions.