Problem 69 "Greatest Common Divisor Algorithm" of 100 on this list now has a formalisation (pdf) and proof.