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.