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.