Definition
Plain language
A formal language for precisely describing concurrent systems and checking them for bugs.
As stated in the literature
A formal specification language developed by Leslie Lamport for describing and verifying concurrent and distributed systems, paired with the TLC model checker.
Also called: TLC
Why it matters: It catches subtle concurrency bugs that traditional testing almost always misses, which is why it's used on critical distributed systems at Amazon and Microsoft.
For example, an engineer can write a TLA+ spec of a distributed lock and have a model checker explore every interleaving to confirm no two clients can hold it at once.
Heard on the show
“The checker is called TLC.”Episode 034 — Catching Multi-Agent Deadlocks Before Deployment With a 40-Year-Old Tool