La semaine dernière, Boris Cherny, l'inventeur de Claude Code, a mentionné qu'Opus était capable d'utiliser TLA+ pour trouver des conditions de course dans le code. Maintenant, tout le monde parle de vérification formelle. En tant qu'éducateur de longue date et défenseur de TLA+, c'est excitant. Mais la nouvelle euphorie m'inquiète. Les méthodes formelles ne résoudront pas le développement de logiciels agents une fois pour toutes.

Les conceptions correctes ne se traduisent pas automatiquement en code correct. Pour vérifier une propriété, nous avons besoin d'une propriété à vérifier. TLA+ divise le système en comportements, chacun une séquence d'états. Dans chaque état, nous pouvons exprimer des expressions booléennes avec trois opérateurs temporels : `[]P` (toujours P), `P'` (P dans l'état suivant), et `<>P` (éventuellement P).

`[]P` signifie que P est vrai dans chaque état de chaque comportement, appelé un invariant. `[](x' >= x)` est une propriété d'action. Ce sont des propriétés de sûreté : quelque chose de mauvais n'arrive jamais. Les propriétés de vivacité utilisent `<>` : `[]<>P` signifie que P est vrai dans au moins un état futur de chaque état ; `<>[]P` signifie que P devient vrai et reste vrai pour toujours ; `[](P => <>Q)` signifie que P cause éventuellement Q.