Two Correct Termination Proofs Compose Into a Hang

Mostafa Dhouib·September 5, 2026·7 min read

Two Correct Termination Proofs Compose Into a Hang

The short answer. Termination does not compose. A planner that provably stops and an executor that provably stops can, wired into a loop, run forever, and both original proofs remain valid throughout. This is not an implementation bug, it is a property of the mathematics, which is why every component's dashboard can be green while the system hangs. Podelski and Rybalchenko's 2004 transition invariant work gives the correct shape of a proof for the composed system: you need a measure over the combined state, and no amount of per-component measure adds up to one.

Here is a system that fails in a way nobody's monitoring can see.

A planner takes a goal and emits a list of steps. It has a bound: at most twenty steps per plan, and it always returns. Proven, tested, correct.

An executor takes a step and runs it. It has a bound: at most ten tool calls per step, and it always returns. Proven, tested, correct.

The executor reports back to the planner. If a step failed, the planner replans.

Every component provably terminates. The system does not.

Why this is not a bug you can find by reading the code

The instinct on hearing this is that somebody made a mistake, that one of the proofs is subtly wrong, that there is an off-by-one somewhere. There is not. Both proofs are correct statements about their components, and they remain correct while the system hangs.

The reason is a property of termination arguments generally, and it is worth stating precisely because the precision is what makes it actionable.

A termination proof is a ranking function: a value computed from the program's state, which strictly decreases every pass and cannot decrease forever because it is bounded below. Floyd formalised this in 1967. Steps-remaining is a ranking function for the planner. Calls-remaining is a ranking function for the executor.

Now compose them. On a replan, the planner's counter resets to twenty. On a new step, the executor's counter resets to ten. Neither ranking function decreases across the composed loop, because each is reset by the other's activity.

So the composed system has no ranking function, which means it has no termination proof, which means it need not terminate. The two proofs did not add up to a third proof. They were never the kind of thing that adds up.

The correct shape of the argument

Podelski and Rybalchenko's 2004 result on transition invariants is the standard reference here, and the useful part for engineering is the shape rather than the formalism.

The idea is that instead of demanding a single global ranking function, you argue about the transition relation of the whole system: every possible way it can move from one state to a later one must be covered by one of a finite set of well-founded relations. It makes termination proofs for looping, mutually recursive systems tractable, and there are tools that automate it.

For our purposes the engineering translation is short:

The measure has to be over the combined state. Not the planner's state, not the executor's state, but something computed from both, which no component resets and which strictly decreases as the system moves forward.

A measure that any component can reset is not a measure. This is the whole failure in one line, and it is a check you can apply to a design in about a minute.

What such a measure looks like in practice

The good news is that for real tasks this measure is usually available and usually boring, which is why it gets skipped rather than being genuinely hard.

Rows unmigrated. Not attempts made. Rows that still need to move. Nothing in the planner or executor can reset it, and it hits zero when the job is done.

Tests still failing. Not fix attempts. The count of failing tests. A replan does not change it. Running a step might.

Records unmatched, tickets unresolved, files unprocessed, fields still empty. The pattern is the same: a count of remaining work, computed in code from ground truth, that no control-flow event can restore.

The tell that you have the wrong measure is that it goes up when the system does something. Attempts, iterations, tokens, calls, elapsed time: these all measure spend. Spend is bounded and worth bounding, but a fuel gauge cannot distinguish arriving from running dry, and that distinction is exactly the one a composed system loses.

Why your monitoring is structurally blind to this

This is the operational consequence and it is the reason the failure survives in production for weeks.

Per-component monitoring answers per-component questions. Did the planner return? Yes, in four seconds. Did the executor return? Yes, in eleven seconds. Error rate? Zero. Timeouts? None. Every dashboard is green and every dashboard is honest.

The hang lives in the relationship between the components, and there is no component whose metrics contain it. You cannot fix this by adding more per-component metrics, however many you add, for the same reason you cannot find the seam by looking harder at either side of it.

What you need is one metric at the level of the task:

Time since the remaining-work measure last decreased. Not time since the last activity, which is always near zero in a hung system because the components are busy. Time since actual progress.

That single number distinguishes a system doing hard work slowly from a system doing nothing energetically, and almost nobody has it. It is the sensor placed at the level the failure occurs at, which is the general form of the fix.

The same shape in three other systems

Once you know composition is where this hides, you find it outside AI immediately.

Retry loops around retry loops. An HTTP client retries three times. The service calling it retries three times. The job scheduler retries three times. Each bound is real; the composition is twenty-seven attempts, and if a fourth layer exists nobody can say what the total is without drawing it out.

Mutually recursive workflow steps. Step A escalates to step B on failure; step B routes back to A when it cannot resolve. Both have bounds per invocation. The pair can ping-pong indefinitely and every invocation is inside its limit.

Cache invalidation cycles. Service A invalidates B's cache, B recomputes and invalidates A's. Each operation terminates. The pair can chase each other for as long as traffic keeps arriving.

In every case the fix has the same form: find the quantity that represents actual progress toward the outcome, verify no participant can reset it, and bound the system on that.

The review question

Ask of any multi-component loop: what decreases across the whole system, and can any component reset it?

If nobody can answer the first half, the system has no termination proof regardless of how many its components have. If the answer to the second half is yes, you have found the hang before it shipped.

FAQ

Why does my agent hang when every component terminates? Because termination does not compose. Each component's ranking function is reset by the other component's activity, so the composed loop has no decreasing measure and therefore no termination proof. Both original proofs stay valid the entire time the system is hung.

What is a ranking function? A value computed from program state that strictly decreases on every pass and is bounded below, so it cannot decrease forever. Floyd formalised it in 1967 and it is the standard way to prove a loop terminates. Steps-remaining and calls-remaining are both ranking functions for their own components.

What are transition invariants? Podelski and Rybalchenko's 2004 approach to proving termination for systems where a single global ranking function is hard to find. Instead of one measure, you cover every way the system can move forward with a finite set of well-founded relations. The engineering takeaway is that the argument must be over the combined state.

Why doesn't per-component monitoring catch this? Because the hang lives in the relationship between components, and no component's metrics contain it. Both return promptly, error rates are zero, and every dashboard is honest. The metric you need is at task level: time since the remaining-work measure last decreased.

What measure should I use instead of an iteration count? A count of remaining work computed in code from ground truth: rows unmigrated, tests still failing, records unmatched. The test is that it must shrink as the task nears completion and that no component can reset it. If it goes up when the system does something, it is measuring spend rather than progress.