[nickpsecurity]

There were a number of methods for doing TLA-like stuff. Others included SPIN/Promela, Pi Calculus (IIRC), and Event-B.