Comment by measurablefunc

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.