Model Checking Paxos in Spin

TL;DR

This paper models the Paxos consensus algorithm in Promela with counting guards, enabling automated verification of quorum conditions using the Spin model checker.

Contribution

It introduces counting guards in Promela for modeling majority voting, and applies Spin to validate and analyze Paxos protocol instances.

Findings

Validated finite Paxos models with Spin

Extracted quorum size preconditions

Demonstrated formal verification of distributed consensus

Abstract

We present a formal model of a distributed consensus algorithm in the executable specification language Promela extended with a new type of guards, called counting guards, needed to implement transitions that depend on majority voting. Our formalization exploits abstractions that follow from reduction theorems applied to the specific case-study. We apply the model checker Spin to automatically validate finite instances of the model and to extract preconditions on the size of quorums used in the election phases of the protocol.