A HOL example formalizing pGCL (Probabilistic Guarded Command Language).

pGCL supports both demonic and probabilistic choice, so can in principle
be applied to the verification of distributed random algorithms.

The high-point of this example is the verification of the probabilistic
voting scheme in Rabin's mutual exclusion algorithm.