Consensus can be defined as all nodes reaching the same state given a variety of (generated) inputs { in this paxos context, it would probably be time / proposal id and proposal val). I’m guessing that if more sophistication was required you could use PropCheck’s state machine properties to ensure all nodes (acceptors) are in the same state beyond what I currently have.
You could probably generate symbolic calls as the aforementioned book talks about in Chapter 4: Custom Generators e.g. a sequence of function calls that are generated with different proposal ids and values…
(From the book) ===> Testing prop_generators:prop_dict_symb() ..............! Failed: After 15 test(s). {call,dict,store,[-6,8, {call,dict,store,[46,-13, {call,dict,store,[2,-2, {call,dict,store,[22,-2, {call,dict,store,[-12,-2, {call,dict,new,[]}]}]}]}]}]}
Here’s some more on consensus in a popular context these days Consensus
Super smart people? @adkron @ferd
Just curious..


















