Ada does a mix of both compile-time and run-time checks. It was systematically designed to eliminate errors in most parts of the development process as the book below shows. SPARK, an Ada variant, can prove absence of all kinds of errors in code with automated provers. Since Ada supports cross-language programming, the typical route is to do most of the key logic in Ada, anything static/simple in SPARK, and anything platform-related in native language if too hard to do in Ada. They periodically update them with recent versions at 2012 for Ada and 2014 for SPARK.

http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Book...

Note: See table of contents especially.

http://cowlark.com/2014-04-27-ada/index.html

Note: This "random walk through Ada" has a nice summary of all kinds of features it has from perspective of an outsider instead of an Ada developer.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

http://www.adacore.com/uploads/technical-papers/SPARKSkein_S...

Note: Link to SPARK and an example by Rod Chapman on doing Skein in it. Just converting it from C to SPARK found an error in original code. Because of course it did haha...