Trustworthy Systems

Welcome to Trustworthy Systems!

(Most of) Trustworthy Systems in September 2024.

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

Research

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

seL4 call graph

Engagement

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

helicopter

Additional resources

seL4

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

seL4 logo

Software

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

gears

For students

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

whiteboard

Publications

Our research publications and tech reports.

bookshelf

Latest news

2024-10-28 – The seL4 Foundation , chaired by Scientia Prof Gernot Heiser , ran the 6th seL4 Summit on 15–17 October. It was the first time the Summit was held in Australia, where seL4 was created. This was fitting, as it coincided with multiple “round” anniversaries: 20 years since the seL4 project started at...

2024-10-15 – As of today, the seL4 web site runs on LionsOS!

2024-08-28 – The DARPA Pipeline Reasoning of Verifiers Enabling Robust Systems (PROVERS) Program is funding the project Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA) . TS is a member of the project team that is led by our long-standing collaborators Collins Aerospace. Other members...