LTSmin is a toolset for model checking and manipulating labelled transition systems. LTSmin already connects a sizeable number of existing (verification) tools: muCRL, mcrl2, DiVinE, SPIN via an included version of SpinJa, NIPS, CADP and opaal. Moreover, it allows to reuse existing tools with new state space generation techniques. Implementing support for a new language module is in the order of 200–600 lines of C ”glue” code, and automatically yields tools for standard reachability checking (e.g., for state space generation and verification of safety properties), reachability with symbolic state storage (vector set), fully symbolic (BDD-based) reachability, distributed reachability (MPI-based), and multi-core reachability (including multi-core compression and incremental hashing). The synergy effects in the LTSmin implementation are enabled by a clean interface: all LTSmin modules work with a unifying state representation of integer vectors of fixed size, and the PINS dependency matrix which exploits the combinatorial nature of model checking problems. This splits model checking tools into three mostly independent parts: language modules, PINS optimizations, and model checking algorithms. On the other hand, the implementation of a verification algorithm based on the PINS matrix automatically has access to muCRL, mcrl2, DVE, PROMELA, opaal and ETF language modules. Finally, all tools benefit from PINS2PINS optimizations, like local transition caching (which speeds up slow state space generators), matrix regrouping (which can drastically reduce run-time and memory consumption of symbolic algorithms), partial order reduction and linear temporal logic.