We describe the design and implementation of Must, a framework for modeling and automatically verifying distributed systems. Must’s modeling language provides a set of communication models formalized by a partial-order semantics, on top of a mainstream programming language, e.g. Rust. Given a program using Must’s API, Must verifies it by means of a novel, optimal dynamic partial order reduction algorithm that maintains completeness and optimality for all communication models supported by the API.

We use Must to design and verify models of distributed systems in an industrial context. We demonstrate the usability of Must’s language by modeling higher-level-system idioms (e.g., timeouts, leader election, versioning) as abstractions over the core language, and demonstrate Must’s scalability by verifying systems employed in production, such as replicated logs and distributed transaction management, the verification of which lies beyond the capacity of previous model checkers.