Guanzhou Hu

Feeling comfortably numb

Find me on GitHub

CV | LinkedIn | Google Scholar (at)
josehu (at)

To all my loved ones and my friends ♥
GitHub Pages — Theme by orderedlist

Practical SMR-style TLA+ Specification of the MultiPaxos Protocol

19 Feb 2024 - Guanzhou Hu

The attached files present a practical TLA+ specification of MultiPaxos that very closely models how a real state machine replication (SMR) system would implement this protocol. I did not find anything similar on the web, so I’d like to share it with anyone interested.

Files of This TLA+ Spec

Below are the files composing the checkable model (organized in VSCode extension style):

What’s Good About This Spec

This spec is different from traditional, general descriptions of Paxos/MultiPaxos in the following aspects:

This spec has been accepted into the official TLA+ Examples repo! 1

Here are some links I found particularly useful when developing this spec by myself: 2 3 4 5

Update: Extended Spec with Extra Features

Below are the files composing an extended version of the spec along with model inputs:

What’s New in the Extended Spec

The extended spec includes the following extra features/variants of MultiPaxos that are very essential and useful in practice:


Please comment below anything you wanna say! 😉