Understanding the Boundaries of TLA+

A Reality Check on the Hype

Recently, Boris Cherny (the creator of Claude Code) noted that Opus successfully utilized TLA+ to identify race conditions within code. This has sparked a massive wave of internet enthusiasm regarding formal verification.

As someone who has spent years teaching and promoting TLA+, I find this interest thrilling. TLA+ is an exceptional tool for architecting intricate concurrent systems and ensuring they are devoid of bugs. However, as a proponent of ~~blind optimism~~ level-headedness, the current euphoria is concerning.

"The idea that formal methods will unilaterally solve the challenges of agentic software development is simply nonsense."

While many have already discussed how a perfect design doesn't guarantee perfect implementation code, I want to highlight a different constraint: To verify a property, you must first be able to define that property.

🛠️ What TLA+ Can Verify

TLA+ conceptualizes a system as a collection of behaviors. A behavior is essentially a linear sequence of states.

Visualizing a Behavior

In any given state, we use boolean expressions (e.g., "All lights are red"). To describe how these states evolve, TLA+ uses temporal logic operators:

Operator	Symbol	Meaning	Example
Always	$\square P$	$P$ is true now and in every future state.	$\square(\text{at\_most\_one\_green})$
Eventually	$\diamond P$	$P$ is true now or will be true at some point.	$\diamond(\text{light4} = \text{"yellow"})$
Leads To	$P \rightsquigarrow Q$	If $P$ happens, $Q$ must eventually follow.	$\text{Request} \rightsquigarrow \text{Response}$

Types of Properties

Invariants: When we check $\square P$ , we are asserting that $P$ holds for every state of every possible behavior.
Action Properties: These involve "primes" (the next state). For example, [](x' >= x) ensures a value never decreases.
Stability: [](P = P') means once $P$ becomes true, it stays true forever.
Liveness Properties: These ensure "something good eventually happens."
- $\square \diamond P$ : $P$ is true infinitely often (e.g., a system that always recovers).
- $\diamond \square P$ : Eventually, $P$ becomes true and stays true (e.g., an algorithm terminating).

Note: TLA+ also handles refinement (a mix of safety and liveness) and incorporates stutter-invariance to handle different levels of abstraction.

Verification Checklist

Safety Properties ("Nothing bad ever happens")
Liveness Properties ("Something good eventually happens")
State Invariants
Action-based transitions

⚠️ What TLA+ Cannot Verify

TLA+ is powerful, but it is not a magic wand. There are fundamental logical boundaries to what it can check.

1. The Formalization Gap

If you cannot translate a human requirement into a precise logical formula, TLA+ is useless.

Example: If you cannot mathematically define what a "bird" is, you cannot prove your software correctly identifies birds.

2. Multi-Step and Real-Time Constraints

TLA+ safety checks typically focus on a single state or a single transition. It cannot natively verify:

Multi-step sequences: e.g., "If I press Delete and then Undo, I should have my original data back."
Physical Time: TLA+ uses logical time (steps), not wall-clock time. You cannot prove a computer boots in "ten seconds."
Floating Point: It is not designed for floating-point arithmetic.

3. Existential vs. Universal Quantification

TLA+ properties are implicitly universal ( $\forall$ ). Checking $\square P$ means $P$ is true for all behaviors. It cannot natively check for the existence of a behavior.

\* TLA+ checks: "In ALL possible worlds, P is true."
\* TLA+ cannot check: "Is there AT LEAST ONE world where P is true?"

Consequently, you cannot use TLA+ to prove a game is winnable, as that requires proving a winning path exists.

4. Comparative Behavior Analysis

You cannot naturally compare two different behaviors within a single property check.

The Energy Mode Dilemma: Imagine verifying that "Energy Saving Mode" always consumes less power than "Normal Mode." To prove this, you would need to compare two separate behaviors:

$\text{Behavior}_A$ (Energy Saving)
$\text{Behavior}_B$ (Normal)

Since TLA+ evaluates properties against individual behaviors, it cannot inherently say "Behavior A is always more efficient than Behavior B" across all possible identical action sequences.

For those new to the field, I recommend exploring the introductory resources linked in the original text to get started with formal specifications.