The Banana and Elevator demos did not specify/verify temporal properties so I suspect it doesn't support specifying temporal formulas at the moment (the T in TL

The Banana and Elevator demos did not specify/verify temporal properties so I suspect it doesn't support specifying temporal formulas at the moment (the T in TLA+). This means it can be used to check correctness properties but not liveness properties. Despite this limitation I believe this is a fantastic tool as it makes writing specs way more approachable.