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
Additional resources
Latest news
The Trustworthy Systems Group is now back at UNSW
2021-07-21 – The Trustworthy Systems (TS) grew to world fame in NICTA , with the design, implementation and verification of seL4 its defining achievement. When NICTA was absorbed into CSIRO's Data61 in mid-20...
seL4 on RISC-V is verified to the binary
2021-05-05 – The seL4 Foundation and RISC-V International announced that the verified seL4 microkernel on the RV64 architecture has been proved down to the execu...
Gernot has been appointed as one of ACM’s Distinguished Speakers
2021-05-04 Professor Gernot Heiser has been appointed as one of ACM's Distinguished Speakers, "Renowned International Thought Leaders Speaking on the Most Important Topics in Computing Today"!
You can see the full list of speakers here .
Congratulations to Gernot for joining this illu...