Just found the TLAPS Tactics page: https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html https://tla.msr-inria.inria.fr/tlaps/content

Just found the TLAPS Tactics page: https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Tactics.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T... Sounds like the first thing TLAPS does is to translate the TLA+ program into SMT and try to prove it with Z3. If that times out then it translates it into a couple of other kinds of provers before giving up (...). Maybe I should look at how TLA+ "hello world" is compiled into SMT as a first step.