Distributed systems serve as the core of modern computing infrastructure, making their correctness essential. However, the high nondeterminism in the computing environment of distributed systems, combined with the complexity of code design and implementation, makes the correctness verification of distributed systems a significant challenge. Distributed system model checking (DMCK) enables the discovery of deep bugs, deterministic reproduction of bugs in real systems, and repair correctness verification by exhaustive code-level state exploration, thereby addressing the typical problems of distributed systems, such as difficult discovery, diagnosis, and repair. This study provides a systematic summary of the research progress in DMCK. Centering around the trade-off between “state explosion” and “manual effort”, it categorizes the development of DMCK into three stages. The first stage focuses on deterministic simulation execution and state space exploration technologies that make DMCK effective. The second stage introduces a small amount of artificial modeling to leverage system semantics for alleviating state explosion, and the third stage aims to enhance the interaction between the model layer and code layer to improve code-level model checking efficiency. Finally, based on the summary of existing work, this study discusses the current limitations of DMCK and promising development directions in the future.