Proof Auditing Formalised Mathematics (2016). This maps out the philosophy for auditing formalised mathematics projects, using the Flyspeck project for illustration.
The Common HOL Platform (2015). This gives an overview of the API and theory components of the Common HOL Platform, and explains how to go about implementing the platform for a given HOL system.
HOL Zero's Solutions for Pollack-Inconsistency (2016). This covers some classic weaknesses in the parsers and pretty printers of theorem provers, and shows how HOL Zero manages to overcome them.
Refactoring Proofs with Tactician (2015). This gives an overview of Tactician's capabilities, and explains how it manages to capture and refactor proofs.