The advent of formally verified OS kernels means that for the first time the authors have a truly trustworthy foundation for systems. In this paper, they explore the design space this opens up. The obvious applications are in security, although not all of them are quite as obvious, for example as they relate to TPMs. They further find that the kernel's dependability guarantees can be used to improve performance, for example in database systems. They think that this just scratches the surface, and that trustworthy kernels will stimulate further research.