/MultiPaxos

MultiPaxos and Disk Paxos in TLA+ and PlusCal

Primary LanguageTLAMIT LicenseMIT

MultiPaxos

A formalization of the Multi-Paxos algorithm. Heavily inspired by a few of Leslie Lamport's papers.

Also contains a formalization of Disk Paxos in PlusCal.