What you'd need is almost dynamic live proof checkers hooked to your IDE capable of tracking the effects of code changes / refactoring to do that, linked to tes

What you'd need is almost dynamic live proof checkers hooked to your IDE capable of tracking the effects of code changes / refactoring to do that, linked to test cases themselves carrying proofs of testing the spec completely. How else will you be guaranteed to catch Goto Fail and similar? What's worse is when you hit the issue of "composability" in cryptography - two servers run different algorithms making different assumptions, and when they interact the assumptions fail to translate and neither provide the guarantee they should. Like cross-protocol attacks, such as when one server becomes a signing oracle for another. Edit: and beyond that, we have cross architecture disagreement on results of calculations intended to be deterministic. Like how SPARC Bitcoin Qt binaries previously would have had the Bitcoin reward schedule loop every 255 years and go back to 50 coins per block and restarting the countdown.