[agentultra]

I could fill a blog post about it but in my current project we're using TLA+ for two things:

1. Helping us design features whose requirements are vague. The more hand-waving required to explain a particular feature the more likely we are to use TLA+ to model our assumptions and verify our understanding. This has led us to ask some interesting questions of our design team to help us build a better feature.

2. Requirements that are really hard that we need to ensure are implemented correctly. We use TLA+ to ensure the properties and invariants are correct with respect to the requirements and validate our model. This is really helpful in the case of concurrency and consistency. For our application we're using event-sourced data and it's imperative that our event store is consistent in the face of concurrent writers, can be replayed in a deterministic and consistent order, and that our assumptions will hold between versions of the events.

[mxschumacher]

Ah - interesting! I would not have expected 1. I will dig into TLA+ and try to understand it better.

Thanks! Please do consider writing a blogpost, I'm sure many here would appreciate it.