TLA+
Leslie Lamports formell specifikationsspråk för konkurrenta system — beskriv vad systemet ska göra, model-checkern verifierar att det inte kan hamna i ogiltigt state.
Bygger på temporal logic of actions. TLC = model checker som uttömmande utforskar alla möjliga state-transitioner. Amazon Web Services använder det för design av S3, DynamoDB, EBS — fann buggar i designen innan implementation. MongoDB, Cosmos DB, Microsoft Azure också. Branta inlärningskurva — Lamport själv skriver lärobokin (Specifying Systems). Apalache är en konkurrent-checker. PlusCal är pseudo-code-syntax som transpileras till TLA+.