Gordon led the development of the HOL theorem prover.[2] He was elected a Fellow of the Royal Society in 1994, and in 2008 a two-day research meeting on Tools and Techniques for Verification of System Infrastructure was held there in honour of his 60th birthday.[3]