Gernot Heiser
@microkerneldude.bsky.social
Physicist by training, computer engineer by passion
Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney and Founding Chairman of the seL4 Foundation
FACM FIEEE FTSE FRSN ML
Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney and Founding Chairman of the seL4 Foundation
FACM FIEEE FTSE FRSN ML
Genode Sculpt OS runs on #seL4: sel4.systems/news/#sculpt
seL4 News | seL4
sel4.systems
November 12, 2025 at 10:31 AM
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
November 6, 2025 at 10:04 AM
Spring time is Jacaranda time in Sydney – the city is full of those magnificent trees
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
I was asked to summarise my memories of Paul, the are at 57:40–62:50
Paul Compton Memorial
YouTube video by Seb Sg
www.youtube.com
October 30, 2025 at 5:44 AM
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
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...
sel4.discourse.group
October 13, 2025 at 7:41 AM
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...
seL4 News | seL4
sel4.systems
September 23, 2025 at 1:32 AM
The recordings of all presentations from this month's #seL4 Summit are up: sel4.systems/news/2025.ht...
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/...
events.linuxfoundation.org/sel4-summit/...
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...
events.linuxfoundation.org
September 8, 2025 at 6:34 AM
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/...
events.linuxfoundation.org/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
September 4, 2025 at 7:59 AM
#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
September 4, 2025 at 7:05 AM
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
September 3, 2025 at 2:21 PM
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
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
John Hatcliff from Kansas State kicks off with a keynote on model- based system development on seL4, as used in various DARPA projects
September 3, 2025 at 7:37 AM
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
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
August 18, 2025 at 12:42 AM
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
August 18, 2025 at 12:33 AM
The humble TS Kitty has just returned from its third overseas trip, having now had gigs in four continents
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!
Happy #seL4 Day from all at Trustworthy Systems!
July 29, 2025 at 2:26 AM
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!
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...
casa.rub.de/veranstaltun...
CASA Distinguished Lecture mit Gernot Heiser (UNSW Sydney) | CASA @ RUB
Das Thema ist "It´s time for truly secure operating systems".
casa.rub.de
May 22, 2025 at 11:11 PM
The recording of my CASA/MPI-SP Distinguished Lecture is now available – thanks for hosting me!
casa.rub.de/veranstaltun...
casa.rub.de/veranstaltun...
Very pleased that UNSW is sponsoring this year’s #seL4 Summit again: sel4.systems/news/#sponso...
seL4 News | seL4
sel4.systems
May 21, 2025 at 12:29 AM
Very pleased that UNSW is sponsoring this year’s #seL4 Summit again: sel4.systems/news/#sponso...
Got an invite for “Blockchain-Powered Machine Learning”. Certainly highly buzzword compliant, although I’m disappointed they couldn’t fit in quantum computing…
May 14, 2025 at 11:47 AM
Got an invite for “Blockchain-Powered Machine Learning”. Certainly highly buzzword compliant, although I’m disappointed they couldn’t fit in quantum computing…
Looking forward to giving this CASA Distinguished Lecture this Tuesday: "It´s time for truly secure operating systems”.
hgi.rub.de/news/newsarc...
hgi.rub.de/news/newsarc...
CASA Distinguished Lecture mit Gernot Heiser (USNW Sydney)
Das Thema ist "It´s time for truly secure operating systems".
hgi.rub.de
May 9, 2025 at 2:16 PM
Looking forward to giving this CASA Distinguished Lecture this Tuesday: "It´s time for truly secure operating systems”.
hgi.rub.de/news/newsarc...
hgi.rub.de/news/newsarc...
Great to see Collins Aerospace sponsoring the #seL4 Summit again: sel4.systems/news/#summit...
seL4 News | seL4
sel4.systems
May 5, 2025 at 12:05 AM
Great to see Collins Aerospace sponsoring the #seL4 Summit again: sel4.systems/news/#summit...
Benchmarking Crimes Meet Formal Verification
There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.
There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.
Benchmarking Crimes Meet Formal Verification
There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.
microkerneldude.org
April 27, 2025 at 1:06 AM
Benchmarking Crimes Meet Formal Verification
There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.
There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.
Why can’t my Mac share a wifi connection as a wifi hotspot, when my Samsung phone has no problem doing this?
April 7, 2025 at 4:31 PM
Why can’t my Mac share a wifi connection as a wifi hotspot, when my Samsung phone has no problem doing this?