A Formal Model of IEEE Floating Point Arithmetic

Lei Yu 📧 with contributions from Fabian Hellauer 📧, Fabian Immler 🌐 and Tjark Weber 📧

July 27, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This development provides a formal model of IEEE-754 floating-point arithmetic. This formalization, including formal specification of the standard and proofs of important properties of floating-point arithmetic, forms the foundation for verifying programs with floating-point computation. There is also a code generation setup for floats so that we can execute programs using this formalization in functional programming languages.


BSD License


May 22, 2023
Added a model of floating-point arithmetic with a single NaN value.
Added a translation of floating-point arithmetic into SMT-LIB.
May 10, 2023
Added the IEEE rounding mode "roundNearestTiesToAway".
February 5, 2018
'Modernized' representation following the formalization in HOL4: former "float_format" and predicate "is_valid" is now encoded in a type "('e, 'f) float" where 'e and 'f encode the size of exponent and fraction.
September 25, 2017
Added conversions from and to software floating point numbers (by Fabian Hellauer and Fabian Immler).


Session IEEE_Floating_Point