Trustworthy Systems

Welcome to Trustworthy Systems!

(Most of) Trustworthy Systems in February 2023.

We are the Trustworthy Systems Group

We research techniques for the design, implementation and verification of secure and performant real-world computer systems.

We achieve impact by fundamentally changing how software systems are engineered in the real world. Our techniques provide the highest possible degree of assurance—the certainty of mathematical proof—while being cost-competitive with traditional low- to medium-assurance systems.

Our research brings together a unique combination of expertise in operating systems, formal methods and programming languages. Our seL4 microkernel is the most thoroughly verified operating system kernel in the world.

Our work goes beyond research. We show how to build robust, high-performance software stacks for the software development community, and also engage with other organisations to apply our technology to real problems.

Our main activities


Breakthroughs that combine our expertise in operating systems, formal methods and programming languages.

seL4 call graph


We apply our unique research and engineering experience to solve problems in the real world.


Additional resources


The world's most highly-assured operating system kernel.

seL4 logo


Our software and proof repositories, as well as packaged software releases.


For students

Info for prospective students and interns, and courses we teach.



Our research publications and tech reports.


Latest news

2023-3-22 – Trustworthy Systems team members Peter Chubb , Lucy Parker , Christopher Irving , and Ivan Velickovic presented their work on sel4 at the recent Everything Open conference in Melbourne. ...

2023-3-17 – Trustworthy Systems student Zilin Chen has just had his PhD thesis approved. We extend to him heartfelt and deserved congratulations. His thesis is Towards A Practical High-Assurance Systems Programming Language . It was supervised by Pro...

2023-3-15 – Robert Sison , a TS member and post-doctoral fellow from the University of Melbourne, works with TS team member Scott Buckley on Time Protection. He recently presented their work at the 25th International Symposium on Formal Methods at the University of Lübeck...