Trustworthy Systems

Welcome to Trustworthy Systems!

(Most of) Trustworthy Systems in December 2021.

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 aim to change the world by making software truly trustworthy.
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


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

seL4 call graph


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


Additional resources


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

seL4 logo


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


For students

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



Our research publications and tech reports.


Latest news

2022-06-22 – The British government backs UNSW Sydney researchers to advance their world-leading cyber security technology, which protects critical computer systems from cyber attacks. The United Kingdom's National Cyber Security Centre (NCSC) will fund UNSW Engineering’s Tru...

2022-02-09 – UNSW has partnered with Secure Systems Research Center to implement ground-breaking cyber security technology. “This collaborative effort between UNSW and SSRC will aim to extend the formally verified seL4 microkernel to support tight integration o...

2021-12-02 – In July, we announced that the assurance story for seL4 on RISC-V keeps building, with the completion of the proof that seL4 enforces integrity , following the earlier proofs of functional correctness and binary correctness for seL4 on RISC-V. ...