Summary: Distributed algorithms have received considerable attention and were studied intensively in the past few decades. Under some hypotheses on the distributed system, there is no deterministic solution to certain classical problems. Randomised solutions are then needed to solve those problems. Probabilistic algorithms are generally simple to formulate. However, their analysis can become very complex, especially in the field of distributed computing. In this paper, the authors formally model in “Coq” a class of randomised distributed algorithms. They develop some tools to help proving impossibility results about classical problems and analysing this class of algorithms. As case studies, the authors examine the handshake and maximal matching problems. They show how to use the tools to formally prove properties about algorithms solving those problems.