TLA+ specification cycle — Jack Vanlightly