Since end of July, a GPL release of GNATprove, the tools to make formal verification of Ada 2012 programs, is available.

One can now formally verify Ada programs using only Free Software! If you are interested, you can look at my previous attempt to verify a toy electronic booth program using GNATprove.