Formal verification is not magic. It can execute deductive proofs, but the relevance and utility of those results is an 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.