Na semana passada, Boris Cherny, o inventor do Claude Code, mencionou que a Opus foi capaz de usar TLA+ para encontrar condições de corrida no código. Agora todo mundo está falando sobre verificação formal. Como educador de longa data e defensor do TLA+, isso é empolgante. Mas a nova euforia me preocupa. Métodos formais não resolverão o desenvolvimento de software agente de uma vez por todas.

Projetos corretos não se traduzem automaticamente em código correto. Para verificar uma propriedade, precisamos de uma propriedade para verificar. TLA+ divide o sistema em comportamentos, cada um uma sequência de estados. Em cada estado podemos expressar expressões booleanas com três operadores temporais: `[]P` (sempre P), `P'` (P no próximo estado) e `<>P` (eventualmente P).

`[]P` significa que P é verdadeiro em todos os estados de todos os comportamentos, chamado de invariante. `[](x' >= x)` é uma propriedade de ação. Estas são propriedades de segurança: algo ruim nunca acontece. Propriedades de vivacidade usam `<>`: `[]<>P` significa que P é verdadeiro em pelo menos um estado futuro de cada estado; `<>[]P` significa que P se torna verdadeiro e permanece verdadeiro para sempre; `[](P => <>Q)` significa que P eventualmente causa Q.