In addition to the points flavio81 made, checking at runtime because unless the language is dependently typed i.e. has types as first class citizens(for example

In addition to the points flavio81 made, checking at runtime because unless the language is dependently typed i.e. has types as first class citizens(for example Idris) a lot of the information about your code you want to prove to be correct is not available at compile time(for example, you have an integer but is it a non-negative integer, a list but is it sorted). It is not about being reliable, it is about being possible.