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
New #seL4 (16.0.0) released! A matching Microkit release (2.3.0) is out as well: sel4.systems/news/#07-22
seL4 News | seL4
sel4.systems
The program of the #seL4 Summit in Vancouver, 1–3 Sep, is out: sel4.systems/Summit/2026/...
seL4 Summit 2026 Program | seL4
sel4.systems
It finally happened – the MCS variant of #seL4 is verified (on RISC-V)! Proofcraft has just finished the functional correctness proof of this most powerful version of the kernel, specifically aimed at supporting mixed-criticality real-time systems. sel4.systems/news/#mcs26
seL4 News | seL4
sel4.systems
UNSW Sydney is #hiring systems faculty – talk to me if you’re interested. This is for mid-career researchers in the AU Lecturer–Senior Lecturer–Associate Professor–Professor progression. Tenure is orthogonal to position level – closes 31 July. external-careers.jobs.unsw.edu.au/cw/en/job/54...
Associate Professor in Systems
Join an organisation that is shaping the future direction of modern computing systems in Australia, in a senior academic role that combines research leadership, strategic contribution, and excellence ...
external-careers.jobs.unsw.edu.au
UNSW Sydney is #hiring systems faculty – talk to me if you’re interested. This is for early-career researchers in the AU Lecturer–Senior Lecturer–Associate Professor–Professor progression. Tenure is orthogonal to position level – closes 31 July. external-careers.jobs.unsw.edu.au/cw/en/job/54...
Lecturer/Senior Lecturer in Systems
Join an organisation that is shaping the future direction of modern computing systems in Australia, in an academic role that combines high-quality research, excellent teaching, and meaningful contribu...
external-careers.jobs.unsw.edu.au
Welcome Gapfruit, latest member of the #seL4 Foundation! sel4.discourse.group/t/gapfruit-j...
Gapfruit joins the seL4 Foundation
We are pleased to welcome a new member - Gapfruit - to the seL4 Foundation. Gapfruit is a Swiss technology company building trustworthy foundations for the systems society depends on - from industria...
sel4.discourse.group
Thursday was UNSW CSE Prizes Night. Several Trustworthy Systems students featured: 2nd year Sam Tyler (left) won two. New Heroes of Operating Systems are (from right) Varun Sethu and Richard Shen: high distinctions in OS, Advanced OS and OS thesis
Sad to hear that Peter G Neumann has passed away, aged 93. He was a pioneer of computer security, back from the PSOS system to much more recently being one of the people behind CHERI capabilities. Very insightful, and a nice guy besides. He’ll be missed. www.linkedin.com/feed/update/...
Peter G. Neumann, a pioneering computer scientist whose life work defined the field of computing risk, has died aged 93. Joining SRI in 1971 and having still worked under our Computer Science Lab… |...
Peter G. Neumann, a pioneering computer scientist whose life work defined the field of computing risk, has died aged 93. Joining SRI in 1971 and having still worked under our Computer Science Lab be...
linkedin.com
Today I had the great honour to receive the Outstanding Technical Achievement and Leadership Award of the IEEE Technical Committee on Real-Time Systems (TCRTS). www.linkedin.com/company/tech...
TCRTS - Technical Committee on Real-Time Systems | LinkedIn
TCRTS - Technical Committee on Real-Time Systems | 391 followers on LinkedIn. The Technical Committee on Real-Time Systems (TCRTS) of the IEEE CS addresses real-time issues in systems design. | The T...
linkedin.com
If you’re looking for an approachable overview of seL4 etc, you might be interested in this one: trustworthy.systems/publications...
TS | seL4: Operating systems with the reliability of mathematics
trustworthy.systems
Proofcraft is a Silver Spo0nsor of the #seL4 Summit – thank you Proofcraft! sel4.discourse.group/t/thank-you-...
Thank you Proofcraft, silver sponsor of the seL4 Summit 2026
The seL4 Foundation thanks Proofcraft, silver sponsor of the seL4 Summit 2026. Founded by the seL4 verification leaders, Proofcraft offers commercial support and projects in formal verification in ge...
sel4.discourse.group
Riverside Research is sponsoring the #seL4 Summit – thank you, Riverside! sel4.discourse.group/t/thank-you-...
Thank you Riverside Research, sponsor of the seL4 Summit 2026 reception
The seL4 Foundation thanks Riverside Research for sponsoring the seL4 Summit 2026 reception. Riverside Research is a national security nonprofit serving the DOD and Intelligence Community. Through th...
sel4.discourse.group
Seems when the AI can’t bullshit its way through, it doesn’t do so well. Who would have thought? fiducia-lang.github.io/blog/claude-...
Claude vs Student: Rocq Proof Development - Fiducia Blog
$3,000 in API costs, four failed attempts at a Rocq proof, and a student who solved it in two days. Lessons on LLMs and formal verification.
fiducia-lang.github.io
#seL4 release 15.0.0 is out! Together with accompanying releases of Microkit, CAmkES, CapDL and rust-sel4. sel4.systems/news/#03-31
seL4 News | seL4
sel4.systems
Microkernels are very much at the centre of this year’s John Lions Distinguished Lecture: Hermann Härtig, Father of L4Re and NOVA (among others) will talk about “Taming the Elephant in the Basement: From L4 to M3” www.eventbrite.com.au/e/john-lions...
John Lions Distinguished Lecture
You're invited to attend this talk by Emeritus Prof. Hermann Härtig, Technische Universität Dresden, Computer Science Department.
eventbrite.com.au
The #seL4 Summit will also feature Voices from Nearby. Alistair Woodmand, Board Member of the Erlang Ecosystem Foundation, on the European Cyber Resiliency Act. David Hardin, Associate Director of Systems Engineering at Collins Aerospace, on real-world formal verification. sel4.systems/news/#03-18
seL4 News | seL4
sel4.systems
This year’s #seL4 Summit in Vancouver will have two great keynotes, Anjana Rajan, Former Assistant National Cyber Director at The White House, and Martin Dehnel-Wild, Chief Scientist at Kry10. sel4.systems/news/#03-18
seL4 News | seL4
sel4.systems
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/...
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...
linkedin.com
Registration is open for this year’s #seL4 Summit in Vancouver, 1–3 September: sel4.discourse.group/t/registrati...
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...
sel4.discourse.group
First publicised use of the #seL4-based #LionsOS in a commercial product: www.linkedin.com/feed/update/...
#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...
linkedin.com
Welcome Fraunhofer AISEC to the #seL4 Foundation! sel4.systems/news/#01-28
seL4 News | seL4
sel4.systems
The Call for Presentations for the #seL4 Summit is out! sel4.systems/news/#01-23
seL4 News | seL4
sel4.systems
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...
Research Associate/Senior Research Associate (Formal Methods)
Conduct research in the area of formal methods and systems independently and as part of the team.
external-careers.jobs.unsw.edu.au
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...
trustworthy.systems