Our Impact

Cyberattacks on critical systems are increasing, and their annual cost to the US alone is estimated to be in the billions to trillions. Attacks on autonomous cars, medical devices etc are putting lives at risk. Preventing such attacks is therefore essential, and hugely beneficial to society.

Formal proofs are the only mechanism that can categorically rule out flaws which enable such attacks, especially in operating systems, by proving that software is a correct implementation of its specification. At Trustworthy Systems we develop performance-focussed operating-system designs and implementation techniques that allow us to apply such proof techniques, to achieve provable security and safety of real-world computer systems.

We are the pioneers of the application of mathematical proof techniques to operating systems, with the verification of our seL4 microkernel, which has triggered world-wide research activities in this space. seL4 is already deployed in safety- and security-critical systems in defence, autonomous vehicles and critical infrastructure, with many more deployments in progress. This development is dramatically improving the safety and security of real-world embedded, cyberphysical and IoT systems, and is creating a pathway to securing general-purpose IT systems.

We have created a world-wide open-source ecosystem of developers and adopters of seL4 technology. To guide and grow this ecosystem we established the seL4 Foundation, which combines small and large companies, universities and government organisations. We receive direct funding from several of these organisations, and collaborate with others on the further development and deployment of the technology we created.