Honestly, it seems floating point computations are, by some measure, possibly pretty old at this point in the formal methods world! Intel has been investing in

Honestly, it seems floating point computations are, by some measure, possibly pretty old at this point in the formal methods world! Intel has been investing in formal verification of its floating point units since at least the 90s when FDIV hit them, and this was when the tech was way worse than what we have today! Hell, CompCert -- which you can download today -- already has a proven adherence to IEEE-754 floating point, implemented by specifying IEEE-754 semantics in Coq, then using that to create a proof the compiler correctly preserves the semantics of IEEE-754 during the compilation process.