Tagged ai-agents
3 pieces
- · 7 min read
Two Correct Termination Proofs Compose Into a Hang
Your planner stops. Your executor stops. Both proofs are valid and neither is wrong. Put them in a loop together and the system runs forever, because termination is not a property that composes. Podelski and Rybalchenko formalised the fix in 2004, and it explains exactly why per-component monitoring cannot see a hang that lives between components.
- · 8 min read
The Verifier That Verifies Nothing
Naming a pipeline stage 'verifier' does not make it one. If the stage is another model call asked whether the output looks right, it shares the generator's blind spots, produces an opinion rather than a check, and has almost certainly never rejected anything. There is a ladder of verifier strength with five rungs, and most production systems are on the bottom one while believing they are near the top.
- · 7 min read
The Five Ways a Loop Fails to Stop
Floyd gave us the conditions a terminating loop has to satisfy in 1967. Negate them one at a time and you get an exhaustive list of the ways termination can fail, which turns a vague symptom into five named diagnoses with five different fixes. Your agent is almost certainly number four, and number four is the only one that looks like success.