There is. But it will only be reliable if every transitive dependency of your codebase, all the way down to the hardware level, has been formally verified. Failing that, you have to rely on opaque contracts at the boundaries, and those are just promises that may be mistaken.

The Halting problem, Rice's theorem, etc. only apply if your goal is to automatically deduce properties or their violations for arbitrary programs. If your goal is simply to prove correctness properties for well understood classes of programs in industry, then there are no fundamental obstructions.