http://homepages.inf.ed.ac.uk/ggrov
This is an unofficial reimagining of the Archive of Formal Proofs
A Definitional Encoding of TLA* in Isabelle/HOLby Gudmund Grov and Stephan Merz