Formal proof for delayed finite field arithmetic using floating point operators

Sylvie Boldo, Marc Daumas, Pascal Giorgi

Formal proof checkers such as Coq are capable of validating proofs of correction of algorithms for finite field arithmetics but they require extensive training from potential users…