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.
2022-11-17 – Congratulations to Zilin Chen and co-authors, including fellow TS member Craig McLaughlin , for having their paper accepted at POPL , the prestigious annual symposium on Principles of Programming Languages, in Boston USA in 2023. This paper forms part of ...
2022-10-25 – Trustworthy Systems had a strong presence at the UNSW Computing Research Expo on October 25th 2022. Designed to showcase the research projects of the School of Computer Science and Engineering, TS was represented by Gernot Heiser , Zoltan Kocsis and Peter Chubb. Gernot Heiser gave a speech on secure a...
2022-10-07 – TS is pleased to announce a pre-release of the seL4 Device Driver Framework (sDDF) for community feedback. We provide an initial design document, code and an official seL4 community request for comment (RFC), for details see the sDDF projects page . TS student Lucy Parker ...
