In this project, a decentralized consensus algorithm, BenOr is implemented using PlusCal and TLA+. BenOr protocol is a binary protocol which decides commit or abort for each instance. For more details about the algorithm, please refer the proof document in the following link
[BenOr Research paper link] (https://www.researchgate.net/publication/255574059_Correctness_Proof_of_Ben-Or's_Randomized_Consensus_Algorithm).
In this project, to test the specs for different scenarios and analyze what can go wrong in distributed set up, TLA+ model checker is used for the validation and model checking.