Merz, S.; Vanzetto, H. Harnessing SMT Solvers for TLA+ Proofs. ECEASST 2012, 53.