MVDS

TLA+ specification of the MVDS spec.

Model Checking

SpecOK: This Model runs with 2 Nodes and uses the AllMessagesDelivered state constraint. It proves that messages are eventually received by peers if requested.