Ada/SPARK formal numerics package.
Instructions for building a GNATprove with support for external axiomatization are in the gnatprove branch. Hopefully they should be obsoleted by the next release of the GNATprove.
The GNAT GPL 2013 compiler handles subrange predicates of
floating-point types incorrectly. Thus, there is no run-time check for
Positive_Float type and others. This has been already fixed by
AdaCore and those predicates will be added once a new compiler is
released.