GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3).
Runtime checks are compiler implementation issue rather than language issue itself. With static analysis compiler could eliminate redundant runtime checks.
For example, if SPARK (Ada subset) is used and absense of runtime errors can be proved by GNATprove, then runtime check generation can be disabled in Ada compiler.
GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3).
https://github.com/AdaCore/spark2014