TLA+

TLA+ is a formal specification language for identifying design flaws in distributed systems. When we last blipped it in 2015, the investment was too high for all but critical systems. Since then, coding agents have changed the calculus: the cost of using TLA+ has gone down, while its value has gone up. TLA+'s awkward developer experience is no longer a blocker, although teams looking for friendly syntax might prefer Quint. We've observed teams verify application traces against a TLA+ model without prior experience.

Meanwhile, developers now have greater need for quality assurance techniques to manage agent-generated code. Where TLA+ was once the preserve of organizations like AWS, which used it to find subtle bugs in DynamoDB, it's now part of a broader trend of polyglot verification, alongside techniques like mutation testing and property-based unit testing.

Building systems using microservices requires us to think more deeply about failure isolation and testing. *TLA+ *is a formal specification language that can be useful in both these scenarios. For failure isolation, TLA+ can be used to identify invariants in your system that can be monitored directly. An invariant can be the ratio of number of requests to one service to the number of requests to a second service, for example. Any change in this ratio would lead to an alert. TLA+ is also being used to identify subtle design flaws in distributed systems. Amazon, for example, used model-checking based on a formal specification written in TLA+ to identify subtle bugs in Dynamo DB before it was released to the public. For most systems, the investment required to create the formal specification and then perform model checking is probably too great; however, for critical systems - complex ones, or those with many users - we think it’s very valuable to have another tool in our toolbox.