Formalising the L4 microkernel API. - Rafal Kolanski; Gerwin Klein (CATS, 2006)

Mapped Separation Logic. - Rafal Kolanski; Gerwin Klein (VSTTE, 2008)

A Logic for Virtual Memory. - Rafal Kolanski (SSV, 2008)

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)

Types, Maps and Separation Logic. - Rafal Kolanski; Gerwin Klein (TPHOLs, 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)

Verification of programs in virtual memory using separation logic. - Rafal Kolanski (2011)

Challenges and Experiences in Managing Large-Scale Proofs. - Timothy Bourke; Matthias Daum 001; Gerwin Klein; Rafal Kolanski (AISC/MKM/Calculemus, 2012)

Large-scale formal verification in practice: A process perspective. - June Andronick; D. Ross Jeffery; Gerwin Klein; Rafal Kolanski; Mark Staples; He Zhang 001; Liming Zhu 001 (ICSE, 2012)

Simulation modeling of a large-scale formal verification process. - He Zhang 001; Gerwin Klein; Mark Staples; June Andronick; Liming Zhu 001; Rafal Kolanski (ICSSP, 2012)

Mechanised Separation Algebra. - Gerwin Klein; Rafal Kolanski; Andrew Boyton (ITP, 2012)

Separation Algebra. - Gerwin Klein; Rafal Kolanski; Andrew Boyton (Arch. Formal Proofs, 2012)

Formal specifications better than function points for code sizing. - Mark Staples; Rafal Kolanski; Gerwin Klein; Corey Lewis; June Andronick; Toby C. Murray; D. Ross Jeffery; Len Bass (ICSE, 2013)

Productivity for proof engineering. - Mark Staples; D. Ross Jeffery; June Andronick; Toby C. Murray; Gerwin Klein; Rafal Kolanski (ESEM, 2014)

Comprehensive formal verification of an OS microkernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Toby C. Murray; Thomas Sewell; Rafal Kolanski; Gernot Heiser (ACM Trans. Comput. Syst., 2014)

Finite Machine Word Library. - Joel Beeren; Matthew Fernandez; Xin Gao; Gerwin Klein; Rafal Kolanski; Japheth Lim; Corey Lewis; Daniel Matichuk; Thomas Sewell (Arch. Formal Proofs, 2016)

AutoCorres2. - Matthew Brecknell; David Greenaway; Johannes Hölzl; Fabian Immler; Gerwin Klein; Rafal Kolanski; Japheth Lim; Michael Norrish; Norbert Schirmer; Salomon Sickert; Thomas Sewell; Harvey Tuch; et al. (Arch. Formal Proofs, 2024)