Last week Boris Cherny, the inventor of Claude Code, mentioned that Opus was able to use TLA+ to find race conditions in code. Now everybody is talking about formal verification. As a long-time educator and advocate of TLA+, this is exciting. But the new euphoria worries me. Formal methods will not solve agentic software development once and for all.

Correct designs don't automatically translate into correct code. To verify a property, we need a property to verify. TLA+ divides the system into behaviors, each a sequence of states. In each state we can express boolean expressions with three temporal operators: `[]P` (always P), `P'` (P in the next state), and `<>P` (eventually P).

`[]P` means P is true in every state of every behavior, called an invariant. `[](x' >= x)` is an action property. These are safety properties: something bad never happens. Liveness properties use `<>`: `[]<>P` means P is true in at least one future state of every state; `<>[]P` means P becomes true and stays true forever; `[](P => <>Q)` means P eventually causes Q.