Het artikel bespreekt de kracht en de grenzen van TLA+ (Temporal Logic of Actions), mede naar aanleiding van de hype rondom AI en formele verificatie.
De kernpunten zijn:
- Wat TLA+ kan: Het is uitmuntend in het controleren van safety properties (invarianten en actie-eigenschappen die garanderen dat er 'nooit iets slechts gebeurt') en liveness properties (die garanderen dat er 'uiteindelijk iets goeds gebeurt').
- Wat TLA+ niet kan: De taal kan geen eigenschappen verifiëren die niet logisch geformaliseerd kunnen worden, eigenschappen over meerdere stappen (zonder hacks), reële tijd, of bereikbaarheid (of een bepaalde toestand überhaupt mogelijk is).
- Geavanceerde beperkingen: TLA+ heeft moeite met hyper-eigenschappen (eigenschappen over sets van gedragingen, zoals beveiliging of statistiek) en metaproperties (eigenschappen over de gehele toestandsruimte).
- Workarounds: Hoewel technieken zoals hulpvariabelen en zelf-compositie sommige beperkingen kunnen omzeilen, worden deze beschouwd als 'hacks' die de complexiteit verhogen en de modellen onoverzichtelijk maken.
De auteur concludeert dat TLA+ zeer waardevol is voor het ontwerpen van concurrente systemen, maar geen universele oplossing is voor alle softwareproblemen.
Wat TLA+ kan en niet kan controleren
Vorige week noemde Boris Cherny, de uitvinder van Claude Code, dat Opus in staat was om TLA+ te gebruiken om race conditions in code te vinden. Sindsdien praat het hele internet over formele verificatie.
Als iemand die al lang TLA+ onderwijst en promoot, vind ik dit geweldig! TLA+ is uitmuntend in het ontwerpen van complexe concurrente systemen en het garanderen dat deze vrij zijn van bugs. Maar als iemand die ook houdt van nuchterheid, baart deze nieuwe euforie me zorgen. Ik lees veel mensen beweren dat formele methoden het probleem van agentic software development definitief zullen oplossen, en dat is onzin.
Er is al genoeg geschreven over de zwaktes van TLA+ wat betreft wat het kan garanderen, zoals het feit dat correcte ontwerpen niet automatisch vertalen naar correcte code. Daarom wil ik me in deze nieuwsbrief richten op een andere beperking: om een eigenschap te verifiëren, moeten we eerst een eigenschap hebben om te verifiëren! Dus welke eigenschappen kan TLA+ eigenlijk niet eens uitdrukken?
(Deze tekst gaat uit van basiskennis van TLA+.)
Wat TLA+ kan controleren
TLA+ verdeelt een systeem in een set van 'gedragingen' (behaviors). Elk gedrag is een reeks toestanden, zoals: "lamp één is groen, dan geel, dan rood". In elke toestand kunnen we reguliere booleaanse expressies uitdrukken, zoals "Lamp vier is groen" of "Alle lampen zijn rood". We kunnen deze expressies vervolgens aanpassen met drie "temporele" logische operatoren:
[]P ("altijd P"): is waar als P waar is in de huidige toestand en in elke toekomstige toestand. Voorbeeld: [](atmostone_green) is waar als elke toekomstige toestand maximaal één groen licht heeft.P' ("P prime"): is waar als P waar is in de volgende toestand. Voorbeeld: light="green" && light'="red" is waar als de lamp verandert van groen naar rood.<>P ("uiteindelijk P"): is waar als P waar is in de huidige toestand of in ten minste één toekomstige toestand. Voorbeeld: <>(light4 = "yellow") is waar als lamp 4 nu of in een toekomstige toestand geel is.
Wanneer we zeggen dat P een eigenschap van het systeem is, bedoelen we dat het waar is in de begintoestand van elk gedrag. Als we de eigenschap []P controleren, betekent dit dat []P waar is in elke begintoestand, en volgens de definitie van "altijd" betekent dit dat P waar is in elke toekomstige toestand vanaf die begintoestand. Dit houdt in dat het waar is in elke toestand van elk gedrag. We noemen dit een invariant, en dit is een van de meest fundamentele eigenschappen die we in TLA+ controleren.
We kunnen [] combineren met primes om actie-eigenschappen of change variants te krijgen. [](x' >= x) is waar als de nieuwe waarde van x altijd groter of gelijk is aan de oude waarde van x. Een ander voorbeeld is [](P => P'): zodra P waar is, kan het nooit meer onwaar worden. De werkelijke TLA+ is iets complexer vanwege iets dat "stutter-invariance" wordt genoemd, maar dat zijn details. Zowel actie-eigenschappen als invarianten zijn veiligheidseigenschappen (safety properties), wat grosso modo betekent: "er gebeurt nooit iets slechts".
Levendigheid (liveness), daarentegen, betekent: "er gebeurt altijd iets goeds". Alle liveness-eigenschappen zijn gebaseerd op <>. Op zichzelf betekent <>P alleen dat "P waar is in ten minste één toestand van elk gedrag", wat meestal te zwak is als systeemeigenschap. Door compositie kunnen we interessantere liveness-eigenschappen maken:
[]<>P: is waar als P in elke toestand uiteindelijk weer waar wordt in een toekomstige toestand. Dit kan herstelmechanismen representeren, zoals: "Als de nodes een nieuwe leiderschapsverkiezing houden, zullen ze uiteindelijk overeenstemming bereiken over een leider."<>[]P: is waar als P op een gegeven moment waar wordt en daarna voor altijd waar blijft. Dit is ideaal om aan te tonen dat algoritmen termineren met de correcte resultaten.[](P => <>Q): is waar als er voor elke toestand waarin P waar is, een toekomstige toestand is waarin Q waar is. Dit kan aantonen dat P uiteindelijk Q veroorzaakt, of dat "alle berichten die in de wachtrij worden geplaatst, uiteindelijk in de geschiedenis van een lezer terechtkomen". Omdat het parsen van deze formule verwarrend is, wordt de kortere notatie P ~> Q (P leidt tot Q) gebruikt.
Er zijn nog enkele andere operatoren, zoals ENABLED en <<A>>_v, maar het grootste deel van wat we controleren zijn invarianten, actie-eigenschappen en liveness. Daarnaast is er refinement, wat een combinatie is van veiligheid en levendigheid en een onderwerp op zich is.
Wat TLA+ niet kan
Laten we beginnen met het voor de hand liggende: als je niet weet hoe je een eigenschap moet representeren als een logische formule, dan kan TLA+ je niet helpen. Dat geldt voor elke formele methode. Als je het menselijke begrip van een "vogel" niet kunt formaliseren, kun je niet bewijzen dat je app vogels herkent. Helaas vallen veel belangrijke eigenschappen in deze categorie.
Vervolgens zijn er de zaken die te specifiek zijn. TLA+ veiligheidseigenschappen werken op het niveau van individuele toestanden (invarianten) of een enkele stap (actie-eigenschappen). Je kunt niet natievelijk een eigenschap definiëren over twee of meer stappen, zoals: "het indrukken van verwijderen en vervolgens ongedaan maken brengt je terug naar de oorspronkelijke staat", of "zodra de aan-knop wordt ingedrukt, start de computer binnen tien stappen op". Ook kunnen we geen eigenschappen definiëren voor floating-point operaties of over reële tijd, enkel over logische tijd.
Dan is er de beperking die mij het meest interesseert. TLA+ eigenschappen zijn impliciet gekwantificeerd over alle gedragingen. Ik zei dat het controleren van []P betekent dat "P waar is in elke toestand", maar wat het eigenlijk betekent is: "voor alle gedragingen is []P waar voor de begintoestand van dat gedrag". Elke eigenschap die TLA+ van een systeem kan controleren, moet een eigenschap zijn die waar is voor elk individueel gedrag.
Wat laat dat buiten? Veel meer dan je zou verwachten:
- Bereikbaarheid (Reachability): We kunnen niet zeggen: "er bestaat een gedrag waarin P waar is". We kunnen dus niet bewijzen dat P mogelijk is, zelfs als we het niet daadwerkelijk bereiken. Een voorbeeld hiervan is het bewijzen dat een spel winbaar is. Geavanceerdere bereikbaarheidseigenschappen zouden zijn: "P is bereikbaar vanuit elke begintoestand" of "P is bereikbaar vanuit elke toestand waarin Q waar is".
- Hyper-eigenschappen (Hyperproperties): We kunnen geen eigenschappen definiëren over een set van gedragingen. Stel dat we telefoonhardware modelleren en willen verifiëren dat de energiebesparingsmodus altijd minder energie verbruikt dan de normale modus. De eigenschap is: "elke reeks acties verbruikt in de energiebesparingsmodus niet meer stroom dan in de normale modus". Om dit te weerleggen, heb je twee gedragingen nodig die identiek zijn, behalve dat de één in energiebesparingsmodus start en de ander niet. Eén enkel gedrag is niet voldoende, dus is dit onmogelijk om natuurlijk in TLA+ te controleren. Hyper-eigenschappen lijken niche, maar ze dekken een groot deel van de beveiligingseigenschappen en alle statistische eigenschappen (bijv. "de 95ste percentiel responstijd is 5ms").
- Metaproperties: We kunnen geen eigenschappen definiëren over de toestandsruimte als geheel. We kunnen bijvoorbeeld niet zeggen dat er slechts één pad is van toestand X naar Y. Het is onduidelijk hoe nuttig dit in de praktijk zou zijn, maar deze "metaproperties" hebben potentieel.
Wat TLA+ "eigenlijk" kan
Ik heb het somewhat versimpeld door te zeggen dat TLA+ deze dingen niet kan. Ik bedoel dat als je een specificatie schrijft die direct correspondeert met het systeem dat je wilt bouwen, TLA+ deze zaken niet als eigenschappen van dat systeem kan uitdrukken.
Je kunt bepaalde dingen echter wel nabootsen:
- Hulpvariabelen (auxiliary variables): Je kunt eigenschappen over meerdere stappen simuleren door alle toestandsveranderingen op te slaan in een
state_history sequentie en de eigenschap te definiëren als een invariant op die sequentie.
- Zelf-compositie (self-composition): Je kunt sommige hyper-eigenschappen nabootsen waarbij elk gedrag van de zelf-gecomponeerde specificatie in feite twee gedragingen van het werkelijke systeem is.
- TLC-tools: De belangrijkste TLA+ model checker (TLC) kan de meest basale bereikbaarheidseigenschappen controleren met het nieuwe
REACHABLE trefwoord en sommige toestandsruimte-eigenschappen met TLCGet.
Dit zijn nuttige hacks, maar het blijven hacks. Elk van deze methoden vereist veel vindingrijkheid en brengt ernstige nadelen met zich mee. Hulpvariabelen verpesten refinements, zelf-compositie laat de toestandsruimte exponentieel groeien, enzovoort. Hacks combineren niet goed met andere TLA+ functies en dekken niet alle nuances van de eigenschappen die je wilt uitdrukken. Bovendien zorgen ze ervoor dat je modellen er vreemd en rommelig uitzien en niet meer overeenkomen met je werkelijke systemen.
Je zou ook een andere tool kunnen gebruiken met een andere focus. CTL kan bereikbaarheidseigenschappen controleren, PRISM kan probabilistische eigenschappen controleren, etc. Zij maken een afweging door minder goed te zijn in de zaken waar TLA+ juist in uitblinkt, en natuurlijk kan geen van hen eigenschappen afhandelen die we logisch niet kunnen uitdrukken.
Uiteindelijk is TLA+ erg goed in het plukken van de "laaghangende vruchten": invarianten en liveness dekken veel zaken die ons interesseren, en TLA+ is redelijk goed in het uitdrukken en controleren daarvan. Er zit veel potentieel (en veel valkuilen) in het gebruik van TLA+ om "vibe code" te controleren. Maar er zijn ook veel zaken die het niet eens kan uitdrukken, laat staan controleren.
***
Voetnoten:
- "Temporal logic of actions". Het is een specificatietaal die wordt gebruikt om bugs in concurrente systemen te vinden.
- (En wat betreft de vraag waarom iemand die zo evangelisch is over formele methoden bij een testbedrijf is gegaan: daar zou binnenkort een artikel over op hun blog verschijnen.)
Wat TLA+ kan en niet kan controleren
Vorige week noemde Boris Cherny, de uitvinder van Claude Code, dat Opus in staat was om TLA+ te gebruiken om race conditions in code te vinden. Sindsdien praat het hele internet over formele verificatie.
Als iemand die al lang TLA+ onderwijst en promoot, vind ik dit geweldig! TLA+ is uitmuntend in het ontwerpen van complexe concurrente systemen en het garanderen dat deze vrij zijn van bugs. Maar als iemand die ook houdt van nuchterheid, baart deze nieuwe euforie me zorgen. Ik lees veel mensen beweren dat formele methoden het probleem van agentic software development definitief zullen oplossen, en dat is onzin.
Er is al genoeg geschreven over de zwaktes van TLA+ wat betreft wat het kan garanderen, zoals het feit dat correcte ontwerpen niet automatisch vertalen naar correcte code. Daarom wil ik me in deze nieuwsbrief richten op een andere beperking: om een eigenschap te verifiëren, moeten we eerst een eigenschap hebben om te verifiëren! Dus welke eigenschappen kan TLA+ eigenlijk niet eens uitdrukken?
(Deze tekst gaat uit van basiskennis van TLA+.)
Wat TLA+ kan controleren
TLA+ verdeelt een systeem in een set van 'gedragingen' (behaviors). Elk gedrag is een reeks toestanden, zoals: "lamp één is groen, dan geel, dan rood". In elke toestand kunnen we reguliere booleaanse expressies uitdrukken, zoals "Lamp vier is groen" of "Alle lampen zijn rood". We kunnen deze expressies vervolgens aanpassen met drie "temporele" logische operatoren:
[]P ("altijd P"): is waar als P waar is in de huidige toestand en in elke toekomstige toestand. Voorbeeld: [](atmostone_green) is waar als elke toekomstige toestand maximaal één groen licht heeft.P' ("P prime"): is waar als P waar is in de volgende toestand. Voorbeeld: light="green" && light'="red" is waar als de lamp verandert van groen naar rood.<>P ("uiteindelijk P"): is waar als P waar is in de huidige toestand of in ten minste één toekomstige toestand. Voorbeeld: <>(light4 = "yellow") is waar als lamp 4 nu of in een toekomstige toestand geel is.
Wanneer we zeggen dat P een eigenschap van het systeem is, bedoelen we dat het waar is in de begintoestand van elk gedrag. Als we de eigenschap []P controleren, betekent dit dat []P waar is in elke begintoestand, en volgens de definitie van "altijd" betekent dit dat P waar is in elke toekomstige toestand vanaf die begintoestand. Dit houdt in dat het waar is in elke toestand van elk gedrag. We noemen dit een invariant, en dit is een van de meest fundamentele eigenschappen die we in TLA+ controleren.
We kunnen [] combineren met primes om actie-eigenschappen of change variants te krijgen. [](x' >= x) is waar als de nieuwe waarde van x altijd groter of gelijk is aan de oude waarde van x. Een ander voorbeeld is [](P => P'): zodra P waar is, kan het nooit meer onwaar worden. De werkelijke TLA+ is iets complexer vanwege iets dat "stutter-invariance" wordt genoemd, maar dat zijn details. Zowel actie-eigenschappen als invarianten zijn veiligheidseigenschappen (safety properties), wat grosso modo betekent: "er gebeurt nooit iets slechts".
Levendigheid (liveness), daarentegen, betekent: "er gebeurt altijd iets goeds". Alle liveness-eigenschappen zijn gebaseerd op <>. Op zichzelf betekent <>P alleen dat "P waar is in ten minste één toestand van elk gedrag", wat meestal te zwak is als systeemeigenschap. Door compositie kunnen we interessantere liveness-eigenschappen maken:
[]<>P: is waar als P in elke toestand uiteindelijk weer waar wordt in een toekomstige toestand. Dit kan herstelmechanismen representeren, zoals: "Als de nodes een nieuwe leiderschapsverkiezing houden, zullen ze uiteindelijk overeenstemming bereiken over een leider."<>[]P: is waar als P op een gegeven moment waar wordt en daarna voor altijd waar blijft. Dit is ideaal om aan te tonen dat algoritmen termineren met de correcte resultaten.[](P => <>Q): is waar als er voor elke toestand waarin P waar is, een toekomstige toestand is waarin Q waar is. Dit kan aantonen dat P uiteindelijk Q veroorzaakt, of dat "alle berichten die in de wachtrij worden geplaatst, uiteindelijk in de geschiedenis van een lezer terechtkomen". Omdat het parsen van deze formule verwarrend is, wordt de kortere notatie P ~> Q (P leidt tot Q) gebruikt.
Er zijn nog enkele andere operatoren, zoals ENABLED en <<A>>_v, maar het grootste deel van wat we controleren zijn invarianten, actie-eigenschappen en liveness. Daarnaast is er refinement, wat een combinatie is van veiligheid en levendigheid en een onderwerp op zich is.
Wat TLA+ niet kan
Laten we beginnen met het voor de hand liggende: als je niet weet hoe je een eigenschap moet representeren als een logische formule, dan kan TLA+ je niet helpen. Dat geldt voor elke formele methode. Als je het menselijke begrip van een "vogel" niet kunt formaliseren, kun je niet bewijzen dat je app vogels herkent. Helaas vallen veel belangrijke eigenschappen in deze categorie.
Vervolgens zijn er de zaken die te specifiek zijn. TLA+ veiligheidseigenschappen werken op het niveau van individuele toestanden (invarianten) of een enkele stap (actie-eigenschappen). Je kunt niet natievelijk een eigenschap definiëren over twee of meer stappen, zoals: "het indrukken van verwijderen en vervolgens ongedaan maken brengt je terug naar de oorspronkelijke staat", of "zodra de aan-knop wordt ingedrukt, start de computer binnen tien stappen op". Ook kunnen we geen eigenschappen definiëren voor floating-point operaties of over reële tijd, enkel over logische tijd.
Dan is er de beperking die mij het meest interesseert. TLA+ eigenschappen zijn impliciet gekwantificeerd over alle gedragingen. Ik zei dat het controleren van []P betekent dat "P waar is in elke toestand", maar wat het eigenlijk betekent is: "voor alle gedragingen is []P waar voor de begintoestand van dat gedrag". Elke eigenschap die TLA+ van een systeem kan controleren, moet een eigenschap zijn die waar is voor elk individueel gedrag.
Wat laat dat buiten? Veel meer dan je zou verwachten:
- Bereikbaarheid (Reachability): We kunnen niet zeggen: "er bestaat een gedrag waarin P waar is". We kunnen dus niet bewijzen dat P mogelijk is, zelfs als we het niet daadwerkelijk bereiken. Een voorbeeld hiervan is het bewijzen dat een spel winbaar is. Geavanceerdere bereikbaarheidseigenschappen zouden zijn: "P is bereikbaar vanuit elke begintoestand" of "P is bereikbaar vanuit elke toestand waarin Q waar is".
- Hyper-eigenschappen (Hyperproperties): We kunnen geen eigenschappen definiëren over een set van gedragingen. Stel dat we telefoonhardware modelleren en willen verifiëren dat de energiebesparingsmodus altijd minder energie verbruikt dan de normale modus. De eigenschap is: "elke reeks acties verbruikt in de energiebesparingsmodus niet meer stroom dan in de normale modus". Om dit te weerleggen, heb je twee gedragingen nodig die identiek zijn, behalve dat de één in energiebesparingsmodus start en de ander niet. Eén enkel gedrag is niet voldoende, dus is dit onmogelijk om natuurlijk in TLA+ te controleren. Hyper-eigenschappen lijken niche, maar ze dekken een groot deel van de beveiligingseigenschappen en alle statistische eigenschappen (bijv. "de 95ste percentiel responstijd is 5ms").
- Metaproperties: We kunnen geen eigenschappen definiëren over de toestandsruimte als geheel. We kunnen bijvoorbeeld niet zeggen dat er slechts één pad is van toestand X naar Y. Het is onduidelijk hoe nuttig dit in de praktijk zou zijn, maar deze "metaproperties" hebben potentieel.
Wat TLA+ "eigenlijk" kan
Ik heb het somewhat versimpeld door te zeggen dat TLA+ deze dingen niet kan. Ik bedoel dat als je een specificatie schrijft die direct correspondeert met het systeem dat je wilt bouwen, TLA+ deze zaken niet als eigenschappen van dat systeem kan uitdrukken.
Je kunt bepaalde dingen echter wel nabootsen:
- Hulpvariabelen (auxiliary variables): Je kunt eigenschappen over meerdere stappen simuleren door alle toestandsveranderingen op te slaan in een
state_history sequentie en de eigenschap te definiëren als een invariant op die sequentie.
- Zelf-compositie (self-composition): Je kunt sommige hyper-eigenschappen nabootsen waarbij elk gedrag van de zelf-gecomponeerde specificatie in feite twee gedragingen van het werkelijke systeem is.
- TLC-tools: De belangrijkste TLA+ model checker (TLC) kan de meest basale bereikbaarheidseigenschappen controleren met het nieuwe
REACHABLE trefwoord en sommige toestandsruimte-eigenschappen met TLCGet.
Dit zijn nuttige hacks, maar het blijven hacks. Elk van deze methoden vereist veel vindingrijkheid en brengt ernstige nadelen met zich mee. Hulpvariabelen verpesten refinements, zelf-compositie laat de toestandsruimte exponentieel groeien, enzovoort. Hacks combineren niet goed met andere TLA+ functies en dekken niet alle nuances van de eigenschappen die je wilt uitdrukken. Bovendien zorgen ze ervoor dat je modellen er vreemd en rommelig uitzien en niet meer overeenkomen met je werkelijke systemen.
Je zou ook een andere tool kunnen gebruiken met een andere focus. CTL kan bereikbaarheidseigenschappen controleren, PRISM kan probabilistische eigenschappen controleren, etc. Zij maken een afweging door minder goed te zijn in de zaken waar TLA+ juist in uitblinkt, en natuurlijk kan geen van hen eigenschappen afhandelen die we logisch niet kunnen uitdrukken.
Uiteindelijk is TLA+ erg goed in het plukken van de "laaghangende vruchten": invarianten en liveness dekken veel zaken die ons interesseren, en TLA+ is redelijk goed in het uitdrukken en controleren daarvan. Er zit veel potentieel (en veel valkuilen) in het gebruik van TLA+ om "vibe code" te controleren. Maar er zijn ook veel zaken die het niet eens kan uitdrukken, laat staan controleren.
***
Voetnoten:
- "Temporal logic of actions". Het is een specificatietaal die wordt gebruikt om bugs in concurrente systemen te vinden.
- (En wat betreft de vraag waarom iemand die zo evangelisch is over formele methoden bij een testbedrijf is gegaan: daar zou binnenkort een artikel over op hun blog verschijnen.)
Groetjes,