How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. - Raphaël Rieu-Helft; Claude Marché; Guillaume Melquiond (VSTTE, 2017)

A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. - Guillaume Melquiond; Raphaël Rieu-Helft (IJCAR, 2018)

Formal Verification of a State-of-the-Art Integer Square Root. - Guillaume Melquiond; Raphaël Rieu-Helft (ARITH, 2019)

A Why3 proof of GMP algorithms. - Raphaël Rieu-Helft (J. Formaliz. Reason., 2019)

Development and verification of arbitrary-precision integer arithmetic libraries. (Développement et vérification de bibliothèques d'arithmétique entière en précision arbitraire). - Raphaël Rieu-Helft (2020)

WhyMP, a formally verified arbitrary-precision integer library. - Guillaume Melquiond; Raphaël Rieu-Helft (J. Symb. Comput., 2023)

Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function. - Paul Bonnot; Benoît Boyer; Florian Faissole; Claude Marché; Raphaël Rieu-Helft (FMCAD, 2024)