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:
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.
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.
The world's most highly-assured operating system kernel.
Our software and proof repositories, as well as packaged software releases.
Info for prospective students and interns, and courses we teach.
Our research publications and tech reports.
2121-11-29 – UNSW Sydney has signed a research agreement with Swiss technology company Neutrality to develop cyber network safeguards for organisations whose integrity and trust is essential in protecting people. “ This project aims at protecting communications of humanitarian and other non-government organisations from cyber-att...
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.
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.