Also a formal specification can have bugs. Formal verification checks that the code matches the spec, not that the spec implements all desired behaviors and no undesired behaviors.
You're right, though it's worth noting that you can also use formal verification to verify properties about the specification! For example you can verify that a security system doesn't allow privilege escalation.
Yep, though of course it's still on you to remember to verify everything you care about. Actually writing out all your requirements in a formal (or just programming) language is the hard part of programming.
