The CBC Team at Runtime Verification, Inc. is happy to announce release 1.3 of VLSM, a Coq framework for modeling and verifying distributed systems executing in the presence of faults. The framework is available as the package coq-vlsm in Coq’s package index and is compatible with Coq 8.16, 8.17 and 8.18.
The framework builds on the theory Validating Labelled State Transition and Message Production Systems, which is described in an accompanying paper. The framework’s release notes and links inside the paper further clarify the relationship between the theory and the Coq definitions and results.
VLSM notably supports reasoning about systems subject to equivocation, a fault mode where system components claim different beliefs about the state of a distributed protocol to different parts of the system in order to steer the protocol-abiding components into making inconsistent decisions. A key result connects the framework to unrestricted Byzantine behavior, establishing that the effect that Byzantine components with unrestricted faults can have on honest, well-behaving components is no different than the effect equivocating components can have on non-equivocating components.
To demonstrate the framework’s functionality and expressiveness, the release provides several tutorial examples as well as formalizations of the ELMO family of message validating protocols emerging from the Ethereum blockchain community and the Paxos protocol for crash-tolerant distributed consensus.