Hi Lucas,
I've been using TLA+ for specifying front-end development on a couple projects now. I will try to put some thoughts together in a blog, but a few quick thoughts below.
- Angular can be viewed as a state machine. Modeling user flows through Angular can identify invariants like, "When a user signs up with a phone number, and then exits registration, if they continue registration, the user will eventually provide their email address." Translating workflow diagrams into TLA+ can identify where improper assumptions have been made.
- Many standard multitier web applications (frontend, backend, DB, maybe there's a cache and/or pub-sub queue) can be modeled with TLA+ in a single specification. This means that we can model data flows in a single file, which can be good for early design and other invariants like, "The system will never store bad data in the database."
I would look into articles[1] which discuss SPA as state machines (the linked article mentions the project xstate [2] which I think could be an interesting companion to TLA+). Learn TLA+ or Pluscal with a focus on states and transitions. I have found that just identifying some invariants in your system can be an important way to understand the project and better discuss with stakeholders. I will try to post some example specifications in the next week or so.
Cheers,
Sam