That's quite an interesting algorithm, especially the random selection part. I'd really like to read the original paper!

I found a correctness-proof which includes peseudo-code in the papers "Correctness Proof of Ben-Or’s Randomized Consensus Algorithm"[1] and "The correctness proof of Ben-Or’s randomized consensus algorithm"[2].

[1] http://ecommons.cornell.edu/bitstream/1813/7336/1/98-1682.pd... [2] http://www.cs.toronto.edu/~samvas/teaching/2221/handouts/ben...