Been looking at using formal methods with #tlaplus Mind bending! If you model things as state machines the model checker can check the specification for you. Often it's used in distributed systems, but it can be used for any sort of state machines really. I made a model for the simple #game pong... https://github.com/illume/pong-tlaplus

I can see how it could be used in other types of UI too. As long as you use something like #redux  where actions work on state. 

 @44119516 fun model!