TLA+ is a formal specification language used to model software systems. We can take the specification and check if it satisfies the properties we want, or produce a counterexample if it doesn’t. TLA+ is exceptionally well-suited for specifying concurrent and distributed systems, everything from kernel spinlocks to communicating microservices.
