Bounded Model Checker Modulo Theories Checking executions of TLA+ specifications up to a predefined execution length. Semantics of TLA+ operations is encoded in SMT.