In real conditions, static analysis and theorem proving can verify lots of safety properties. See e.g. Astrée & Airbus, or F* and Project Everest.
IMHO, the solution is to use static analysis in conjunction with DSLs that have restricted semantics to make static analysis and hand-written proofs easy.
You're referring to verifying 'lots' of safety properties, I referred to verifying that an algorithm does everything it's supposed to. These are not the same thing in the general case.
My actual point was that generic incompleteness and undecidability theorems do not guarantee that any given program must be defective.
The thrust of langsec is in fact to parse all inputs at the boundaries, using algorithms with known properties, that is, ones where it's feasible to prove that they'll halt, won't overrun buffers, and so on.
I hope readers will be able to look past this one sentence in your post and take a good hard look at the rest of it, which is quite important.