Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. - Magnus O. Myreen; Gregorio Curello (CPP, 2013)