Formal Verification of the Safegcd Implementation

Russell O'Connor, Andrew Poelstra

The modular inverse is an essential piece of computation required for elliptic curve operations used for digital signatures in Bitcoin and other applications. A novel approach to t…