spire-tla

TLA⁺ specifications of the Spire single-value consensus algorithm and the Spanning Privilege (SP) multi-value consensus algorithm. A pre-print of Spire and SP is available on IEEE's TechRxiv.

Modules

Module	Description
Spire.tla	Specification of the Spire algorithm.
SpireSafe.tla	Bounded model checking of Spire's safety property.
SpireLive.tla	Bounded model checking of Spire's liveness property.
SpireTlaps.tla	Machine-verifiable proof of Spire's safety.
SP.tla	Specification of the Spanning Privilege (SP) algorithm.
SPSafe.tla	Bounded model checking of SP's safety.

Running

Spire exhaustive correctness check

make check

Spire random simulation

make sim

Spire liveness check

make faircheck

SP exhaustive correctness check

make multicheck

Generate TLA⁺ PDF documents

make pdf