S. Merz and H. Vanzetto, “Harnessing SMT Solvers for TLA+ Proofs”, ECEASST, vol. 53, Nov. 2012.