points by joubert 6 years ago

Yes. Latest language standard is Ada 2012.

Spark, a subset of Ada 2012 supports formal proofs of program properties ranging from absence of run-time errors to functional correctness (compliance of the code with formally specified requirements).

If you're curious, you can learn more at https://learn.adacore.com/courses/courses.html