The Gappa tool helps developers to verify arithmetic properties on their numerical programs (either floating-point or fixed-point computations). It can also generate formal proofs of the properties for extra confidence. It has been successfully used with several projects, e.g. for writing some robust floating-point filters of CGAL and for certifying the elementary functions of CRlibm.
These details are provided for information only. No information here is legal advice and should not be used as such.