Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study