> I recognize that there is probably no objective way to deductively prove it because of the Halting Problem etc.

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 and completely deduce properties or their violations for arbitrary programs. If your goal is simply to prove security and correctness properties for well-understood classes of programs in industry, then there are no fundamental obstructions.