Right. So maybe we can try to think about how to break bitcoin up into modular parts (eg. secp256k1, vm/script, encoding/decoding, merkle tree, create/verify block header, add block to tree, etc.). Then we can start with verifying the parts, and with verified parts you are much more likely to have a valid whole. Maybe at that point we can all band together and build an asic for it, then all run the asic instead of building software on the myriad OS's (which practically precludes the possibility of formal verification, as you've noted). Then maybe we'll have a safe bitcoin?! It's extreme but I'll entertain it.