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-11-17 – Four TS undergraduate students, together with Gernot Heiser , attended the Symposium on Operating Systems Principles (SOSP) in Koblenz, Germany. Honours students Lucy Parker and Alwin Joshy , and 3rd-year students Mathieu Paturel and Krishnan Winter , had all won travel scholarship...
2023-10-31 – Trustworthy Systems has just released the seL4 Microkit . The seL4 Microkit, formerly known as the Core Platform, is an operating system framework on top of seL4 which provides a small set of simple abstractions that ease the design and implementation of statically structured systems on seL4, while stil...
2023-10-23 – TS members Ivan Velickovic, Lucy Parker, and Gernot Heiser participated in the seL4 Summit in Minneapolis. Lucy Parker presented the latest developments on the seL4 device driver framework, discussing the design of the networking system, and showed off its awesome performance. ...
