Formal methods have their place.<p>I think we do need more waterfall-type design and documentation of cryptosystems (not massive pointless documentation, but relevant documentation and security&#x2F;engineering tradeoffs design justifications.)<p>Also, for more and better eyeballs to audit code, it needs to be simple and clear code.<p>More thorough C unit&#x2F;system testing, fuzzing and static&#x2F;dynamic analysis steps as standard would help... I think a project&#x2F;startup which could be like a TravisCI for the security and correctness of C code would work because there&#x27;s just so much C code which needs better coverage.