The first is a proof published in a paper that you can read. I recall the proof is for single decree paxos. In reality, you need multiple rounds. There are many

The first is a proof published in a paper that you can read. I recall the proof is for single decree paxos. In reality, you need multiple rounds. There are many subtle variations and I am not aware of a proof for that. Is an implementation correct? Frankly, that is a PhD thesis that is still to have been written. If you want to do a PhD and this topic burns inside you, go for it. Regarding consensus algorithm overview, no .. not that I know of. Here is a good video on Paxos: https://www.youtube.com/watch?v=JEpsBg0AO6o&t=2545s https://www.youtube.com/watch?v=JEpsBg0AO6o&t=2545s Enjoy my friend.