The hype about ChatGPT brings AI to the attention of a wider audience. It might even seem that AI has now reached a level in which many tasks that we originally thought to be in the human domain and not in the machine domain might be taken away from us. But is that really true?
TLA+ is a modeling language in which one can model technical systems with discrete states. It has been used to describe many things, from the jugs problem in Die Hard 3 over a diverse array of algorithms up to Amazon Storage Services. The power of TLA+ comes from the TLC Model Checker, which checks your model for certain properties. These properties could be invariants — statements that are true of every possible state, like there are no buffer overruns. And it can check temporal properties — e.g., that an algorithm eventually finishes.
