O TLA+ é uma linguagem de especificação formal para identificar falhas de design em sistemas distribuídos. Quando publicamos sobre ela pela última vez em 2015, o investimento era alto demais para quase tudo, exceto sistemas críticos. Desde então, agentes de programação mudaram esse cálculo: o custo de usar TLA+ caiu, enquanto seu valor aumentou. A experiência de desenvolvimento desconfortável do TLA+ não é mais um bloqueador, embora equipes que buscam uma sintaxe amigável possam preferir o Quint. Observamos equipes verificando traces de aplicações em relação a um modelo TLA+ sem experiência prévia.
Enquanto isso, pessoas desenvolvedoras agora têm maior necessidade de técnicas de garantia de qualidade para gerenciar código gerado por agentes. Onde o TLA+ antes era exclusividade de organizações como a AWS, que o usava para encontrar bugs sutis no DynamoDB, agora ele faz parte de uma tendência mais ampla de verificação poliglota, ao lado de técnicas como [testes de mutação](/radar/techniques/mutation-testing testes unitários baseados em propriedades.
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.
