[agentultra]

For some trivial small problems writing a model in TLA+ or Lean is definitely more costly than just writing the software even if you get a few things wrong. It'd be like commissioning a blueprint for your shed in the backyard. For those sorts of tasks it is sufficient to just write a few tests and call it a day.

However for more complex services that are trying to manage several clusters of resources amongst tens of thousands of tenants or more there are invariably going to be errors. The kinds of errors you see might require a particular series of events to change your state in 53 steps to hit it... but if you're servicing > 1M requests in a minute that ends up being frequent enough to be bothersome.

Even more so if you're working on a memory controller in a new hardware platform that is expected to ship in a few million units. It'd be nice to know that you have strong evidence that your system is correct.

And developing models is hard but so is thinking. Nobody said it was easy. But one shouldn't say that we can't engineer robust software systems. It's just patently false.