What TLA+ can and can't check

TLA+ is an effective tool for verifying properties in complex concurrent systems, but recent enthusiasm about its ability to solve problems in AI development overstates its capabilities. The key limitation is that TLA+ can only verify properties that are explicitly defined—it cannot express or check properties that designers fail to specify in the first place. While TLA+ excels at checking safety properties like invariants and action properties, it cannot automatically discover what properties should be verified or guarantee that correct designs will translate into correct code.