TLA+

Block a spécifié en TLA+ le protocole de stockage Git derrière Buzz, et l'a vérifié par model-checking pour la durabilité, la reconstruction et les push concurrents. Le billet d'ingénierie de Tyler Longwell du 21 juillet 2026 décrit ce qui est vérifié : des dépôts conservés comme des packfiles immuables adressés par contenu, plus un pointeur de manifeste mutable, avancé par un compare-and-swap conditionnel qui fait office de point de commit. Le résultat est conditionnel. Il ne tient que sous trois garanties explicites fournies par le magasin d'objets, ce qui explique pourquoi Block l'accompagne d'une suite de conformance par backend.

TLA+ apparaît une deuxième fois dans la même base de code : l'isolation multi-tenant est formalisée en TLA+, les propriétés d'autorisation en Tamarin. Le rapport de recherche du 12 août 2026 juge ce volume de travail formel rare pour une version v0.4.x/0.5.x.

Julien Lépine, CTO d'AWS France, présente les choses différemment dans If This Then Dev #351. Quand du code peut être généré à raison de 100 000 lignes par jour, le problème devient de garder le contrôle sans tout lire. Il décrit la modélisation formelle en TLA+ comme un moyen de tenir des invariants, avec du raisonnement automatisé pour borner les agents et une IA vérifiant la divergence entre le code et le modèle. DynamoDB, à plus de 5 000 milliards de requêtes par heure, est l'échelle qu'il cite.

Block, Boris Cherny et DynamoDB sont les utilisateurs recensés, ce qui place un langage de spécification formelle au centre de la question du code généré par agents. Le billet de Longwell ne comporte ni chiffres ni benchmarks : c'est un exposé de conception, et ce que coûte le maintien de l'alignement entre le modèle et le code n'est pas précisé.