Home

Awesome

TLA+ specifications for Raft, including membership changes

This repository contains a number of TLA+ specifications of the Raft consensus protocol. Of particular interest are the following:

The apalache_no_membership spec is known to work with Apalache 0.16.5 build 417cf58.

Original specs

This repository contains specifications adapted by us (George Pîrlea and Darius Foo) from three different existing Raft TLA specifications, which can be found in the thirdparty folder:

Abandoned effort to annotate membership changes

Besides the above, this repository also contains an abandoned effort to add type annotations to the version of the spec that includes membership changes.

Attribution & Licensing

Our specifications are based on the spec written by Diego Ongaro, with improvements due to Daniel Ricketts, and the addition of cluster membership changes due to Brandon Amos and Huanchen Zhang. We thank them for making these available under a permissive license.

This work is licensed under the Creative Commons Attribution-4.0 International License https://creativecommons.org/licenses/by/4.0/.