“Let's start with the obvious one: if you don't know how to represent your property as a logical formula, then TLA+ can't help you. Nor can any formal method.” https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/