Blog of Gernot Heiser, one of the developers of the seL4 verified microkernel.

We use rigorous formal methods to develop trustworthy software systems—systems that come with provable security, safety and reliability guarantees.