Merz, S. On the Logic of TLA+. Comput. Inform. 2012, 22, 351-379.