It's impractical by a huge margin. Why? Well, not only because bit flipping does occur naturally due to radiation but also because there's no such thing as a f

It's impractical by a huge margin. Why? Well, not only because bit flipping does occur naturally due to radiation but also because there's no such thing as a formally proven hardware stack in the world. At the end of the day your software has to run on hardware that exists. Not only has that hardware not been formally proven, you can't even know exactly how the hardware will behave from one month to the next due to firmware patches (spectre/meltdown mitigations, for example). Those patches can affect behavior and performance by huge amounts. Additionally, formal proofs don't cover one of the biggest classes of bugs: insufficient specifications. If you formally prove your software to the wrong specification then you still end up with buggy software. So even with provably correct software methodology you still need classical QA processes. Moreover, it is not necessary to have formally correct algorithms and state machines in order to achieve the maximum quality of software.