Do you happen to have any intuition pump here? Any term of art or class of tests to throw LLMs at to get a sense for these?
An UI is a state machine and TLA+ is a tool for validating state machines. You can e.g. ask it to prove that every state is reachable from every other state (so users can’t get stuck somewhere even when a network request fails etc) or you can assert stuff renders correctly in sequence, or that key shortcuts change with the context correctly, or…
I used TLA+ in a (hobby) web app by asking it to model the endpoints and the data user can get from them, and then what kind of access that data can grant in the system, and then implement some properties over that kind of data. I suppose basically like "you can't get access to another user's shopping basket", although mine was maybe a bit more convoluted.