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