Secure Microkernels, State Monads and Scalable Refinement. - David A. Cock; Gerwin Klein; Thomas Sewell (TPHOLs, 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)

Mind the Gap. - Simon Winwood; Gerwin Klein; Thomas Sewell; June Andronick; David A. Cock; Michael Norrish (TPHOLs, 2009)

Refinement in the Formal Verification of the seL4 Microkernel. - Gerwin Klein; Thomas Sewell; Simon Winwood (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

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)

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. - Sascha Böhme; Anthony C. J. Fox; Thomas Sewell; Tjark Weber (CPP, 2011)

Provable Security: How Feasible Is It? - Gerwin Klein; Toby C. Murray; Peter Gammie; Thomas Sewell; Simon Winwood (HotOS, 2011)

seL4 Enforces Integrity. - Thomas Sewell; Simon Winwood; Peter Gammie; Toby C. Murray; June Andronick; Gerwin Klein (ITP, 2011)

Formally Verified System Initialisation. - Andrew Boyton; June Andronick; Callum Bannister; Matthew Fernandez; Xin Gao; David Greenaway; Gerwin Klein; Corey Lewis; Thomas Sewell (ICFEM, 2013)

Translation validation for a verified OS kernel. - Thomas Arthur Leck Sewell; Magnus O. Myreen; Gerwin Klein (PLDI, 2013)

Formal Replay of Translation Validation for Highly Optimised C. - Thomas Sewell (VPT@CAV, 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)

CoGENT: Verifying High-Assurance File System Implementations. - Sidney Amani; Alex Hixon; Zilin Chen; Christine Rizkallah; Peter Chubb; Liam O'Connor; Joel Beeren; Yutaka Nagashima; Japheth Lim; Thomas Sewell; Joseph Tuong; Gabriele Keller; et al. (ASPLOS, 2016)

Refinement through restraint: bringing down the cost of verification. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Sidney Amani; Japheth Lim; Toby C. Murray; Yutaka Nagashima; Thomas Sewell; Gerwin Klein (ICFP, 2016)

A Framework for the Automatic Formal Verification of Refinement from Cogent to C. - Christine Rizkallah; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Zilin Chen; Liam O'Connor; Toby C. Murray; Gabriele Keller; Gerwin Klein (ITP, 2016)

Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis. - Thomas Sewell; Felix Kam; Gernot Heiser (RTAS, 2016)

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)

COGENT: Certified Compilation for a Functional Systems Language. - Liam O'Connor; Christine Rizkallah; Zilin Chen; Sidney Amani; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Alex Hixon; Gabriele Keller; Toby C. Murray; Gerwin Klein (CoRR, 2016)

High-assurance timing analysis for a high-assurance real-time operating system. - Thomas Sewell; Felix Kam; Gernot Heiser (Real Time Syst., 2017)

Translation validation for verified, efficient and timely operating systems. - Thomas Sewell (2017)

MARDy: Mycology Antifungal Resistance Database. - Anthony Nash; Thomas Sewell; Rhys A. Farrer; Alireza Abdolrasouli; Jennifer M. G. Shelton; Matthew C. Fisher; Johanna Rhodes (Bioinform., 2018)

Proof pearl: Braun trees. - Tobias Nipkow; Thomas Sewell (CPP, 2020)

Cogent: uniqueness types and certifying compilation. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Vincent Jackson; Sidney Amani; Gerwin Klein; Toby Murray; Thomas Sewell; Gabriele Keller (J. Funct. Program., 2021)

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. - Thomas Bauereiss; Brian Campbell 001; Thomas Sewell; Alasdair Armstrong; Lawrence Esswood; Ian Stark; Graeme Barnes; Robert N. M. Watson; Peter Sewell (ESOP, 2022)

Candle: A Verified Implementation of HOL Light. - Oskar Abrahamsson; Magnus O. Myreen; Ramana Kumar; Thomas Sewell (ITP, 2022)

Cakes That Bake Cakes: Dynamic Computation in CakeML. - Thomas Sewell; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar; Alexander Mihajlovic; Oskar Abrahamsson; Scott Owens (Proc. ACM Program. Lang., 2023)

CN: Verifying Systems C Code with Separation-Logic Refinement Types. - Christopher Pulte; Dhruv C. Makwana; Thomas Sewell; Kayvan Memarian; Peter Sewell; Neel Krishnaswami (Proc. ACM Program. Lang., 2023)

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)

Verifying Device Drivers with Pancake. - Junming Zhao; Alessandro Legnani; Tiana J. Tsang Ung; H. Truong; Tsun Wang Sau; Miki Tanaka; Johannes Åman Pohjola; Thomas Sewell; Robert Sison; Syeda Hira; Magnus Myreen; Michael Norrish; et al. (CoRR, 2025)