With those, all you have done is written the program twice. Once in the language and once in the formal verification.
(Almost) all of the mistakes it is possible to make while programming are possible to duplicate in the formal methods.
So if you have a security flaw where you have forgotten to specify that Method A must not be called before passing Security Check A, or if the specification does not spell out that calling Method B invalidates the current security state. That flaw will exist no matter how thorough the formal methods are.