For proving distributed computing protocol soundness, I'm a big fan of formal verification and model checking, in particular TLA+[1] by Leslie Lamport who is be

For proving distributed computing protocol soundness, I'm a big fan of formal verification and model checking, in particular TLA+[1] by Leslie Lamport who is behind the Lamport clocks referenced in the paper and curiously Latex, and the well known Byzantine generals problem in blockchains. In particular a peer-reviewed on synchronization protocol has been proven incorrect on a subtle race condition using formal verification. [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html