Les algorithmes distribués probabilistes se formulent simplement, cependant leur analyse est complexe car il faut traiter à la fois l'aspect distribué et l'aspect probabiliste. Dans cet article, nous présentons une formalisation en Coq d'un algorithme distribué probabiliste résolvant le problème du rendez-vous. Cette formalisation nous permet de raisonner et de prouver des propriétés telles que la terminaison ou des calculs de probabilités.