What TLA+ Can and Can’t Check
TLA+ can check invariants, step-by-step safety properties, and liveness—but only after a property has been made precise. This article is a useful counterweight to claims that formal methods can automatically validate agent-written software: some important claims, including “this state is reachable” or comparisons across multiple executions, are not directly expressible as ordinary properties of one TLA+ behavior.
The article explains that reachability can sometimes be approximated with TLC’s REACHABLE support or auxiliary variables, and some multi-run properties with self-composition. Those techniques have limits: auxiliary variables complicate refinement, and self-composition can make the state space explode. The point is not that TLA+ is weak—it is effective for many concurrency invariants and liveness questions—but that a model only checks the properties its author can formulate.
The sole Lobsters commenter, TLA+ expert Andrew Helwer, agreed that some properties are technically expressible but awkward to state, and wondered whether making them ergonomic would introduce trade-offs with the logic itself.