1. The undecidability of most interesting properties of programs in Turing-complete languages is due to the fact that we cannot build a universal decider for said properties. The project discussed in the original post concerns a single program. This is crucial. We can (and did) prove a lot of interesting facts about individual programs without contradicting Goedel's incompleteness result.

2. Referring to NP-completeness is bound to mislead the uninitiated. Checking the correctness proofs is in P (ie the checker runs in time polynomial in the size of the proofs presented); creating the proofs is not known to be in NP (importantly: in the size of the claim to be proved).

Disclaimer: I'm involved in the seL4 verification project.