For model checking Alloy might be a better example, it directly builds SAT instances (through the Kodkod constraint solver) that are then solved with a SAT solv

For model checking Alloy might be a better example, it directly builds SAT instances (through the Kodkod constraint solver) that are then solved with a SAT solver. I don't think the standard TLA+ checker (TLC) uses SAT explicitly, though there's an alternate checker (Apalache) that uses a Satisfiability Modulo Theories solver like Z3. (Caveat that I've been wrong about stuff like this before, never dug into the implementation of TLA+ tools, but that's what I pick up from https://lamport.azurewebsites.net/tla/tools.html https://lamport.azurewebsites.net/tla/tools.html )