Even if you write a formal specification the operating system the code runs on is almost certainly not formally specified so you're just moving the trust boundary slightly further out to the OS & associated libraries.
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!