formulation-proof

This is my first attempt that I write the codes of a proof of a consensus protocol using TLA+ so some errors may exist.

Run the code

Download TLA toolbox and add the source code to your own project and then you can run it.