The theory of Validating Labelled State transition and Message production systems (VLSMs) enables describing and proving properties of distributed systems executing in the presence of faults. This project contains a formalization of this theory in the Coq proof assistant along with several examples of distributed protocols modeled and verified using VLSMs, including the ELMO (Equivocation-Limited Message Observer) family of message validating protocols and the Paxos protocol for crash-tolerant distributed consensus.
- License: BSD 3-Clause "New" or "Revised" License
- Compatible Coq versions: 8.16 and later
- Additional dependencies:
- Coq-std++ 1.9.0 and later
- Itauto
- Coq-Equations
- Coq namespace:
VLSM - Related publication(s):
We recommend using opam to install project dependencies. Besides the basic building instructions below, we also provide a more detailed building guide, with special recommendations for Windows users.
To install the project dependencies via opam, do:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.18.0 coq-stdpp.1.9.0 coq-itauto coq-equationsTo build the project when you have all dependencies installed, do:
git clone https://github.com/runtimeverification/vlsm.git
cd vlsm
make # or make -j <number-of-cores-on-your-machine>- Lib: Extensions to the Coq standard library and Coq-std++.
- Core: Core VLSM definitions and results.
- Examples: Applications of VLSMs, including tutorials.
- VLSMs that Generate Logical Formulas: construction of VLSMs corresponding to propositional logic symbols, with their composition having well-formed propositional formulas as valid messages.
- VLSMs that Multiply: construction of VLSMs that perform arithmetic operations, with their composition having products of powers as valid messages.
- Primes Composition of VLSMs: construction of an infinite family of VLSMs that multiply and their composition based on primes.
- Round-based Asynchronous Muddy Children Puzzle: the muddy children puzzle as a constrained composition of VLSMs that communicate asynchronously in rounds. For additional background, see the first and second part of a workshop presentation on the formalization.
ELMO (Equivocation-Limited Message Observer) is a family of protocols that demonstrates gradual refinement of a specification to make it validating for increasingly more complex constraints.
- BaseELMO: basic definitions and results related to ELMO.
- UMO: definition and properties of UMO (Unvalidating Message Observer) components and the UMO protocol.
- MO: definition and properties of MO (Message Observer) components and the MO protocol.
- ELMO: definition and properties of ELMO components and the ELMO protocol.
Paxos is a protocol for achieving distributed consensus among network nodes in the presence of crash faults and message loss.
- Abstract Specification of Consensus: specification of consensus as a set of values that can be agreed on by nodes.
- Specification of Consensus by Voting: specification of consensus where nodes agree on a value by voting.
- A Basic Paxos Protocol: specification of consensus by votes from a quorum of acceptor nodes and using a leader node for each ballot.