Running the manual: an approach to high-assurance microkernel development. - Philip Derrin; Kevin Elphinstone; Gerwin Klein; David A. Cock; Manuel M. T. Chakravarty (Haskell, 2006)

Towards a Practical, Verified Kernel. - Kevin Elphinstone; Gerwin Klein; Philip Derrin; Timothy Roscoe; Gernot Heiser (HotOS, 2007)

Kernel design for isolation and assurance of physical memory. - Dhammika Elkaduwe; Philip Derrin; Kevin Elphinstone (IIES@EuroSys, 2008)

Experience report: seL4: formally verifying a high-performance microkernel. - Gerwin Klein; Philip Derrin; Kevin Elphinstone (ICFP, 2009)

seL4: formal verification of an OS kernel. - Gerwin Klein; Kevin Elphinstone; Gernot Heiser; June Andronick; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (SOSP, 2009)

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)