Ada is awesome.

Strong, expressive typing: types are not interchangeable, even if they share the same representation. Units, ranges, and semantics can be encoded directly in types.

Subtypes and range constraints allow you to constrain values at the type level, with violations being detected at compile time very often, dramatically reducing invalid state problems.

Design-by-contract is built into the language via pre-conditions, post-conditions, and invariants.

Its packages offer real modularity with implementation details strictly hidden unless explicitly exposed.

Has built-in concurrency model, rather than bolted-on libraries.

Unmatched in hard real-time systems via deterministic scheduling, priority inheritance, bounded execution time analysis, and precise control over memory layout.

Explicit handling of undefined behavior, making formal verification possible.

Which brings us to SPARK (Ada subset), which allows mathematic proof of correctness.

It is difficult to think of another production-grade formal verification ecosystem.