Trustworthy Systems Group: secure and performant real-world computer systems

We are the Trustworthy Systems Group

We research techniques for the design, implementation and verification of secure and performant real-world computer systems.

• We aim to change the world by making software truly trustworthy.
• Having made verified software a reality, our goal is to create a societal shift  towards mainstream adoption.

We achieve impact by 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 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 show how to build robust, high-performance software stacks for the software development community, and also engage with other organisations to apply our technology to real problems.

Additional resources

Latest news

2025-11-13 – TS is proud to announce the release of a new proof-of-concept firewall system running on LionsOS. The firewall has a highly modular design, each module being a process running in its own address space. It uses components of both LionsOS and the seL4 device driver framework (sDDF) to demonstrate how to construct a Microkit-based…

2025-11-02 – The Trustworthy Systems (TS) group was strongly involved in the workshop day associated with this year’s ACM SIGOPS Symposium on Operating Systems Principles in Seoul, Korea. 

2025-09-25 – A highlight of every year is the seL4 summit. Run by the seL4 Foundation, it showcases the cutting edge of research on and work with seL4. This year the summit was in Prague, Czechia, and was attended by three in the TS team.