Physicist by training, computer engineer by passion.
Gernot Heiser FACM FIEEE FTSE FRSN ML is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney. He is also the founding Chairman of the seL4 Foundation.
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.
http://microkerneldude.org/2025/04/27/benchmarking-crimes-meet-formal-verification/
Hello Fedoverse,
I joined here when Twitter was going feral in late'22, hoping for a new home.
Unfortunately, this doesn't seem to have taken off, I don't remember when I last saw anything technical in @discuss.systems. Maybe I'm using it incorrectly, but whatever it is, it doesn't seem to work for me.
So I've set up on Bluesky and will be posting there from now on: https://bsky.app/profile/microkerneldude.bsky.social
@sel4 welcome Cyberagentur and thanks for your support!
German cybersecurity funding agency Cyberagentur joins the seL4 Foundation.
Announced that the launch of their ÖvIT program – ecosystem for verified IT – which funds two projects that advance seL4 and its ecosystem: One by Foundation members Kry10 and Proofcraft, the other (PISTIs-V) by Foundation member UNSW Sydney and parters.
https://sel4.systems/news/#member-cyberagentur
https://www.cyberagentur.de/presse/ein-meilenstein-fuer-it-sicherheit-in-deutschland/
A new version of application spam:
"Dear Professor Scientia Professor Gernot Heiser,
"I hope this email finds you well. My name is [Your Full Name], and I have recently completed my ...'
Presentation videos and slides from the seL4 #Summit are now available:
* videos on our YouTube channel: https://www.youtube.com/@seL4
* slides are linked from the Summit program: https://sel4.systems/Foundation/Summit/2024/program
"seL4 co-habitating the hardware" with untrustworthy firmware: Roman from ETH at the #seL4Summit about real-world hardware
Rob from Trustworthy Systems at the #seL4Summit talks about TS verification work aiming for whole system security
Incremental cyber retrofit at work: Nathan from DornerWorks talks at the #seL4Summit about running ROS on seL4
Clearly, more students need to take UNSW's Advanced Operating Systems course!
Ning Qu from Foundation Premium Member NIO talks at the ##seL4Summit about their seL4-based SkyOS, which has been shipping in their latest models since last month
Miki from Trustworthy Systems at the #seL4Summit presenting Pancake, our new systems language with verified compiler, which we're using to implement and verify LionsOS components
Courtney from Trustworthy Systems at the #seL4Summit talking about optimising the synchronisation messages between the asynchronous components of the seL4 device driver framework
Leigha VanderKlok from DornerWorks reports on experience with the Microkit VMM at the #seL4Summit - tl;dr mostly good, few more things to do
@carsickcans there's an implementation that is currently undergoing verification
Proud as a peacock watching TSer Ivan delivering his #LionsOS talk at the #seL4Summit from an Arm board running LionsOS
Enjoying the (almost sell-out) crowd at the #sel4Summit, where half the attendees are present odds former #TrustworthySystems people
This year the seL4 technology celebrates three anniversaries: start of the seL4 project (20y), first implementation correctness proof (15y), and open-sourcing (10y).
There will be a panel at the seL4 Summit on this occasion, featuring some of the main players – should be fun 😀
https://sel4.discourse.group/t/sel4-summit-2024-anniversary-panel-session/914
Welcome Lewis & Clark College, new Associate Member of the seL4 Foundation
https://sel4.systems/news/#member-lewis-clark
