, APALACHE TLA + model checker (development version), 2017.

, ByMC: Byzantine model checker, 2013.

I. Abraham and D. Malkhi, The blockchain consensus layer and BFT, Bulletin of EATCS, vol.3, issue.123, 2017.

G. Bracha and S. Toueg, Asynchronous consensus and broadcast protocols, J. ACM, vol.32, issue.4, pp.824-840, 1985.

D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts et al., TLA + proofs, 18th Intl. Symp. Formal Methods (FM 2012), ser, vol.7436, pp.147-154, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00726631

R. Guerraoui, Non-blocking atomic commit in asynchronous distributed systems with failure detectors, Distributed Computing, vol.15, issue.1, pp.17-25, 2002.

I. Konnov, M. Lazi´clazi´c, H. Veith, and J. Widder, A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms, pp.719-734, 2017.

I. Konnov, H. Veith, and J. Widder, Who is afraid of Model Checking Distributed Algorithms, 2012, contribution to: CAV Workshop

, What you always wanted to know about model checking of fault-tolerant distributed algorithms, PSI 2015, Revised Selected Papers, ser. LNCS, vol.9609, pp.6-21, 2016.

L. Lamport, Specifying systems: the TLA + language and tools for hardware and software engineers, 2002.

M. Lazic, I. Konnov, J. Widder, and R. Bloem, Synthesis of distributed algorithms with parameterized threshold guards, OPODIS, ser. LIPIcs, vol.95, p.20, 2017.

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker et al., How Amazon web services uses formal methods, Comm. ACM, vol.58, issue.4, pp.66-73, 2015.

M. , A case study of agreement problems in distributed systems: Non-blocking atomic commitment, pp.209-214, 1997.

Y. J. Song and R. Van-renesse, Bosco: One-step Byzantine asynchronous consensus, DISC, ser. LNCS, vol.5218, pp.438-450, 2008.

T. Srikanth and S. Toueg, Simulating authenticated broadcasts to derive simple fault-tolerant algorithms, Dist. Comp, vol.2, pp.80-94, 1987.

Y. Yu, P. Manolios, and L. Lamport, Model checking TLA + specifications, Correct Hardware Design and Verification Methods, pp.54-66, 1999.