TLA+ does have things that make it hard for you to modularize and reuse pieces of it in the large. The first category of problems deal with tooling. TLA+ doesn

TLA+ does have things that make it hard for you to modularize and reuse pieces of it in the large. The first category of problems deal with tooling. TLA+ doesn't have a great story when it comes to automation. There is no package manager. Version control is trickier than it needs to be (it's not obvious what files you might want to commit to git and which you shouldn't when you first start working with TLA+). There isn't a lot of support for automatically running things at the commandline (the community mostly uses the TLA+ toolbox, which is a GUI-based IDE). You can and people do these things, but they feel like distinctly second-class citizens. Really TLA+ feels tied to the TLA+ toolbox, warts and all. The second problem is language support. TLA+'s main way of breaking down problems into modules and then using one module as an interface for another (its notion of refinement) suffers from problems analogous to the ones faced when dealing with inheritance. In TLA+'s case, it is easy to add additional new states into a state machine defined in another module (this is TLA+'s celebrated idea of stuttering), but is rather more annoying to do the opposite, e.g. show that in your new module a single state is meant to correspond to a two states in another module (e.g. you have a transaction primitive that allows you to assume that two states can be done simultaneously). This is complicated by the fact that the easiest verification technique in TLA+ is model-checking, which fares the worst when dealing with transitive chains of logical implication. TLA+'s model checker does not have a native notion of logical implication. Instead the way you e.g. prove the statement A => B is by effectively proving A and B but privileging A to be the search space that the model checker operates in. This means chains of the form A => B, B => C, C => D and therefore A => D (and all the intermediate stages) are somewhat annoying. You either prove each step with separate models along the chain and just let a human infer that this means A => D, or you prove the statement A => (B and C and D), without using any of the intermediate implications. Without robust support for transitive implication, the option of using composition in the traditional composition vs. inheritance debate becomes much less palatable as an option when it comes to inheritance. To some extent this is a limitation inherent in model checking and goes away with the proof based verifier for TLA+ TLAPS. But there isn't a collection, that I know of, of proved theorems for TLAPS like many other theorem provers. I suspect again this is due to both the lack of a package manager in the TLA+ ecosystem as well as some not so ergonomic parts of TLAPS. TLAPS feels very magical. Its main way of proving things is what's often referred to as sledgehammer or auto in other theorem provers; write the next step in your proof and hope the computer is smart enough to infer it from the previous step. It feels magical when it works. When the computer can't figure something out, it can be a huge pain to figure out why. It doesn't feel like I'm mechanically building up a proof so much as it feels like I'm playing a guessing game with the computer to see which leaps of logic it'll accept. This gets better with time as you develop an intuition of which leaps work and which don't, but can still be painful. This is mainly because TLAPS itself isn't a prover, but rather delegates to the "magic" methods of other provers. Finally set theory and first order logic, the theoretical basis of TLA+, sometimes makes showing equivalence between items (which is vitally necessary when dealing with code written by multiple individuals who might use different encodings for the same idea) very difficult. In particular, trying to use the fact that A is equivalent to B, therefore some predicate P has an exactly analogous P' on B is tricky. Another way of stating this is that TLA+ as a language makes it a bit difficult to leverage isomorphisms and homomorphisms to reduce the amount of work you have to do. This is somewhere where alternative logical systems can have a big leg up. All that being said, among the technologies commonly referred to as "formal verification," I would say that TLA+ is the one I would most commonly recommend to people in business situations. This precisely because of what many people view as a flaw, that TLA+ is a formal specification language and not a way to actually write or verify actual running code. Because TLA+ specs are divorced from your codebase, they require far less buy-in to see dividends. You don't have to rewrite your codebase in another language. You don't even have to change your coding practices. Indeed TLA+'s closest competitor on most teams is also precisely what most teams lack, which is high-quality documentation. This means you can integrate TLA+ into your work with extremely little risk. Try formalizing your mental model in TLA+. See if it reveals interesting conclusions. If it does, congratulations! TLA+ has been useful to you and you can keep it around as an artifact detailing your thoughts in the future. If not, delete your specs and no harm no foul. No code depends on its existence. You don't need some lengthy transition period to migrate systems away from "using" TLA+. You lose no more time than the amount you put into writing your spec.