Welcome to Trustworthy Systems!
We are the Trustworthy Systems group. We use rigorous formal methods to develop trustworthy software systems—systems that come with provable security, safety and reliability guarantees.
We are 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 vision statement is:
We have made verified software a reality.
We’re now working on creating a societal shift towards mainstream adoption.
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 build robust 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.
Engagement
We apply our unique research and engineering experience to solve problems in the real world.
Additional resources
seL4
The world's most highly-assured operating system kernel.
Software
Our software and proof repositories, as well as packaged software releases.
For students
Info for prospective students and interns, and courses we teach.
Publications
Our research publications and tech reports.
Latest news
Alaska Center for Energy Power joins the Laot team
2021-10-27 – The Alaska Center for Energy and Power (ACEP) has joined the Laot project team . ACEP will conduct tests and demonstrations in their Fairbanks facility.
First release of the seL4 Core Platform
2021-10-22 – The seL4 Core Platform (seL4CP) has been proposed in an seL4 RFC . It was co-designed and -implemented with the Laot project and has now been publicly released for feedback and (eventual) TSC endorsement.
Gernot explains why seL4 is safe – and the role of TS
2021-09-28 – Following CSIRO's abandoning of TS and the seL4 technology TS developed, the seL4 community and the seL4 Foundation have grown a lot. This has led to concerns that the broader participation might have the potential to undermine the integrity of seL4. In his latest blog, Gernot explains why there is no reason for such conce...