That also assumes that your axioms are correct and the verification code is also correct. It's also a lot of work to update your system, when assumptions are challenged.
That the resulting code is many orders of magnitude larger and more complicated than the "informal" original, and often simply cannot exist, and is incomprehensible to most humans if it does, is left as an exercise for the reader.
I mean, formal methods cannot even prove collatz conjecture terminates. Somehow that thing seems to be running some sort of almost turing complete machine in the number encoding. Good luck formalizing existing software!