I had a fun time recently implementing Raft leader election and log replication (i.e. I didn't get to snapshotting/checkpointing). One of the most challenging projects I've tried to do.
The Raft paper is very gentle to read, and gives you a great intuition on its own. Even if you don't want to implement it, you probably use software that uses it: like etcd or consul or cockroach or tidb, etc.
Some people say Figure 2 of the Raft paper has everything you need but I'm pretty sure that's just not true. It's a little bit more vague than looking at the TLA+ spec to me anyway.
The Raft paper is very gentle to read, and gives you a great intuition on its own. Even if you don't want to implement it, you probably use software that uses it: like etcd or consul or cockroach or tidb, etc.
I collected all the resources I found useful while doing it here: https://github.com/eatonphil/goraft#references. This includes Diego Ongaro's thesis and his TLA+ spec.
Some people say Figure 2 of the Raft paper has everything you need but I'm pretty sure that's just not true. It's a little bit more vague than looking at the TLA+ spec to me anyway.