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-5-31 – We extend a very heartfelt farewell to Zoltan Kocsis, who is leaving Trustworthy Systems to pursue his real interests in pure mathematics. During his time with TS he initially worked on proving translation correctness of the seL4 kernel on the RISC-V architecture (thus t...
2023-5-5 – The Association for Computing Machinery (ACM) has awarded the prestigious ACM Software System Award to TS members Gernot Heiser and Kevin Elphinstone, and others. The ACM Software System Award recognises the development of a software system that has...
2023-4-19 – Gernot Heiser has been elected to the German National Academy of Science Leopoldina . Leopoldina is the oldest continuous scientific academy in the world, operating for over 360 years. Elections is based on strict standards of scientific excellence an...
