It _is_ possible to do some checks at compile time, but not for all programs. Or, you can check all programs, but only be _sure_ about your results on some of them. Or, you can add some constraints and force the programmer to write extra information so that you can make it work on more programs.

Overall, there's no free lunch: somewhere, someone will have to do some extra work.

Other useful invariants include some RAII idioms, Rust memory checks, resource usage (e.g. locks), etc.