TLA plus

Formal specification language created by person - Leslie Lamport for describing concurrent and distributed systems.

Key insight: math is the best way to describe distributed systems. TLA+ uses temporal logic to specify system behavior precisely enough that a model checker can exhaustively verify properties.

Used at Amazon, Microsoft, and others to find subtle bugs in distributed protocols that testing alone would miss.

Relevant here as an analogy: if math turned out to be the right formalism for distributed systems, what is the right formalism for software system specification in general? This is the question behind type-safe specification - 2026-02.