Specification

Developing distributed and concurrent systems is a complex task that requires careful attention to the details. Testing such systems is challenging because it’s difficult to simulate all possible states, including those that can happen due to system failures, network latency, and other factors. This makes it hard to ensure that the system behaves correctly in all circumstances.

Therefore it’s essential to have a proactive approach that involves modeling the system’s behavior in a formal way. Such an approach can help identify potential issues before they occur, saving time and preventing costly flaws.

TLA+

TLA+ is a formal specification language developed by Leslie Lamport based on the idea of specifying systems using simple mathematics. It is used for designing, modelling, documentation, and verification of programs, especially concurrent and distributed systems. TLA+ and its tools are useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code.

To know more about TLA+, check The TLA+ Home Page.

Anemos Consensus Spec

The Anemos consensus specification (inherited unchanged from Pactus, so the source filenames intentionally stay Pactus.*) is written in TLA+ format. It includes all invariants that can be held in every state of every execution that the protocol allows. The TLA+ specification is compiled into a PDF file.

Scope of this proof — the inherited BFT consensus core only. The TLA+ specification is the unmodified Pactus model: it covers the inherited BFT consensus core — the propose / prepare / precommit / commit voting state machine and its change-proposer rounds — and the safety/liveness invariants over those states. It does not model the Anemos consensus-embedded oracle or its slashing: the per-block OracleData section folded into Block.Hash(), the committee-subset price signing, and the commit-time deviation slashing are outside the scope of this formal model. The oracle’s separate security argument (subset rotation, the TWAP, the honest-majority-of-stake ceiling, and deviation/availability penalties) is given in the whitepaper §2.2 and §5, not here.

Safety Proof

By defining some invariants we can ensure the safety of the consensus protocol in any possible and distinct state, and therefore we have the informal safety proof of the inherited BFT consensus core (propose / prepare / precommit / commit) using TLA+ — the proof does not cover the Anemos oracle or its slashing (see the scope note above).

Liveness Proof

Checking the liveness is not easy, but with defining some constraints, we have the informal proof of liveness of the inherited BFT consensus core using TLA+ (again, the Anemos oracle/slashing layer is out of scope — see the whitepaper §2.2/§5 for its separate argument).