THE LIMITS OF WHAT TLA+ CAN VERIFY

Summary from the TLDR newsletter

TLA+ cannot express possibility and reachability properties, hyperproperties, statistical properties, and properties about whether a system is robust against code changes.