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

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

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

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

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…

Looking forward to giving this CASA Distinguished Lecture this Tuesday: "It´s time for truly secure operating systems”. hgi.rub.de/news/newsarc...

RIP Usenix ATC – I’ve got many fond memories of you www.usenix.org/blog/usenix-...

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.

Why can’t my Mac share a wifi connection as a wifi hotspot, when my Samsung phone has no problem doing this?

Giving a joint keynote at ASPLOS+EuroSys was an honour but also 😁 After all, I was talking about LionsOS

LionsOS v0.3.0 is released! github.com/au-ts/lionso... This is on the back of sDDF (#seL4 driver framework) 0.6.0 and Microkit 2.0.1

The seL4 whitepaper is trending on HN: news.ycombinator.com/item?id=4345...

Time for the Coalition to end the nuclear (con)fusion. (3/3)

Mr O’Brien further walked back from nuclear in parliament: “No-one on the side of the House, including me, is suggesting that nuclear technology—even small nuclear reactors—is an absolute certainty for this country” (Hansard) tedobrien.com.au/nuclear-ener... (2/3)

Nuclear is being promoted as the ‘bold’ centrepiece of the Coalition’s climate and energy platform, but in recent weeks we’ve seen Ted O’Brien confirm it’s little more than an idea: “the nuclear technology for Australia is yet to be selected” perindavey.com.au/answer-your-... (1/3)

A coalition of tech companies and telcos has proposed industry codes to keep Australian kids safe from online porn and harmful content. Facial age estimation tech has a mean error of 3.7 years, yet the codes still deem it an "appropriate" age assurance measure. theconversation.com/tech-compani...

Thanks Alex Mason for posting this interesting article on LinkedIn: randomaugustine.medium.com/on-apple-exc... While not all seems to be correct, it contains a lot of stuff I didn’t know, thanks Random Augustine for the in-depth analysis!

Hello Bluesky! I stopped using Twitter (@GernotHeiser) in Dec’22 when it started to go feral. I tried Mastodon (@[email protected]), but that never took off. So I’m here now.