The seL4 Summit 2025

seL4 Summit 2025 Program

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

Program-at-a-glance

Keynote Talks Panel Talks Talks Reception Talks Talks Talks Talks BoFs BoFs Wed Sep 3 Tue Sep 2 Thu Sep 4 Fri Sep 5 Informal Social Activities Keynote Day 1 Day 2 Day 3

Main Program

All times are local time in Prague, Czech Republic (GMT+2).

See the Schedule on LF Events.

Timing of sessions and room locations are subject to change.

Day 1 3 September 2025
9:00 - 9:10
Welcome
Nick Spinale, Colias Group
9:10 - 10:00
Keynote
Model-based Development for seL4 Microkit/Rust with Integrated Formal Methods using HAMR
John Hatcliff, Jason Belt, Robby, Stefan Hallerstede, Robert VanVossen, Junaid Babar, Kansas State University, Aarhus University, Dornerworks, Collins Aerospace
Break
10:30 - 11:00
The next 700 verified seL4 platforms
Gerwin Klein, Proofcraft
11:00 - 11:30
FPGA based Accelerators w/ Microkit
Wanja Zaeske on behalf of Vincent Janson, German Aerospace Center (DLR)
11:30 - 12:00
seL4 on Big Iron: Experiences and recommendations from Neutrality's Atoll hypervisor
David Cock, Neutrality
Lunch
13:30 - 13:45
A program logic for seL4-based system verification
Matt Brecknell, Kry10
13:45 - 14:00
A Verified, High-Performance, IPv6 Network Stack
Alain Kägi, Daniel Neshyba-Rowe, Lewis & Clark College
14:00 - 14:30
Verified ZynqMP DMA Driver in Concurrent Separation Logic
Gordon Stewart, Riverside Research
14:30 - 15:15
Science, Engineering, Craft, Magic - Revolutions in the field of Software
Boyd Multerer, Kry10
Break
15:45 - 16:15
Towards Dependable System Services on seL4
Yanyan Shen, Dhammika Elkaduwe, NIO
16:15 - 16:45
Porting NASA's core Flight System to Magnetite on seL4
Juliana Furgala, Samuel Jero, MIT Lincoln Laboratory
16:45 - 17:15
Integration of seL4 in a Flight Vehicle Mission System
Darren Cofer, Collins Aerospace
Reception @ Červený Jelen 18:30
Day 2 4 September 2025
9:00 - 9:45
Panel
Building a business case for using a verified kernel
Darren Cofer, Robbie VanVossen, Boyd Multerer, Peter de Ridder, Yanyan Shen, Juliana Furgala (moderator), Collins Aerospace, DornerWorks, Kry10, MEP, NIO, MIT Lincoln Laboratory
9:45 - 10:00
seL4 Foundation update
June Andronick, seL4 Foundation
Break
10:30 - 11:00
Sculpt OS - a dynamic general-purpose OS powered by Genode on seL4
Alexander Boettcher, Sebastian Sumpf, Genode Labs
11:00 - 11:30
CellulOS: An OS for comparing Isolation Mechanisms
Sid Agrawal, Arya Stevinson, Linh Pham, Ethan Xu, Shaurya Patel, Hugo Lefeuvre, Aastha Mehta, Reto Achermann, Margo Seltzer, University of British Columbia, Oracle, Hammerspace
11:30 - 12:00
Rust-based drivers and verified rust applications on seL4
Robbie VanVossen, DornerWorks
Lunch
13:30 - 13:45
Porting seL4 to the RISC-V SoC, toward a Secure and High-Performance RISC-V AI Platform
Yuning Liang, Deep Computing
13:45 - 14:00
SureVoice Solid
Peter de Ridder, MEP
14:00 - 15:00
Deep Dive
Trustworthy Systems R&D Update
Gernot Heiser, UNSW Sydney
Break
15:30 - 16:15
Dividing Timelines to Verify seL4 Applications
Thomas Sewell, UNSW Sydney
16:15 - 16:45
Verifying Device Drivers with Pancake
Junming Zhao, UNSW Sydney
16:45 - 17:00
Improving Confidential Computing with seL4: A Promising Guest OS Solution
Alexander Weidinger, Fraunhofer AISEC
Day 3 5 September 2025
9:00 - 9:50
Keynote
Ecosystem formally verifiable IT – provable Cybersecurity (EvIT)
Sebastian Jester, Cyberagentur
9:50 - 10:00
Announcements
June Andronick, seL4 Foundation
Break
10:30 - 11:00
A Deep Dive into seL4’s Binary Verification Story
Nick Spinale, Colias Group
11:00 - 11:15
Discussion, BoF Teasers
11:15 - 12:00
BoFs
Lunch
13:30 - 14:15
BoFs
14:15 - 14:30
BoF Wrap-up
14:30 - 14:45
Concluding Remarks
Robbie VanVossen, DornerWorks

Social Activities

A number of informal social activities are being organised for Tuesday Sep 2, 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.
  • Prague Old Town

    Prague Old Town & Josefov Walking Tour

    Join June Andronick on a walking tour of the old town.

    Date: Tuesday Sep 2, 2025
    Time: 2pm
    Cost: Free, but bookings are essential. Guides earn their money with tips.
    Details: Free walking tour website
    Location: Powder Tower Tower

  • Prague Castle

    Prague Castle

    Visit the Prague Castle.

    We're looking for a volunteer to be the point of contact for this activity. Please email summit@sel4.systems if you're interested.

    Date: Tuesday Sep 2, 2025
    Time: 2pm
    Cost: ~18 Euro, book online.
    Details: Visiting the castle
    Location: Prague Castle

  • Prague Astronomical Clock Tower

    Prague Astronomical Clock Tower

    Go on a guided tour of the Prague Astronomical Clock Tower.

    We're looking for a volunteer to be the point of contact for this activity. Please email summit@sel4.systems if you're interested.

    Date: Tuesday Sep 2, 2025
    Time: 1:45pm, for a tour starting at 2pm
    Cost: ~14 Euro entry + ~6 Euro for the guided tour.
    Details: Official website
    Location: Ticket Office on the ground floor of the Astronomical Clock Tower

  • Prague River

    Prague Sightseeing Cruise

    Join Martin Decky on the Prague River sightseeing cruise.

    Date: Tuesday Sep 2, 2025
    Time: 2pm
    Cost: Tickets from 18 Euro
    Details: Find out more on the cruise website
    Location: Prague Boats