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…