Dense Sphere Packings: a blueprint for formal proofs, Cambridge
University Press, LMS volume 400, 2012. This book contains the
second-generation proof of the Kepler conjecture that was used as
the blueprint for the formal proof of the Kepler conjecture.

The Kepler Conjecture: the Hales-Ferguson Proof (with S. Ferguson, edited by J. Lagarias), Springer, 2011. This is a reprint in book form of the series of articles by Ferguson and Hales on the Kepler conjecture, with supplementary articles by Lagarias. The separate articles are available at [arXiv-link].

The Subregular germ of orbital integrals Mem. AMS 99, 1992, no. 476. Hales’s 1986 PhD thesis on calculations of some Shalika germs of p-adic orbital integrals using Igusa theory.