I am very interested in TLA+. I work on an existing application, say, for serving graphs to customers on the frontend. I want to, for example, add a new button to the front end to turn on dark mode.
What I want to know from experienced formal methods folks: how do I go about scoping my new feature in TLA+? Do I have to model my entire system in the language, or just a subset of features? Is my example even a good use case for TLA+?
What I want to know from experienced formal methods folks: how do I go about scoping my new feature in TLA+? Do I have to model my entire system in the language, or just a subset of features? Is my example even a good use case for TLA+?