Also take a look at Dafny, Why3/WhyML, and Ada/SPARK. Very pragmatic tools that are getting some industry adoption. Coq and Isabelle also see some use, but the

Also take a look at Dafny, Why3/WhyML, and Ada/SPARK. Very pragmatic tools that are getting some industry adoption. Coq and Isabelle also see some use, but they are more costly to use in my experience.