TLA+
Język formalnej specyfikacji systemów współbieżnych autorstwa Leslie Lamporta — opisujesz, co system ma robić, a model checker sprawdza, że nie trafi w niedozwolony stan.
Oparty na temporalnej logice akcji. TLC to model checker, który wyczerpująco przeszukuje wszystkie możliwe przejścia stanów. Amazon Web Services używa go przy projektowaniu S3, DynamoDB i EBS — znajdował błędy projektowe przed implementacją. Korzystają też MongoDB, Cosmos DB i Microsoft Azure. Krzywa uczenia jest stroma — Lamport sam napisał podręcznik (Specifying Systems). Konkurencyjny checker to Apalache. PlusCal to składnia w stylu pseudokodu, transpilowana do TLA+.