> In the end we all know that the answer is for humans to stop doing this work. We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them. This would ensure that the protocol actually does what it says, and that implementers don’t further screw it up, thus invalidating the security proof.

And yet, there are still regular posts here about whether static type systems have any merit at all... never mind advanced things like linear/dependent types, theorem provers, TLA+, etc. Just use Go!