ABSTRACT. We report on a machine assisted verification of an efficient implementation of Montgomery Multiplication which is a widely used method in cryptography for efficient computation of modular exponentiation. We shortly describe the method, give a brief survey of the VeriFun system used for verification, verify a classical as well as a more recent algorithm for computing multiplicative inverses, illustrate proof-technical obstacles encountered upon verification, present the formal proofs and finally report on the effort when creating the proofs. Our work uncovered a serious fault in a state-of-the-art algorithm for computing multiplicative inverses based on Newton-Raphson iteration, thus providing further evidence for the benefit of computer-aided verification.