Islaris: verification of machine code against authoritative ISA semantics. - Michael Sammler; Angus Hammond; Rodolphe Lepigre; Brian Campbell 001; Jean Pichon-Pharabod; Derek Dreyer; Deepak Garg 001; Peter Sewell (PLDI, 2022)

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. - Angus Hammond; Zongyuan Liu 001; Thibaut Pérami; Peter Sewell; Lars Birkedal; Jean Pichon-Pharabod (Proc. ACM Program. Lang., 2024)

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture. - Angus Hammond; Ricardo Almeida 003; Thomas Bauereiss; Brian Campbell 001; Ian Stark; Peter Sewell (Proc. ACM Program. Lang., 2025)