Formal Verification of the Safegcd Implementation
Abstract
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 the extended Euclidean algorithm has been developed by Bernstein and Yang within the last few years and incorporated into the libsecp256k1 cryptographic library used by Bitcoin. However, novel algorithms introduce new risks of errors. To address this we have completed a computer verified proof of the correctness of (one of) libsecp256k1's modular inverse implementations with the Coq proof assistant using the Verifiable C's implementation of separation logic.
Cite
@article{arxiv.2507.17956,
title = {Formal Verification of the Safegcd Implementation},
author = {Russell O'Connor and Andrew Poelstra},
journal= {arXiv preprint arXiv:2507.17956},
year = {2025}
}
Comments
15 pages; Coq sources can be found at https://github.com/BlockstreamResearch/simplicity/tree/c1dddedd553b403da877377e658f17f0d2184cc4/Coq/C/secp256k1 ; Alectryon preview can be viewed at e.g. https://html-preview.github.io/?url=https://github.com/BlockstreamResearch/simplicity/blob/c1dddedd553b403da877377e658f17f0d2184cc4/alectryon/verif_modinv64_impl.v.html