There is large areas in cryptography where if you don’t do it right the whole thing won’t work at all - in that sense there are large parts that are self verifying which collapses complexity. I’m not saying it’s all easy, just that experts can navigate through complexity because they know what to ignore by abstracting it and thinking about properties it holds, not keeping in mind all the guts underneath. Maybe good example is that you can use sha256 effectively in your code without knowing or focusing on how it works internally. You’re interfacing with it through relatively easy properties it has.
There are even larger areas in cryptography where if you don't do it right the whole thing will work, and after a few months someone will make $1B by crashing your currency into oblivion.
Edit: if you want to see how that can happen, I like to take apart weak cryptocurrencies and show what's wrong with them. Someone paid me to do a public review of a thing called Stratis a while back, and I went to town. Here's a highlight. https://twitter.com/PLT_cheater/status/1235036182284820481
I still accept commissions doing code review. It's just too much fun.
Except cryptography usually rely on mathematical proofs. I'm not aware of such possibility for distributed systems. I know Lamport did work on that subject, but i'm not sure if you can equate a TLA+ proof on some properties to a mathematical proof about the structure of numbers, nor do i know if ethereum even has a TLA+ proof or equivalent of anything regarding the PoS protocol (i honestly don't know, so i may be completely wrong).
But the main issue in provable security is that you're trying to prove real world things with math, and so far we're quite bad at it. The more mathematical the thing you want to prove is, the better.
I wouldn't rely on experts being able to navigate through complexity as it happens quite a bit that a major bug in a protocol obliterating it completely is found 15 years after its inception...
Formal? Computer assisted proof checkers? Building strong cryptosystems is notoriously hard, especially when you start composing different systems since some are only secure given certain preconditions which are on you to remember and ensure.
Proof checkers only check for invariants you knew to check for. They're not future proofing against exploits, they're merely a solidification of what you knew about your attack surface at a time.
Good cryptography should be auditable, that means it should be simple. It should not rely on experts knowing their way through the complexity but should rely on mathematical guarantees.
Yes the cryptography primitives should act like black boxes, no need to peak inside but when a number of these black boxes are used together to form a high level protocol allot of subtle things can go wrong for example see the history of SSL/TLS https://www.feistyduck.com/ssl-tls-and-pki-history/
