TLA+

/ˌtiː ɛl ˈeɪ plʌs/ · Noun · Development

Definitions

  1. A formal specification language created by Leslie Lamport for modeling and verifying concurrent and distributed systems, using temporal logic of actions to exhaustively check that a system design satisfies safety and liveness properties before any code is written — famously used at AWS to find subtle bugs in DynamoDB and S3.

    In plain English: A mathematical language for designing and checking complex systems on paper to prove they won't have certain kinds of bugs.

    Example: "We modeled the consensus protocol in TLA+ and the model checker found a livelock that no amount of code review would've caught."

Related Terms