TLA+ is a formal verification tool excellent for designing concurrent systems and finding bugs, but it has a fundamental limitation: it can only verify properties that can be formally expressed. The article explains what TLA+ can check—invariants, safety properties, and liveness properties using temporal logic—while cautioning against overstating its ability to solve all problems in agentic software development.