Proofs are programs and programs are proofs of themselves. The ways proofs might help you show that a program is "correct" (what you meant to say) are 1. the effect of writing it twice in different languages 2. that proofs may be more abstract and you can refine the program from them.

But a proof/formal methods can't actually prevent you from being wrong because you can be wrong at any meta level.

> "correct" (what you meant to say)

Oh, this is a definition of "correct", it's not me correcting the OP.

But the human world is not exact and full of context. Even mathematical.proofs exist within a context of an axiomatic system, known proofs, and various domain assumptions.

I remember that in my computability theory class, defining the right proof was by far the most difficult task. And this was in very small, closed systems.

> But the human world is not exact and full of context.

That is of course correct. However, it was my impression that the contract mentioned in the OP was completely on the blockchain, and therefore completely deterministic (no oracles or whatever.) Hence I figured it could've been proved with absolute rigor, in which case it should've been possible to formally prove the correctness. I'll be honest, I didn't look through the contract in detail now, so I might be wrong.

It's possible that maybe, just maybe, the interior world of some crypto scheme may have sufficient formal proofs.

It doesn't change the fact that the crypto system lives in a human world were law, politics and attacks can coerce you to do a lot of things and the formality of the system is just irrelevant.