For decades, randomization has played a central role in distributed computing, offering elegant and practical solutions to problems that are difficult or impossible to solve deterministically. Applications include consensus, synchronization, and leader election algorithms that are increasingly crucial to decentralized systems such as databases and Cryptocurrency exchanges. But despite their prevalence, randomized distributed algorithms are notoriously difficult to reason about, as unexpected behavior arises from the interaction between random sampling and concurrent execution. Informal reasoning and pen-and-paper proofs often overlook those subtleties, leading to incorrect arguments and bugs. In this talk, I will outline the challenges and pitfalls behind randomized concurrent algorithms, and introduce a new foundational program logic for reasoning about such programs.

