> 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.
Formal verification is not magic. It can execute deductive proofs, but the relevance and utility of those results is a question of human values. Spec bugs are a thing. Bad design is a thing. Out-of-scope usage is a thing. Even a halting oracle won't help with those.