Thanks for the informative answer!
Just a note, I (personally) don’t consider TLA+ a FV technique — it is a really good technique that actually scales much better than formal verification programs like Agda or Coq.
It's formal verification of an abstract machine as opposed to running code. The problem is that formal methods as a field doesn't yet have a rich enough vocabulary to distinguish between its flavors. I use "code verification" and "design verification", which is a little more specific, but has its own issues.
Is TLA+ a sandwich?
> TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.
But it only proves a model, not the actual code — that’s a major distinction.
- the requirements generally change quite frequently
- the requirements are generally a long way from being "formally verifiable"
Where I, personally, have found the most value so far using FV techniques is from modelling "tricky" things whose requirements are quite solid. A few examples from my work:
- A state machine for managing LoRa communication. The requirements in the LoRa spec are pretty good. I took those requirements and designed a state machine I could implement on a low-power device and modelled that SM in TLA+ to verify that there were no deadlocks/attempted transitions to invalid states.
- A state machine for managing the Bluetooth communication between an Android app, a Bluetooth-Iridium (satellite) bridge, and the server on the other side of the Iridium link. Similar to the LoRa case, I used TLA+ to ensure that there were no deadlocks in my proposed SM (and uhh made a number of corrections as I went). Ultimately, due to the design of the BT/Iridium gateway, the exercise resulted in the conclusion that it wasn't actually possible for this process to be 100% reliable but it was possible to detect and retry the edge cases.
- Modelling a somewhat awkward email/SMS invite flow for a mobile app. You could get an invitation over email or SMS, and your account transitioned through a few different states as both your email address and your phone number were verified. Modelling this helped ensure that your account couldn't get into a state where no forward progress was possible or into a state where you could use a half-completed account.