> TLA+ is very useful but only few services adopt and benefit from it. It's true that formal specifications are rarely used, but I would bet that the ratio of

> TLA+ is very useful but only few services adopt and benefit from it. It's true that formal specifications are rarely used, but I would bet that the ratio of those that benefit significantly from them to those that use them is far greater than many other, far vaguer tools. > Also it's not very readable That depends on what you mean by "readable." A prose description can appear readable in the sense that the reader may think they understand what the document says, but sometimes that's just because the text is vague enough to allow for conflicting interpretations. TLA+, on the other hand, is precise. True, it takes some learning, but it's easier to learn than a programming language, as it's much, much smaller (the reference documentation for the entire language and all of the standard library fits comfortably on 7 pages (https://lamport.azurewebsites.net/tla/summary.pdf https://lamport.azurewebsites.net/tla/summary.pdf) > and cannot document many design aspects e.g. the reasons behind technical decisions It can document some decisions very well. For one, you can state precisely your assumptions as well as the requirement. You then describe the desired operation of the system. You can then check that the design fits the requirements given the assumptions, and show that other designs don't. It is true that it's not intended to model the reasoning behind every decision, such as cost/time of implementation, but generic (i.e., non-software-specific) project management tools can help you with that. Now, I am not saying that a formal specification is always required, and I agree that writing down an informal one is far better than not writing down anything at all, but it can really save a lot of time and trouble in subtle/complex/unclear cases.