What TLA+ can and can't check

TLA+ remains highly valuable for proving safety, invariants, and liveness properties in complex concurrent systems, but the article warns CIOs and technology leaders not to treat it as a silver bullet for AI or agentic software. Its strategic limitation is that it only checks properties that can be formalized and quantified across all behaviors, which means it cannot directly answer many business-critical questions such as reachability, multi-step user outcomes, real-time constraints, or whether a desirable state is merely possible—so IT teams still need strong requirements, architecture, and testing discipline alongside formal methods.