R. Rieu-Helft, “A Why3 proof of GMP algorithms”, JFR, vol. 12, no. 1, pp. 53–97, Jan. 2019.