Model-checking the Raft spec

[A. Jesse Jiryu Davis]

Hello! I was curious about the Raft TLA+ spec. I'd like to model-check it, enhance it with leader leases, and model-check it again. First step: model check Diego Ongaro's original spec.

In the repository README, Ongaro encourages us to use a version in an open pull request instead of the main-branch version:

https://github.com/ongardie/raft.tla

... but neither version has any invariants or temporal properties, and there's no config file. I suppose Ongaro just used this spec for description and perhaps proof, not model-checking.

So, has anyone model-checked a version of this Raft spec? Any tips or public code?

[A. Jesse Jiryu Davis]

There are obvious model-checking tricks like a SYMMETRY declaration, and additional state constraints, that I hope someone has already done for me. It looks like the current spec's state space is infinite.

[Markus Kuppe]

Hi Jesse,

you should be able to reuse much from https://github.com/microsoft/CCF/blob/main/tla/consensus/ccfraft.tla

M.