Nothing can beat Ada when it comes to safety, and it has all the constructs in the language you want, and it has all the positives that you want. Heck, there is a reason for why Ada/SPARK is used for a lot of important projects, say, a cryptographic library.

In any case, Ada would be the perfect choice, IMO.