Agent preflight gates - #3
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 26b9a2ade8
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| 1. Read the current `results/{problem_id}/blueprint.md` draft as pure text. | ||
| 2. First check that `blueprint.md` contains a full proof draft of the entire target theorem rather than a partial proof, fragment, or exploratory notes. If it does not, do not call the verifier yet. | ||
| 3. Call MCP tool `verify_proof_service` with: | ||
| 1. Confirm that the latest preflight record for the active target has `gate_status="pass"`. If not, do not call the verifier and do not treat the draft as a settled final proof. |
There was a problem hiding this comment.
This new guard blocks verify_proof_service unless preflight is already pass, which creates a dead-end for targets marked blocked_on_status_mismatch: the agent is instructed to keep attacking hard/open problems and to rely on verification before success, but this rule prevents verifying any exploratory full proof that could resolve the mismatch. In practice, a candidate proof for a currently-open/unclear target can never be validated, so the workflow cannot converge from exploratory work to a verified result.
Useful? React with 👍 / 👎.
| 2. Propose materially different decomposition plans. | ||
| 3. For each plan, state: | ||
| 1. Confirm that the latest preflight record for the active goal has `gate_status="pass"`, or that the active goal is an explicitly narrowed variant whose scope was approved in a later preflight record. | ||
| 2. If the preflight gate is blocked for the active goal, do not propose decomposition plans for that goal as if it were settled. Instead append a blocking `events` record and return. |
There was a problem hiding this comment.
Returning immediately when preflight is blocked prevents decomposition planning entirely, but the updated agent policy explicitly allows exploratory decomposition under blocked preflight (as long as it is not presented as a settled final proof). This early return removes a key exploration path for ambiguous/open-status problems and can stall progress that the policy now expects the agent to continue making.
Useful? React with 👍 / 👎.
The repo's Codex MCP configs were pointing at system Python from the agent root, which made local MCP startup fragile once the workspace-local mcp package shadowed the third-party dependency and FastMCP attempted update checks through the current proxy setup. Point both agents at their project virtualenvs, run them from the mcp directory, and disable FastMCP update checks. Add ignore rules for Codex/OMX state, caches, virtualenvs, and generated demo artifacts so local execution does not keep dirtying the working tree. Constraint: Local MCP servers must use the agent-specific virtualenvs described by the README Constraint: Current environment exports a SOCKS proxy that breaks FastMCP update checks without extra dependencies Rejected: Rename the repo mcp directories | broader code and documentation churn than needed for a local-run fix Confidence: high Scope-risk: narrow Reversibility: clean Directive: Keep MCP servers launched from each agent's .venv and mcp cwd unless the package layout changes Tested: Started both MCP servers with the corrected config; ran the README example through verification and produced blueprint_verified.md Not-tested: Fresh-clone bootstrap before any local virtualenv exists
The generation agent now performs a mandatory preflight before proof search, decomposition, final-proof drafting, or verification. The new preflight skill records statement clarity, terminology/model ambiguity, and literature status, and the downstream search/proving/verification skills now stop with explicit blocking records unless the active target has gate_status="pass". This keeps the workflow from silently collapsing subclass-only or open-problem evidence into a settled proof target and makes those decisions queryable in memory. Constraint: Prompt-and-skill surface only; no new dependencies or verification-side changes Rejected: Let downstream skills infer ambiguity ad hoc | too easy to miss and too hard to audit consistently Confidence: high Scope-risk: moderate Reversibility: clean Directive: Keep theorem-status and model-ambiguity checks centralized in preflight and require gate_status="pass" before final-proof drafting Tested: git diff --cached --check; find agents/generation/.agents/skills/preflight-problem-statement -maxdepth 3 -type f | sort; rg -n "preflight-problem-statement|gate_status=\"pass\"|blocked_by_preflight|known_only_in_subclasses|status_assessment" agents/generation/AGENTS.md agents/generation/.agents/skills -S Not-tested: End-to-end generation run with the local verification service
ARCHITECTURE §6.5 wires the librarian channel as request/response with a 30 s recv timeout. When a single APPLY runs longer than that, the coordinator returns from `_forward_new_events` without acking the event. The reply still arrives in the pipe afterwards. On the next tick the watcher re-surfaces the same event_id, the coordinator re-sends APPLY, and the librarian replies a *second* time (idempotent re-apply per §5.5.0 #3). Both replies now sit in the pipe. Pre-fix: the next event in the loop would naively pair its `request` with the redundant ev1 reply still buffered ahead of its real reply, so coordinator would ack the wrong (event_id) event. Worse, the out-of-band reply for the truly-pending event remains in the pipe and poisons all subsequent ticks. Drain replies whose `event_id` does not match the APPLY we just sent before treating any reply as the answer. Reply event_ids come straight from `_handle_apply` in `librarian/daemon.py`, so a matching id is the authoritative correlation. Regression test in tests/unit/test_m8_forward_drains_stale_replies.py.
1 participant
No description provided.