View the project on GitHub
Welcome to the VLSM project website!
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.
This is an open source project, licensed under the BSD 3-Clause “New” or “Revised” License.
The latest released version of VLSM can be downloaded from GitHub.
Report issues on GitHub.