/spire-tla

A TLA⁺ specification of the Spire consensus protocol

Primary LanguageTLABSD 3-Clause "New" or "Revised" LicenseBSD-3-Clause

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