Summary
The plan agent can rewrite PROGRESS.md in a format that archon-loop.sh's parse_objective_files() cannot parse, causing prover dispatch to silently fail. Neither the plan agent nor the review agent receives this error, so the system loops indefinitely without self-correcting. In our run, this wasted 9 iterations, ~163 minutes of wall time, and ~$28 in API costs with zero progress.
Root Cause
parse_objective_files() in archon-loop.sh (line 173-187) requires a ## Current Objectives section to extract target .lean files:
awk '
/^## Current Objectives/ { found=1; next }
found && /^## / { exit }
found { print }
' "$PROGRESS_FILE"After a productive prover iteration, the plan agent rewrote PROGRESS.md using ## Strategy instead of ## Current Objectives. The file still listed per-file objectives under ### N. **File.lean** sub-headings, but since the parent heading was wrong, parsing returned empty.
Before (productive iteration, worked):
## Current Objectives
Fill all sorry proofs across 9 files...
### 1. **Common/FileA.lean** — Fix compile error + fill 4 sorries
...
After (next iteration's plan agent, broken):
## Strategy
Previous iteration revealed that almost all remaining sorries trace to infrastructure gaps...
### 1. **Common/FileA.lean** — Enrich type classes + fill sorries
...
The Feedback Loop Failure
The shell orchestrator logged a warning every iteration:
{"event":"shell","level":"warn","message":"No files parsed from PROGRESS.md ## Current Objectives."}This warning appeared in all 9 broken iterations. However:
-
Plan agent couldn't see the warning — it was logged to the JSONL file but never injected into the plan agent's prompt. The plan agent had no way of knowing its own PROGRESS.md was being rejected by the shell parser.
-
Review agent misdiagnosed the problem — the review agent observed "zero edits, zero sorry reduction" across consecutive sessions, but attributed it to mathematical strategy exhaustion ("replay loop — same targets assigned, same strategies exhausted"). It recommended the plan agent switch to infrastructure-building tasks. It never identified the real cause: that provers were not being launched at all due to a heading format mismatch. The review agent's recommendations were mathematically sound but addressed the wrong problem entirely.
-
Plan agent faithfully followed the wrong diagnosis — it read the review's recommendations, adopted the infrastructure-building strategy, carefully restructured its objectives — and then wrote PROGRESS.md with ## Strategy again (still without ## Current Objectives). By iteration 17, the plan agent explicitly stated: "The plan is mature and actionable. The system needs to execute it." — blaming infrastructure rather than its own output format.
In short: the review agent never realized the problem was in PROGRESS.md's heading format; the plan agent never received the shell-level error; and both agents spent 9 iterations optimizing mathematical strategy while the actual failure was a one-line format mismatch invisible to both of them.
Impact
| Metric |
Value |
| Iterations wasted |
9 (iter-012 through iter-020) |
| Wall time wasted |
~163 minutes |
| API cost wasted |
~$28 |
| Sorry resolved |
0 |
| Plan agent re-analyzed state uselessly |
9 times |
| Review agent ran uselessly |
9 times |
Suggested Fixes
-
Validate PROGRESS.md format after plan agent writes it: archon-loop.sh should run parse_objective_files() immediately after the plan phase and, if empty, inject a corrective hint into a retry prompt or re-run the plan agent.
-
Include shell warnings in the plan agent's prompt: The plan agent's initial prompt should include the orchestrator's last warning/error messages from the previous iteration, so it can self-correct format issues.
-
Make parsing more resilient: parse_objective_files() could also accept alternative headings (e.g. ## Strategy) or scan for **/*.lean** patterns anywhere in the file, rather than requiring the exact heading ## Current Objectives.
Environment
Summary
The plan agent can rewrite
PROGRESS.mdin a format thatarchon-loop.sh'sparse_objective_files()cannot parse, causing prover dispatch to silently fail. Neither the plan agent nor the review agent receives this error, so the system loops indefinitely without self-correcting. In our run, this wasted 9 iterations, ~163 minutes of wall time, and ~$28 in API costs with zero progress.Root Cause
parse_objective_files()inarchon-loop.sh(line 173-187) requires a## Current Objectivessection to extract target.leanfiles:After a productive prover iteration, the plan agent rewrote
PROGRESS.mdusing## Strategyinstead of## Current Objectives. The file still listed per-file objectives under### N. **File.lean**sub-headings, but since the parent heading was wrong, parsing returned empty.Before (productive iteration, worked):
After (next iteration's plan agent, broken):
The Feedback Loop Failure
The shell orchestrator logged a warning every iteration:
{"event":"shell","level":"warn","message":"No files parsed from PROGRESS.md ## Current Objectives."}This warning appeared in all 9 broken iterations. However:
Plan agent couldn't see the warning — it was logged to the JSONL file but never injected into the plan agent's prompt. The plan agent had no way of knowing its own PROGRESS.md was being rejected by the shell parser.
Review agent misdiagnosed the problem — the review agent observed "zero edits, zero sorry reduction" across consecutive sessions, but attributed it to mathematical strategy exhaustion ("replay loop — same targets assigned, same strategies exhausted"). It recommended the plan agent switch to infrastructure-building tasks. It never identified the real cause: that provers were not being launched at all due to a heading format mismatch. The review agent's recommendations were mathematically sound but addressed the wrong problem entirely.
Plan agent faithfully followed the wrong diagnosis — it read the review's recommendations, adopted the infrastructure-building strategy, carefully restructured its objectives — and then wrote PROGRESS.md with
## Strategyagain (still without## Current Objectives). By iteration 17, the plan agent explicitly stated: "The plan is mature and actionable. The system needs to execute it." — blaming infrastructure rather than its own output format.In short: the review agent never realized the problem was in PROGRESS.md's heading format; the plan agent never received the shell-level error; and both agents spent 9 iterations optimizing mathematical strategy while the actual failure was a one-line format mismatch invisible to both of them.
Impact
Suggested Fixes
Validate PROGRESS.md format after plan agent writes it:
archon-loop.shshould runparse_objective_files()immediately after the plan phase and, if empty, inject a corrective hint into a retry prompt or re-run the plan agent.Include shell warnings in the plan agent's prompt: The plan agent's initial prompt should include the orchestrator's last warning/error messages from the previous iteration, so it can self-correct format issues.
Make parsing more resilient:
parse_objective_files()could also accept alternative headings (e.g.## Strategy) or scan for**/*.lean**patterns anywhere in the file, rather than requiring the exact heading## Current Objectives.Environment
Exploresubagent routes to Sonnet 4.6 automatically for codebase search — this is Claude Code behavior, not Archon routing.init.shwas run;/archon-lean4:doctorreports all green (same setup as Prover agents never use MCP tools; Skill invocations fall back to Bash with 'command not found' #9)