This repository contains specifications related to the Stellar Consensus Protocol (SCP).

The balloting protocol

AbstractBalloting.tla contains a high-level specification of SCP's balloting protocol in terms of logical federate-voting messages (also see the PDF version AbstractBalloting.pdf). This specification will be useful to prove that the concrete balloting protocol is correct by refinement.

We provide an inductive invariant implying the safety property. On Linux, you should be able to check that this invariant is inductive using the Apalache model-checker by running make abstractballoting-safety. This checks the invariant for the system parameters defined in ApaAbstractBalloting.tla.

Balloting.tla contains a specification of the PREPARE and COMMIT phases of the balloting protocol(also see the PDF version Balloting.pdf). On Linux, you should be able to check with the TLC model-checker that the Balloting specification refines the AbstractBalloting specification using make balloting-refinement. This checks the refinement for the system parameters defined in TLCBalloting.tla.

The nomination protocol

The nomination protocol is a sub-protocol of the Stellar Consensus Protocol.

Nomination.tla is written in TLA+ and set up to check the main liveness properties of the protocol with the TLC model-checker. This is best viewed or edited with the TLA Toolbox or the TLA+ extension for VS Code. Nomination.pdf is a typeset version of the specification.

NominationPlusCal.tla is written in the PlusCal Algorithm Language, which transpiles to TLA+ (the transpiled code appears between the \* BEGIN TRANSLATION and \* END TRANSLATION markers). Best viewed or edited with the TLA Toolbox. NominationPlusCal.pdf is a typeset version of the specification.

Nomination.qnt is written in quint, a new language that also transpiles to TLA+ but also has its own tooling. Best viewed or edited with the quint extention for VS Code. Use the quint REPL to run tests and random simulations. For example, on my setup I can run npx quint -r Nomination.qnt::Test, which loads the Test module and starts the quint REPL. Then I can run run1 (in the REPL), which prints true (which means run1 is a valid behavior of the specification). Finally I can run (again in the REPL) stateAsRecord to print all the variables in the state reached at the end of run1.