Been following the development of Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan...
Looks interesting, perhaps because it seems to be a bit more down to earth than some of the other proposals where you have to derive Whitehead&Russell before you're allowed to use the + operator. But it also seems quite dead. The latest link is from 2012.
It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny
I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I learned in college rather than the weird magic keywords of Coq.