Abstract The TLA $$^+$$ + language has been widely used, both in academia and industry, to specify and reason about distributed systems. This paper presents Apalache , an efficient and flexible symbolic model checker for TLA $$^+$$ + . Apalache ’s engine is based on bounded model checking, with symbolic transitions being extracted from TLA $$^+$$ + specifications and verification conditions suitable for satisfiability modulo theories (SMT) solvers being generated from them. Reasoning can be done in terms of safety and liveness properties, with liveness checking realised via a liveness-to-safety reduction. Apalache ’s flexibility lies in its three complementary functionalities: bounded exhaustive verification, for bounded guarantees, randomised symbolic execution, for prototyping and bug detection, and inductiveness checking, for unbounded guarantees. The paper describes Apalache ’s architecture and features, including its support for PlusCal and Quint, two languages that share the same semantic foundation as TLA $$^+$$ + . Industrial usage of Apalache is also presented, together with a case study which illustrates how Apalache can be used to verify the agreement property of a consensus protocol.