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