Distributed systems are challenging to formally verify due to their concurrent and asynchronous nature. Significant advances have been made in reducing this complexity for individual systems, but modern applications are often composed of multiple distributed systems, which most current verification tools are not well-equipped to handle. In this talk, a novel, compositional atomic distributed object model that can greatly simplify high-level reasoning about both individual and composite distributed systems will be presented. The atomic distributed object model builds on work on shared-memory concurrency. It specifies distributed systems using a new push/pull semantics that abstracts away low-level details such as network delays and failures. An object’s state is partitioned into a persistent component and a tree of volatile caches that methods nondeterministically update to model as-yet uncommitted state changes. This model is general enough to faithfully capture common behaviors of many strongly consistent replicated distributed systems including Paxos, Raft, and Chain Replication. A distributed system verification framework is implemented in Coq with the atomic distributed object model at its core. The framework provides more standard intermediate specifications for both Paxos variants and Chain Replication so that the abstract object model can be formally connected to concrete distributed system implementations through refinement. Examples will demonstrate that proving properties even of composite distributed systems can be straightforward thanks to the elegant object interface.