I don’t know TLA+, but I find it interesting that the author indicates one of the strengths of TLA+ is it’s shared global memory when as programmers one is advised to never have global shared memory.