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.
I could be wrong, but I have the impression what you are looking for is how constexpr and consteval work in C++ https://en.cppreference.com/w/cpp/language/consteval
You can look into theorem proover (Coq, lean ...) and code extracted from them. A middle ground is FramaC+WP plugin for hoare logic for C.
Some languages like F* are also proof oriented.
In all its generality, the problem is undecidable. But there are quite a lot of tools that are meant to formally verify properties about programs. Proof assistants, of course, but there are also tools for more mainstream languages, like Frama-C, Ada/Spark, Java/KeY, Creusot (Rust), etc.