software testing

TLA+ is a formal specification language. TLA+ is used to design, model, and verify concurrent systems. TLA+ allows a user to describe a system formally with simple, precise mathematics.

Automation is changing the labor market. To automate a task, someone needs to put in the work to describe the task correctly to a computer. For some tasks, the reward for automating a