TLA+ (Temporal Logic of Actions) is een formele modellerings-toolkit die wordt gebruikt om het gedrag van systemen te definiëren via overgangssystemen en temporele eigenschappen, zoals Safety (er gebeurt nooit iets slechts) en Liveness (er gebeurt uiteindelijk iets goeds).
Hoewel TLA+ waardevol is voor het ontwerpen van betrouwbare gedistribueerde systemen, kent het beperkingen. Model checking via TLC is beperkt tot eindige instanties en er bestaat vaak een kloof tussen de abstracte specificatie en de uiteindelijke software-implementatie.
Om deze kloof te dichten, wordt gekeken naar moderne bewijssystemen:
- Lean: Voor interactieve, stapsgewijze bewijzen.
- Verus: Specifiek ontworpen voor Rust, waardoor specificaties en bewijzen direct in de code kunnen leven.
Het team van Reasonable werkt aan het automatiseren van dit proces met AI-agenten. Ze hebben een pijplijn ontwikkeld die TLA+-specificaties vertaalt naar machine-gecontroleerde Verus-bewijzen, waarbij een prover-reviewer loop wordt gebruikt om de correctheid van de gegenereerde bewijzen te waarborgen.
Het internet ontdekt TLA+. En nu?
De virale tweet van Boris Cherny liet zien hoe nuttig formele modellen kunnen zijn bij agentic coding. Dit artikel geeft een praktische introductie in wat TLA+ precies is.
TLA+ is echter slechts het startpunt. We kijken ook naar hoe temporele specificaties, moderne bewijssystemen en AI-agenten samen kunnen werken: van het modelleren van systeemgedrag tot het genereren van machine-gecontroleerde bewijzen, met als uiteindelijk doel software die in één cyclus wordt gespecificeerd, geïmplementeerd en geverifieerd. We geven daarnaast een inkijkje in het werk dat we bij Reasonable doen om dit mogelijk te maken.
Boris tweet, het internet kopieert
Deze week bracht Boris Cherny TLA+, een formele modellerings-toolkit die al meer dan 30 jaar oud is, terug in de schijnwerpers met een tweet. Hij gebruikte Opus 5.5 om delen van de Claude Agent SDK te modelleren in TLA+ en Lean. Het resultaat was typisch voor het internet: ongeveer een miljoen weergaven, duizenden bladwijzers en een golf van vragen over wat TLA+ nu eigenlijk is. De post van Boris is een uitstekende showcase en sluit aan bij eerdere voorbeelden die aantonen dat TLA+ de moeite waard is bij agentic coding (zie bijvoorbeeld de post van Datadog over harness-first agents).
Voor wie zich nu afvraagt wat TLA+ is en waarvoor het dient: TLA+ is een van de formele technieken waar ons team zich diep in heeft verdiept.
De reden waarom we dit belangrijk vinden, is dat TLA+ ons een compacte taal biedt om te definiëren wat een systeem mag doen en wat er altijd (of uiteindelijk) waar moet zijn. Dat is een nuttig startpunt voor verificatie, maar het is niet het eindpunt.
In het kort:
- TLA+ beschrijft mogelijke systeemgedragingen en de eigenschappen waaraan deze gedragingen moeten voldoen.
- TLA+ verifieert op zichzelf geen volledige implementatie. Het controleert een model van de software, niet de software zelf, en de belangrijkste model checker onderzoekt alleen eindige instanties.
- Moderne bewijssystemen kunnen ons verder brengen. In Verus kunnen specificatie, bewijs en de Rust-implementatie in dezelfde taal bestaan.
- AI kan delen van dit proces al automatiseren. We hebben een agentische pijplijn gebouwd die meer dan 16.000 TLA+-specificatie/eigenschap-paren heeft omgezet in meer dan 3.000 machine-gecontroleerde Verus-bewijzen.
De interessante vraag is dan ook niet alleen of een agent TLA+ kan schrijven, maar wat er mogelijk wordt zodra agenten kunnen schakelen tussen specificaties, bewijzen en echte programma's. Een deel van ons werk bij Reasonable is het trainen van modellen om agenten in staat te stellen dit consistent, betrouwbaar en snel te doen.
Wat TLA+ is
Stel je een scenario voor waarbij drie computers (a, b en c) het eens moeten worden over wie de leider is. Databases vertrouwen op een correcte leidersverkiezing. We stellen de eis dat er nooit twee leiders tegelijkertijd mogen bestaan.
TLA+ (Temporal Logic of Actions) is een taal voor het vastleggen van twee soorten objecten:
- Een overgangssysteem (transition system): Wat het systeem kan doen. Er zijn toestanden (states), die snapshots van het systeem zijn (wie is kandidaat, wie heeft op wie gestemd, wie is leider), en acties, wat enkelvoudige stappen zijn die een toestand veranderen ("a start een verkiezing", "b stemt op a").
- Temporele eigenschappen (temporal properties): Uitspraken over hoe een uitvoering zich in de loop van de tijd ontwikkelt. Bijvoorbeeld: "Er zijn nooit twee leiders" of "Er wordt uiteindelijk een leider gekozen."
Een TLA+-model definieert legale systeemtoestanden en toegestane overgangen tussen deze toestanden. Het legt geen volgorde op de overgangen en probeert de kansverdeling van verschillende gebeurtenissen niet te modelleren. Dit is de juiste abstractie voor gedistribueerde systemen, waar berichten, timeouts en gebruikersacties in veel verschillende volgordes kunnen voorkomen.
De onderliggende wiskunde is eenvoudig en maakt gebruik van verzamelingen, waar/onwaar-uitspraken en relaties. Temporele eigenschappen worden vervolgens opgebouwd uit operatoren over uitvoeringen:
- $\square P$ (altijd P): P geldt in elke bezochte toestand.
- $\Diamond P$ (uiteindelijk P): P geldt in een toekomstige toestand.
- $P \rightsquigarrow Q$ (P leidt tot Q): wanneer P geldt, geldt Q uiteindelijk daarna.
Er zijn twee soorten eigenschappen die bijzonder vaak van belang zijn:
- Safety (Veiligheid): Er gebeurt nooit iets slechts. Voor onze verkiezing: $\square$ (er zijn nooit twee leiders). De model checker onderzoekt elke mogelijke toestand en bevestigt de eigenschap. Als een regel wordt gewijzigd waardoor een computer twee keer kan stemmen, zal de checker een tegenvoorbeeld teruggeven: een concrete manier waarop het model de eigenschap schendt.
- Liveness (Levendigheid): Er gebeurt uiteindelijk iets goeds. Veiligheid alleen is niet genoeg; een systeem dat voor altijd niets doet, is immers perfect veilig. Daarom eisen we ook: $\Diamond$ (iemand is leider). Levendigheid vereist fairness-aannames, die uitvoeringen uitsluiten waarbij een actie voor altijd mogelijk blijft, maar simpelweg nooit wordt uitgevoerd. Weak fairness $\text{WF}(A)$ stelt dat een actie die consistent mogelijk blijft, uiteindelijk moet gebeuren; strong fairness $\text{SF}(A)$ geldt voor acties die oneindig vaak mogelijk worden.
Het mentale model is simpel: een TLA+-model beschrijft de mogelijke uitvoeringspaden van een systeem, en een eigenschap beschrijft welke paden acceptabel zijn. Verificatie stelt de vraag of elk mogelijk pad acceptabel is.
TLC, de standaard TLA+ model checker, beantwoordt dit door alle bereikbare toestanden voor een eindige instantie te enumereren. Een bewijs maakt de sterkere uitspraak dat de eigenschap in algemene zin geldt.
Wat TLA+ niet is
TLA+ wordt steeds vaker ingezet bij bedrijven als AWS, MongoDB en Datadog, en in projecten zoals Kafka. Er zijn echter drie belangrijke kanttekeningen waarbij TLA+ alleen onvoldoende is voor volledige softwareverificatie.
Model checking heeft grenzen. In de praktijk gebruiken mensen TLA+ meestal met TLC. TLC onderzoekt elke mogelijke run, maar alleen voor een eindig model. In ons voorbeeld groeit de toestandsruimte van 38 toestanden bij drie computers naar meer dan een miljoen bij negen computers. Om een eigenschap voor willekeurige systeemgroottes vast te stellen, is een bewijs nodig. De eigen prover van TLA+, TLAPS, kan dit in sommige gevallen doen, maar de automatisering is beperkt, vooral bij liveness-argumenten.
Het model is niet de implementatie. Een TLA+-specificatie is meestal een apart model van de software. Er is geen automatische garantie dat de implementatie zich exact gedraagt als het model; de twee kunnen uit elkaar groepen naarmate de code verandert. Dit is een element van de klassieke spec-to-implementation gap.
TLA+ kan niet elke eigenschap uitdrukken. TLA+ is gebaseerd op lineaire temporele logica (LTL), wat uitspraken doet over individuele uitvoeringen. Sommige interessante eigenschappen gaan echter over alternatieve toekomsten of strategieën:
- CTL (branching-time logic) kan uitspraken doen als: "vanuit elke toestand kan er nog steeds een nieuwe verkiezing worden gestart."
- ATL kan strategische uitspraken doen zoals: "deze computer heeft een strategie om leider te worden, ongeacht wat de anderen doen."
Deze rijkere eigenschappen worden relevant zodra we nadenken over systemen met meerdere concurrerende of collaborerende agenten. Een complete verificatiestack heeft dus meer nodig: sterkere bewijsmachines, een verbinding met echte code en uiteindelijk rijkere logica's.
Van TLA+ naar bewijzen
Een route is om het model over te brengen naar een modern bewijssysteem. Enkele opties zijn:
- Lean: Interactief; je (of een AI) schrijft het bewijs stap voor stap. Het is zeer algemeen, veel gebruikt in de wiskunde en was de prover in de post van Boris.
- Verus: Auto-actief en ontworpen rondom Rust. Je levert de specificaties en de belangrijke bewijsstructuur, terwijl een geautomatiseerde solver veel van de laagere redeneringen afhandelt.
- Veil: Een op Lean gebaseerde tool, specifiek gebouwd voor state-machine modellen. Het is onlangs gebruikt om een sync-engine te verifiëren, waarbij 17 bugs werden opgelost. Liveness is hier echter nog toekomstig werk en het geverifieerde model is nog steeds gescheiden van de implementatie.
Waarom Verus gebruiken? Omdat specificaties en bewijzen naast de echte Rust-implementatie kunnen leven. Dit biedt een route om de kloof tussen specificatie en implementatie te dichten: in plaats van alleen eigenschappen te bewijzen over een abstract model, kunnen we uiteindelijk bewijzen dat de implementatie dat model verfijnt (refines).
Het automatiseren van formele verificatie is aantrekkelijk omdat veel van het werk repetitief is:
- Safety-bewijzen zijn meestal inductief: toon aan dat de eigenschap initieel geldt en dat elke mogelijke actie deze behoudt.
- Liveness-bewijzen stellen vooruitgang vast: typically neemt een bepaalde hoeveelheid af naarmate het systeem vordert, in combinatie met fairness-aannames.
Het tracken van invarianten, het splitsen over acties en het invullen van details voor de solver maakt dit een natuurlijk doel voor bewijs-genererende agenten.
Van bewijzen naar machine-gecontroleerde software
Softwareverificatie vereist dat we eerst een nuttige beschrijving hebben van wat de software moet doen. TLA+ is hier aantrekkelijk omdat temporele specificaties compact en leesbaar zijn. Als we deze modellen kunnen verbinden met moderne bewijssystemen en implementaties, worden verschillende richtingen mogelijk:
- Verfijningsbewijzen (Refinement proofs): Bewijzen dat de Rust-implementatie het TLA+-model volgt. Automatisering hiervan verkleint de kloof tussen het verifiëren van een model en het verifiëren van de software.
- Programmasynthese: Starten vanuit het model en een implementatie genereren, samen met een bewijs dat de implementatie het model verfijnt.
- Protocolzoektocht (Protocol search): Wanneer het controleren van een kandidaat-protocol goedkoop genoeg is, kan de verifieerder dienen als objectieve functie om varianten van een protocol te genereren en te behouden die aan de gewenste eigenschappen voldoen.
- Voorbij lineaire tijd: Het uitdrukken van eigenschappen over alternatieve toekomsten of strategieën vereist logica's die verder gaan dan LTL.
Een voorproefje van onze voortgang
We hebben gewerkt aan een pijplijn voor het vertalen van TLA+-specificaties naar machine-gecontroleerde Verus-bewijzen. De belangrijkste resultaten tot nu toe zijn:
- Een TLA+ naar Verus transpiler: We hebben een algoritmische transpiler gebouwd en deze vergeleken met een agentisch alternatief (waarbij een LLM de vertaling maakt en een tweede LLM deze reviewt).
- Een prover–reviewer loop met anti-cheat checks: Eén agent schrijft een bewijs en een andere reviewt dit. Een aparte gatekeeper controleert of de agenten de specificatie niet hebben gewijzigd of shortcuts hebben geïntroduceerd zoals
assume(false).
- Een dataset van temporele bewijzen in Verus: Uitgaande van 16.459 echte TLA+-specificatie/eigenschap-paren, produceerde de pijplijn meer dan 3.000 machine-gecontroleerde safety- en liveness-bewijzen.
- Een evaluatie van huidige modellen: We hebben zowel gesloten als open-weight frontier-modellen getest op een evaluatieset om te zien welke temporele bewijzen ze kunnen voltooien.
***
Bronverwijzing
@misc{meszaros2026tlaplus,
author = {M{\'e}sz{\'a}ros, Anna and Ujv{\'a}ry, Szilvia and Strelbytska, Kseniia and Szil{\'a}gyi, Bal{\'a}zs and Husz{\'a}r, Ferenc},
title = {The internet discovers TLA+. Now what?},
howpublished = {\url{https://reasonable.io/blog/tla-tutorial/}},
year = {2026},
month = sept,
organization = {Reasonable},
note = {Reasonable blog post, accessed \today},
}
Het internet ontdekt TLA+. En nu?
De virale tweet van Boris Cherny liet zien hoe nuttig formele modellen kunnen zijn bij agentic coding. Dit artikel geeft een praktische introductie in wat TLA+ precies is.
TLA+ is echter slechts het startpunt. We kijken ook naar hoe temporele specificaties, moderne bewijssystemen en AI-agenten samen kunnen werken: van het modelleren van systeemgedrag tot het genereren van machine-gecontroleerde bewijzen, met als uiteindelijk doel software die in één cyclus wordt gespecificeerd, geïmplementeerd en geverifieerd. We geven daarnaast een inkijkje in het werk dat we bij Reasonable doen om dit mogelijk te maken.
Boris tweet, het internet kopieert
Deze week bracht Boris Cherny TLA+, een formele modellerings-toolkit die al meer dan 30 jaar oud is, terug in de schijnwerpers met een tweet. Hij gebruikte Opus 5.5 om delen van de Claude Agent SDK te modelleren in TLA+ en Lean. Het resultaat was typisch voor het internet: ongeveer een miljoen weergaven, duizenden bladwijzers en een golf van vragen over wat TLA+ nu eigenlijk is. De post van Boris is een uitstekende showcase en sluit aan bij eerdere voorbeelden die aantonen dat TLA+ de moeite waard is bij agentic coding (zie bijvoorbeeld de post van Datadog over harness-first agents).
Voor wie zich nu afvraagt wat TLA+ is en waarvoor het dient: TLA+ is een van de formele technieken waar ons team zich diep in heeft verdiept.
De reden waarom we dit belangrijk vinden, is dat TLA+ ons een compacte taal biedt om te definiëren wat een systeem mag doen en wat er altijd (of uiteindelijk) waar moet zijn. Dat is een nuttig startpunt voor verificatie, maar het is niet het eindpunt.
In het kort:
- TLA+ beschrijft mogelijke systeemgedragingen en de eigenschappen waaraan deze gedragingen moeten voldoen.
- TLA+ verifieert op zichzelf geen volledige implementatie. Het controleert een model van de software, niet de software zelf, en de belangrijkste model checker onderzoekt alleen eindige instanties.
- Moderne bewijssystemen kunnen ons verder brengen. In Verus kunnen specificatie, bewijs en de Rust-implementatie in dezelfde taal bestaan.
- AI kan delen van dit proces al automatiseren. We hebben een agentische pijplijn gebouwd die meer dan 16.000 TLA+-specificatie/eigenschap-paren heeft omgezet in meer dan 3.000 machine-gecontroleerde Verus-bewijzen.
De interessante vraag is dan ook niet alleen of een agent TLA+ kan schrijven, maar wat er mogelijk wordt zodra agenten kunnen schakelen tussen specificaties, bewijzen en echte programma's. Een deel van ons werk bij Reasonable is het trainen van modellen om agenten in staat te stellen dit consistent, betrouwbaar en snel te doen.
Wat TLA+ is
Stel je een scenario voor waarbij drie computers (a, b en c) het eens moeten worden over wie de leider is. Databases vertrouwen op een correcte leidersverkiezing. We stellen de eis dat er nooit twee leiders tegelijkertijd mogen bestaan.
TLA+ (Temporal Logic of Actions) is een taal voor het vastleggen van twee soorten objecten:
- Een overgangssysteem (transition system): Wat het systeem kan doen. Er zijn toestanden (states), die snapshots van het systeem zijn (wie is kandidaat, wie heeft op wie gestemd, wie is leider), en acties, wat enkelvoudige stappen zijn die een toestand veranderen ("a start een verkiezing", "b stemt op a").
- Temporele eigenschappen (temporal properties): Uitspraken over hoe een uitvoering zich in de loop van de tijd ontwikkelt. Bijvoorbeeld: "Er zijn nooit twee leiders" of "Er wordt uiteindelijk een leider gekozen."
Een TLA+-model definieert legale systeemtoestanden en toegestane overgangen tussen deze toestanden. Het legt geen volgorde op de overgangen en probeert de kansverdeling van verschillende gebeurtenissen niet te modelleren. Dit is de juiste abstractie voor gedistribueerde systemen, waar berichten, timeouts en gebruikersacties in veel verschillende volgordes kunnen voorkomen.
De onderliggende wiskunde is eenvoudig en maakt gebruik van verzamelingen, waar/onwaar-uitspraken en relaties. Temporele eigenschappen worden vervolgens opgebouwd uit operatoren over uitvoeringen:
- $\square P$ (altijd P): P geldt in elke bezochte toestand.
- $\Diamond P$ (uiteindelijk P): P geldt in een toekomstige toestand.
- $P \rightsquigarrow Q$ (P leidt tot Q): wanneer P geldt, geldt Q uiteindelijk daarna.
Er zijn twee soorten eigenschappen die bijzonder vaak van belang zijn:
- Safety (Veiligheid): Er gebeurt nooit iets slechts. Voor onze verkiezing: $\square$ (er zijn nooit twee leiders). De model checker onderzoekt elke mogelijke toestand en bevestigt de eigenschap. Als een regel wordt gewijzigd waardoor een computer twee keer kan stemmen, zal de checker een tegenvoorbeeld teruggeven: een concrete manier waarop het model de eigenschap schendt.
- Liveness (Levendigheid): Er gebeurt uiteindelijk iets goeds. Veiligheid alleen is niet genoeg; een systeem dat voor altijd niets doet, is immers perfect veilig. Daarom eisen we ook: $\Diamond$ (iemand is leider). Levendigheid vereist fairness-aannames, die uitvoeringen uitsluiten waarbij een actie voor altijd mogelijk blijft, maar simpelweg nooit wordt uitgevoerd. Weak fairness $\text{WF}(A)$ stelt dat een actie die consistent mogelijk blijft, uiteindelijk moet gebeuren; strong fairness $\text{SF}(A)$ geldt voor acties die oneindig vaak mogelijk worden.
Het mentale model is simpel: een TLA+-model beschrijft de mogelijke uitvoeringspaden van een systeem, en een eigenschap beschrijft welke paden acceptabel zijn. Verificatie stelt de vraag of elk mogelijk pad acceptabel is.
TLC, de standaard TLA+ model checker, beantwoordt dit door alle bereikbare toestanden voor een eindige instantie te enumereren. Een bewijs maakt de sterkere uitspraak dat de eigenschap in algemene zin geldt.
Wat TLA+ niet is
TLA+ wordt steeds vaker ingezet bij bedrijven als AWS, MongoDB en Datadog, en in projecten zoals Kafka. Er zijn echter drie belangrijke kanttekeningen waarbij TLA+ alleen onvoldoende is voor volledige softwareverificatie.
Model checking heeft grenzen. In de praktijk gebruiken mensen TLA+ meestal met TLC. TLC onderzoekt elke mogelijke run, maar alleen voor een eindig model. In ons voorbeeld groeit de toestandsruimte van 38 toestanden bij drie computers naar meer dan een miljoen bij negen computers. Om een eigenschap voor willekeurige systeemgroottes vast te stellen, is een bewijs nodig. De eigen prover van TLA+, TLAPS, kan dit in sommige gevallen doen, maar de automatisering is beperkt, vooral bij liveness-argumenten.
Het model is niet de implementatie. Een TLA+-specificatie is meestal een apart model van de software. Er is geen automatische garantie dat de implementatie zich exact gedraagt als het model; de twee kunnen uit elkaar groepen naarmate de code verandert. Dit is een element van de klassieke spec-to-implementation gap.
TLA+ kan niet elke eigenschap uitdrukken. TLA+ is gebaseerd op lineaire temporele logica (LTL), wat uitspraken doet over individuele uitvoeringen. Sommige interessante eigenschappen gaan echter over alternatieve toekomsten of strategieën:
- CTL (branching-time logic) kan uitspraken doen als: "vanuit elke toestand kan er nog steeds een nieuwe verkiezing worden gestart."
- ATL kan strategische uitspraken doen zoals: "deze computer heeft een strategie om leider te worden, ongeacht wat de anderen doen."
Deze rijkere eigenschappen worden relevant zodra we nadenken over systemen met meerdere concurrerende of collaborerende agenten. Een complete verificatiestack heeft dus meer nodig: sterkere bewijsmachines, een verbinding met echte code en uiteindelijk rijkere logica's.
Van TLA+ naar bewijzen
Een route is om het model over te brengen naar een modern bewijssysteem. Enkele opties zijn:
- Lean: Interactief; je (of een AI) schrijft het bewijs stap voor stap. Het is zeer algemeen, veel gebruikt in de wiskunde en was de prover in de post van Boris.
- Verus: Auto-actief en ontworpen rondom Rust. Je levert de specificaties en de belangrijke bewijsstructuur, terwijl een geautomatiseerde solver veel van de laagere redeneringen afhandelt.
- Veil: Een op Lean gebaseerde tool, specifiek gebouwd voor state-machine modellen. Het is onlangs gebruikt om een sync-engine te verifiëren, waarbij 17 bugs werden opgelost. Liveness is hier echter nog toekomstig werk en het geverifieerde model is nog steeds gescheiden van de implementatie.
Waarom Verus gebruiken? Omdat specificaties en bewijzen naast de echte Rust-implementatie kunnen leven. Dit biedt een route om de kloof tussen specificatie en implementatie te dichten: in plaats van alleen eigenschappen te bewijzen over een abstract model, kunnen we uiteindelijk bewijzen dat de implementatie dat model verfijnt (refines).
Het automatiseren van formele verificatie is aantrekkelijk omdat veel van het werk repetitief is:
- Safety-bewijzen zijn meestal inductief: toon aan dat de eigenschap initieel geldt en dat elke mogelijke actie deze behoudt.
- Liveness-bewijzen stellen vooruitgang vast: typically neemt een bepaalde hoeveelheid af naarmate het systeem vordert, in combinatie met fairness-aannames.
Het tracken van invarianten, het splitsen over acties en het invullen van details voor de solver maakt dit een natuurlijk doel voor bewijs-genererende agenten.
Van bewijzen naar machine-gecontroleerde software
Softwareverificatie vereist dat we eerst een nuttige beschrijving hebben van wat de software moet doen. TLA+ is hier aantrekkelijk omdat temporele specificaties compact en leesbaar zijn. Als we deze modellen kunnen verbinden met moderne bewijssystemen en implementaties, worden verschillende richtingen mogelijk:
- Verfijningsbewijzen (Refinement proofs): Bewijzen dat de Rust-implementatie het TLA+-model volgt. Automatisering hiervan verkleint de kloof tussen het verifiëren van een model en het verifiëren van de software.
- Programmasynthese: Starten vanuit het model en een implementatie genereren, samen met een bewijs dat de implementatie het model verfijnt.
- Protocolzoektocht (Protocol search): Wanneer het controleren van een kandidaat-protocol goedkoop genoeg is, kan de verifieerder dienen als objectieve functie om varianten van een protocol te genereren en te behouden die aan de gewenste eigenschappen voldoen.
- Voorbij lineaire tijd: Het uitdrukken van eigenschappen over alternatieve toekomsten of strategieën vereist logica's die verder gaan dan LTL.
Een voorproefje van onze voortgang
We hebben gewerkt aan een pijplijn voor het vertalen van TLA+-specificaties naar machine-gecontroleerde Verus-bewijzen. De belangrijkste resultaten tot nu toe zijn:
- Een TLA+ naar Verus transpiler: We hebben een algoritmische transpiler gebouwd en deze vergeleken met een agentisch alternatief (waarbij een LLM de vertaling maakt en een tweede LLM deze reviewt).
- Een prover–reviewer loop met anti-cheat checks: Eén agent schrijft een bewijs en een andere reviewt dit. Een aparte gatekeeper controleert of de agenten de specificatie niet hebben gewijzigd of shortcuts hebben geïntroduceerd zoals
assume(false).
- Een dataset van temporele bewijzen in Verus: Uitgaande van 16.459 echte TLA+-specificatie/eigenschap-paren, produceerde de pijplijn meer dan 3.000 machine-gecontroleerde safety- en liveness-bewijzen.
- Een evaluatie van huidige modellen: We hebben zowel gesloten als open-weight frontier-modellen getest op een evaluatieset om te zien welke temporele bewijzen ze kunnen voltooien.
***
Bronverwijzing
@misc{meszaros2026tlaplus,
author = {M{\'e}sz{\'a}ros, Anna and Ujv{\'a}ry, Szilvia and Strelbytska, Kseniia and Szil{\'a}gyi, Bal{\'a}zs and Husz{\'a}r, Ferenc},
title = {The internet discovers TLA+. Now what?},
howpublished = {\url{https://reasonable.io/blog/tla-tutorial/}},
year = {2026},
month = sept,
organization = {Reasonable},
note = {Reasonable blog post, accessed \today},
}
Groetjes,