In addition to Dafny (https://github.com/Microsoft/dafny) and Whiley (http://whiley.org/), check out Frama-C (https://frama-c.com/) for C and SPARK (http://www.spark-2014.org/) for Ada.

Both are mature enough to be in use, but are limited primarily by the fact that both languages have manual memory management, which is well understood via separation logic, but poorly supported by the tools.

I've written some blog posts about Frama-C:

* https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search....

* https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch....

* https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic...

* https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort...