# Model Checking Paxos in Spin

arXiv: https://arxiv.org/abs/1408.5962 · HTML: https://mlsanity.com/paper/1408.5962/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Aug 2014.

## Built on by (most cited first, 1 of 1)

- [Learning to generate Reliable Broadcast Algorithms](https://mlsanity.com/paper/2208.00525/) (2022)

## Abstract (arXiv)

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.