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
... [More] robust floating-point filters of CGAL and for certifying the elementary functions of CRlibm. [Less]
Remake is a build system that provides a Make-compatible rule-based syntax while supporting dynamic dependencies à la Redo. Its code is portable yet fits into a single file, so as to be easily shippable with any project.
Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.