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:
... 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?