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.
2021-08-22 – The seL4 Foundation has given interim endorsement to TS as a trusted provider for services around seL4 .
2021-07-28 – The assurance story for seL4 on RISC-V keeps building. We first formally proved functional correctness : that the seL4 C code on RISC-V platforms behaves exactly as its specification says . We then established binary correctness : that the machine code running on the processor behaves exac...
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-2015, TS became part of it, and was one of a small number of groups that defined Data61's international reputation. We attrac...