Verifying Almost-Sure Termination for Randomized Distributed Algorithms

Constantin Enea

doi:10.1145/3776691

Return

Verifying Almost-Sure Termination for Randomized Distributed Algorithms

2026-01-01

PRE

Constantin Enea *

Rupak Majumdar

Harshit J. Motwani

V. R. Sathiyanarayana

DOI：10.1145/3776691

Original

Original request for help

Save

Abstract

En 中文

We present a technique for the verification of liveness properties of randomized distributed algorithms. Our technique gives SMT-based proofs for many common consensus algorithms, both for crash faults and for Byzantine faults. It is based on a sound proof rule for fair almost-sure termination of distributed systems that combines martingale-based techniques for almost-sure termination with reasoning about weak fairness. Our proof rule is able to handle parametrized protocols where the state grows unboundedly and every variant function is unbounded. These protocols were out of scope for previous approaches, which either relied on bounded variant functions or on reductions to (non-probabilistic) fairness. We have implemented our proof rules on top of Caesar, a program verifier for probabilistic programs. We use our proof rule to give SMT-based proofs for termination properties of randomized asynchronous consensus protocols, including Ben-Or's protocol and graded binary consensus, for both crash and Byzantine faults. These protocols have notoriously difficult proofs of termination but fall within the scope of our proof rule.

Keywords:

probabilistic programs

proof rules

almost-sure termination