Gernot Heiser

The seL4 microkernel is one of the most solid foundations for building secure systems. But to fully trust the programs running on top of it, we still need formal proofs that they behave exactly as… | ... The seL4 microkernel is one of the most solid foundations for building secure systems. But to fully trust the programs running on top of it, we still need formal proofs that they behave exactly as int...

Happy to share that California-based Foresight Institute has awarded us a grant for our work on bridging gap between verification of user-level components and the #seL4 specification.
This will enable end-to-end verification of a complete operating system.

www.linkedin.com/feed/update/...

Registration open for the seL4 summit 2026 We have an exciting new format for 2026! A full first day dedicated to applications, overviews, and perspectives on seL4-based systems and formally verified software in the real world. Followed by two...

Registration is open for this year’s #seL4 Summit in Vancouver, 1–3 September: sel4.discourse.group/t/registrati...

#firewalls | ExploitChance (Grupo Pentest®) We’re pleased to announce that Numantia will be adopting LionsOS, built on the seL4 microkernel, to run a dedicated packet-filtering specific component inside our appliance. This design choice reflect...

First publicised use of the #seL4-based #LionsOS in a commercial product: www.linkedin.com/feed/update/...

Welcome Fraunhofer AISEC to the #seL4 Foundation!

sel4.systems/news/#01-28

The Call for Presentations for the #seL4 Summit is out!

sel4.systems/news/#01-23

Riverside Research joins the seL4 Foundation

sel4.systems/news/#01-19

yes, this is a true shock!
Emma was a great person

Recent formal-methods PD looking for an exciting opportunity? Such as living in Sydney and contributing to end-to-end verification of LionsOS?
Here’s your chance: external-careers.jobs.unsw.edu.au/cw/en/job/53...

Gerald Heiser: Ein Blick auf den führenden Experten für Betriebssysteme Gerald Heiser ist ein Name, der in der Welt der Informatik und insbesondere im Bereich der Betriebssysteme und Cybersicherheit

AI at work, with some hilarious assertions. But WHY??? investorbit.de/menschen/ger...

Nice move, Kathleen!

Interested in contributing to the #seL4 ecosystem, maybe seing your contributions deployed?
Trustworthy Systems has released a firewall as a community project. It’s well-documented, easy to get started with, and there are plenty of parts to contribute. Details at trustworthy.systems/news/#lionso...

Genode Sculpt OS runs on #seL4: sel4.systems/news/#sculpt

Spring time is Jacaranda time in Sydney – the city is full of those magnificent trees

YouTube video by Seb Sg Paul Compton Memorial

Last week we had a memorial event for my former colleague and boss Prof Paul Compton. It was captured in this video: www.youtube.com/watch?v=isq-...
I was asked to summarise my memories of Paul, the are at 57:40–62:50

The #seL4 Foundation is inviting the community to a survey on the location of next year’s #Summit: sel4.discourse.group/t/sel4-summi...

The recordings of all presentations from this month's #seL4 Summit are up: sel4.systems/news/2025.ht...

Schedule | LF Events Please note: This schedule is automatically displayed in Central European Summer Time (CEST / UTC+2). To see the schedule in your preferred timezone, please select from the drop-down menu to the right...

Regrettably I didn’t take a picture, but one of the coolest talks at the #seL4 Summit was Alexander Böttcher: “Sculpt OS – a dynamic, general-purpose OS powered by Genode on seL4”. It was presented on a laptop running Sculpt OS!
events.linuxfoundation.org/sel4-summit/...

#seL4 for secure voice communication for aircraft: Peter de Ridder from MEP at the seL4 Summit

Again Kaegi at the #seL4 Summit reports on progress on verifying an IPv6 attack with a bunch of undergraduate students

Side Agrawal from UBC discusses evaluating isolation mechanisms at the #seL4 Summit

#seL4 Foundation CEO June Andronick's update reveals that we'll be moving to a new structure, based in Switzerland! Members will no longer have to pay for Linux Foundation membership

Day 2 of the seL4 Summit kicks off with an industry panel discussing making a business case for a verified kernel

Yayan Shen from NIO talks at the #seL4 Summit about fault tolerant designs. Also, after launching their seL4-based OS in their new entry- level brand, it now runs in NIO-branded premium EVs

Gerwin at the #seL4 Summit talking about making the verification generic, so on new platforms the kernel can be verified quickly

Recordings will be published within a week or so

The #seL4 Summit is underway in Prague!
John Hatcliff from Kansas State kicks off with a keynote on model- based system development on seL4, as used in various DARPA projects

And this is how it looks inside, running seL4, Microkit, LionsOS, native device drivers and reusing an unmodified Linux display driver

The humble TS Kitty has just returned from its third overseas trip, having now had gigs in four continents

TS celebrating seL4 Day

Today is the 16th anniversary of the completion of se4’s proof of implementation correctness, and the 11th anniversary of seL4 being open-sourced.
Happy #seL4 Day from all at Trustworthy Systems!

The recording of my CASA/MPI-SP Distinguished Lecture is now available – thanks for hosting me!

casa.rub.de/veranstaltun...