I am currently involved with the following projects.

The Trustworthy COTS Hardware is examining how to improve the trustworthiness of a verified kernel running on potentially unreliable commercial off-the-shelf hardware.

The seL4 (secure embedded L4) project's goal is to provide a reliable and secure microkernel-based platform for future embedded systems. Embedded systems are becoming increasingly complex - microkernels are an approach to reliably and securing integrating software components in embedded systems. The main challenges involve researching a principled and systematic in-kernel resource management approach, and developing the new microkernel in a way that is readily amenable to formal verification.

I am also involved with the L4.verified project. The project aims to formally verify both a model and the complete implementation of the seL4 microkernel.