There is a D subset:

https://dlang.org/articles/safed.html

But nothing like Ada SPARK provability stuff, I don't think.