Most issues (apart from legacy asymmetric primitives) are actually either in the implementation (common in widely deployed software) or the design (even more common in widely deployed software) of higher level protocols. Many implementations issues in crypto code are just regular code bugs. Meanwhile, design issues are not so readily apparent.

There is no linter that will tell you that using the same AES key for years and keeping a block counter in an untrusted location is a bad idea. And if you make your code obscure enough ("abstract" in all the wrong ways), then people will have a really hard time figuring stuff like this out.

And no one does proofs on protocol implementations in practice. Yes, there are some. Yes, there has been some progress to apply it to e.g. OpenSSL — after everyone has been using it for critical infrastructure for decades — so there's like, literally, one practical implementation that has seen a sliver of formal verification.

There's tooling like Cryptol and SPARK to make this a lot easier than it was in the past. Cryptol can generate software or hardware that implements the high-level spec of the algorithm. Far as practical use, certainly not just one even though still extremely rare. Here's some more:

Altran/Praxis Correct-by-Construction for a cert authority

http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct...

Same company ports Skein from C to SPARK, finds trouble

http://www.skein-hash.info/sites/default/files/SPARKSkein.pd...

SPARK Ada is available under GPL and commercial licenses. The book below is quite easy to read compared to most stuff with formal methods. The companies building stuff like this usually also have tools to generate tests (property-based testing) from contracts/specs and can automatically turn anything you can't prove into runtime checks. Shocked it's not used more often in areas like smart contracts or cryptocurrency protocols.

https://www.amazon.com/Building-High-Integrity-Applications-...

Galois built Cryptol for NSA but open sourced it.

https://www.cryptol.net/

Rockwell Collins built SHADE and some other tools for high-assurance crypto. They build stuff for the defense sector mainly funded by NSA. They even have a separation-preserving, verified CPU.

http://www.csl.sri.com/users/shankar/VGC05/Hardin.pdf

There aren't that many people in the world that could build and use a Tamarin model for a crypto protocol, let alone prove it formally. Proof-driven cryptographic engineering is even more specialized than standard cryptographic engineering.

> But if we consider the trend is clearly toward the high-level proof-based code[1], which is way easier to audit, then open source is obviously better.

You disprove your own assertion. Cryptography is very specialized. All specializations in this world require specialized knowledge and niche experience, cryptography included. Assumptions about the obviousness of a specialization is almost itself the definition of an error.