Formelle specs er incident-værktøjer, ikke akademiske beviser

Der er et øjeblik i enhver reel incident, hvor rummet stopper med at tale om features og begynder at tale om tid.

Tid til at stoppe blødningen. Tid til at forstå, hvilken state systemet er i. Tid til at beslutte, om en genstart gør det bedre—eller blot øger blast radius. Tid til at svare på det ene spørgsmål, dit fremtidige jeg vil hade dig for at ignorere: “Hvis vi ikke gør noget, hvad sker der så som det næste?”

I det øjeblik bliver de fleste distribuerede systemer til en konkurrence i historiefortælling. Alle har en plausibel fortælling. Ingen af fortællingerne kan falsificeres hurtigt nok.

Derfor vender jeg igen og igen tilbage til formelle specifikationer. Ikke som en renhedstest. Som et incident-værktøj.

Hillel Wayne siger det klart i sin nylige samtale om formelle metoder: formelle metoder handler ikke kun om at bevise programmer korrekte—de handler om at gøre de kritiske dele af systemer præcise nok til, at man kan ræsonnere om dem. Den præcision er forskellen på “vi tror” og “vi ved”—især når systemet er distribueret, automatiseret og under load.

Det reelle problem er ikke bugs. Det er state, du ikke kan forklare.

De fleste teams ved allerede, hvordan man retter en bug. Du finder en repro, patcher og shipper. De svære problemer opstår, når systemet har flere writers, asynkront arbejde, retries, delvise fejl og timeouts, der interagerer.

Tilføj så agents.

Et agentic workflow er ikke bare kode, der kører. Det er kode, der beslutter sig—og derefter udfører handlinger, der skaber mere state. Hvis det kalder eksterne services, hvis det triggere betalinger, hvis det placerer ordrer, hvis det opdaterer kunders entitlements, bliver hver handling en del af en kæde, du senere kan blive nødt til at forsvare.

Når det går galt, er failure mode sjældent “det crashede”. Failure mode er “det fortsatte—men i den forkerte virkelighed”.

• To workers tror begge, at de ejer det samme job.
• Et retry gør en once-only handling til en at-least-once handling.
• Et menneske ser et dashboard, der er eventually consistent, og træffer en beslutning ud fra en ghost state.
• En agent læser forældet kontekst og udfører med stor selvtillid en valid handling på det forkerte tidspunkt.

Traditionel testning dækker det dårligt, fordi du ikke kan enumerere de interleavings, der betyder noget. Observability hjælper dig med at se, hvad der skete—men først bagefter. “Vi har logs” er ikke det samme som “vi har en model”.

Formelle specs, især TLA+, tvinger dig til at definere systemet som en state machine: hvilken state findes, hvilke transitions er tilladt, hvad skal altid være sandt. Det er ikke akademisk. Det er den eneste måde, jeg kender, der gør distribueret adfærd læsbar.

Determinisme er ikke en implementeringsdetalje. Det er et forretningskrav.

I trading- og payments-nære systemer er målet ikke “ingen incidents”. Målet er “afgrænset skade, forklarlige udfald og hurtig recovery”. Du kan leve med, at en komponent fejler. Du kan ikke leve med ikke at vide, hvad den gjorde.

Determinisme betyder i praksis fire ting:

1. Idempotence er eksplicit: du beslutter, hvilke handlinger der trygt kan gentages, og du koder nøglen, der gør dem sikre.
2. Ordering er intentionel: du vælger, hvor rækkefølge betyder noget (per konto, per portefølje, per kunde), og hvor den ikke gør.
3. Ownership er entydigt: ét sted beslutter, andre observerer. Hvis flere steder beslutter, modellerer du arbitration.
4. Invariants er ikke til forhandling: du definerer, hvad der aldrig må ske—selv under retries, backfills eller delvise outages.

Det er den samme mentale omstilling, der gør AI-systemer mere sikre. Ikke fordi AI er magi, men fordi det er probabilistisk. Hvis du lader probabilistiske komponenter skrive direkte ind i din finansielle sandhed eller dit system of record, mister du evnen til at replay’e og forsvare udfald. Læg dem i narrative layer, og hold truth layer deterministisk. (Den adskillelse er i familie med det, jeg argumenterede for i LLMs Belong in the Narrative Layer, Not in the Financial Truth Layer.)

Formelle specs ligger netop ved den grænse. De er en måde at fastlåse den deterministiske kerne og dens invariants, så resten af systemet kan være kreativt uden at være farligt.

Hvad TLA+ giver dig under incident-pres

Den mest undervurderede værdi ved TLA+ er ikke model checker’en. Det er den samtale, den tvinger frem.

Når du skriver en spec, har uklarhed ingen steder at gemme sig. Du kan ikke nøjes med at sige “workeren tager jobbet”. Du skal definere, hvornår det er eligible, hvem der kan claim’e det, og hvad der sker, hvis to workers prøver. Du kan ikke sige “vi reconcil’er senere”. Du skal definere reconciliation-transition’en og hvad den må ændre.

Under incident-pres betaler den præcision sig på tre konkrete måder:

• Auditability: du kan mappe observerede events tilbage til tilladte transitions. Hvis noget skete, som ikke findes i modellen, har du en reel defect—ikke et mysterium.
• Recoverability: du kan designe “repair moves” på forhånd. Backfill, replay, compensation og freeze paths er også transitions. Hvis du aldrig modellerede dem, improviserer du dem, når det er dyrest.
• Blast radius-kontrol: invariants fortæller dig, hvad du sikkert kan lempe—og hvad du skal beskytte for enhver pris. Den klarhed slår heroics.

Det matcher Waynes pointe om, at formelle metoder i stigende grad er praktiske, og at værktøjer som TLA+ bruges, fordi de hjælper teams med at ræsonnere om kompleks adfærd—ikke fordi de leverer perfekt software. Den pragmatiske framing er den, der betyder noget i en forretningskontekst. Du køber ikke sikkerhed. Du køber færre unknown unknowns. (Igen: se diskussionen.)

Et kendt mønster: incidenten hvor “vi kan ikke afgøre det” er den egentlige outage

Jeg har bygget trading-automation, hvor koden ikke var det skræmmende. Det skræmmende var den usynlige kontrakt mellem komponenter: hvem må handle, under hvilke forudsætninger, og hvordan vi ved, at en handling er endelig.

En type incident gentog sig på tværs af systemer og teams: systemet gjorde det, det lokalt var “tilladt” at gøre, men globalt brød det intentionen. Et retry fyrede efter en timeout, en acknowledgement kom for sent, to services var uenige om, hvorvidt en state transition var committed. Outagen var ikke downtime. Outagen var usikkerhed.

Når du ikke kan afgøre, om en state transition skete, kan du ikke fortsætte sikkert. Du fryser. Mennesker begynder at køre manuelle scripts. Folk foreslår at genstarte queues og redeploye services, fordi det er de eneste håndtag, de kan se. Imens fortsætter systemet med at drifte.

En formel spec ville ikke have forhindret alle fejl. Men den ville have gjort to ting umulige at overse:

• De præcise invariants, der definerer “korrekt nok” adfærd.
• De præcise transitions, der er sikre recovery-moves—inklusive hvilke der er forbudte.

Det er det, jeg mener, når jeg siger, at det er et incident-værktøj. Det reducerer fladen for improvisation.

Sådan adopterer du formelle specs uden at gøre det til teater

Du behøver ikke et virksomhedsdækkende program for formel verifikation. Du har brug for ét afgrænset sted, hvor uklarhed er dyrt.

Her er et mønster, der virker i rigtige teams:

1) Vælg ét “truth workflow” og tegn grænsen

Vælg et workflow, hvor forkert state er værre end downtime. Eksempler: entitlements, billing state, order lifecycle, porteføljepositioner, payouts, irreversible side effects.

Definér, hvad der ligger i den deterministiske kerne (state machine, invariants, transitions), og hvad der ligger udenfor (UI, analytics, agent reasoning, recommendation).

2) Skriv spec’en før næste rewrite—ikke efter incidenten

Specs skrevet post-mortem ender ofte som dokumentation. Specs skrevet før build bliver design.

Hold den lille. Hvis den er for stor til at model-check’e, er den for stor til at være nyttig som beslutningsværktøj.

3) Modellér failure moves som first-class transitions

De fleste systemer modellerer happy path og “håndterer så errors”. Det er ikke nok.

• Hvad betyder “freeze” i state-termer?
• Hvordan genoptager du uden at double-apply handlinger?
• Hvordan ser compensation ud—og hvad må den aldrig røre?

Det er samme mindset som bag AI-rollouts, der compounder: du laver en kontrolleret vej fra current reality til target reality, med reversibility hvor det er muligt. (Relateret: Build on the Stack You Have: The Rollout Pattern That Makes AI Compound.)

4) Gør invariants til runtime checks og runbooks

En spec, der lever i et repo men aldrig påvirker produktionsadfærd, bliver glemt.

Vælg 3 til 5 invariants og implementér dem som:

• Runtime assertions eller guards ved grænsefladerne.
• Alerts, der pager mennesker ved invariant-brud—ikke ved støjende symptomer.
• Runbook-trin, der refererer til invariant’en: hvad der skal tjekkes, hvad der skal fryses, hvad der skal replay’es.

5) Brug spec’en som governance for ændringer

Enhver ændring, der påvirker truth workflow’et, bør opdatere spec’en først. Det er en letvægtsform for change control, der ikke sænker teams—den forhindrer dyr tilbagegang.

Budgetoverskridelser i software kommer ofte af at bygge det forkerte to gange. Den samme dynamik gælder her: uklarhed er et cost center. (Hvis du vil have den bredere governance-vinkel, se Budget overruns are rarely a surprise. They are a governance choice.)

Min vurdering: AI fjerner ikke behovet for specs. Det øger prisen for ikke at have dem.

Der ligger en fristende idé under den nuværende AI-bølge: at modeller vil skrive koden, og måske endda verificere den. Wayne berører, om AI kan bringe formelle metoder ind i mainstream, og jeg er enig i retningen—men ikke i den dovne tolkning. (Se interviewet.)

Hvis AI gør det billigere at producere software, gør det det også billigere at producere subtile failure modes. Agentic systemer multiplicerer side effects. Distribuerede systemer multiplicerer interleavings. Sammen multiplicerer de antallet af plausible fortællinger under en outage.

Formelle specs er sådan, du holder én del af systemet kedelig. Deterministisk. Auditerbar. Recoverable. Det er ikke en luksus. Det er fundamentet, der lader dig bevæge dig hurtigt alle andre steder.

Brug TLA+ dér, hvor “vi kan ikke afgøre det” vil blive din værste incident. Hvis du ikke kan forklare state, ejer du ikke systemet.

Det er min holdning, og jeg har endnu ikke set et team fortryde at gøre truth workflow’et læsbart.