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.
Breakthroughs that combine our expertise in operating systems, formal methods and programming languages.
We apply our unique research and engineering experience to solve problems in the real world.
2023-1-27 – Trustworthy Systems Group participated in the Southern Summer School on Systems and Software Security. It was run at the University of Adelaide by Yuval Yarom (University of Adelaide) and Chitchanok Chuengsatiansup (University of Melbourne) from January 23 to 25 2023...
2022-12-12 – UNSW Sydney has celebrated the seL4 summit in a recent news item . The summit, held in Munich on October 10 -13 2022, was the first held outside the USA and by the seL4 Foundation . The report notes that, “A number of independent obser...
2022-12-12 – Congratulations to Zilin Chen for winning the Distinguished Artifact Award at the 2022 ACM SIGPLAN International Conference on Software Language Engineering. Chen and co-authors, including TS’s Gernot Heiser’s and TS affiliate Gerwin Klein , won the a...
