Merge v1.0.1 updates and switch Codex to streaming app-server

DOCS.md

@@ -7,7 +7,7 @@ OpenProver uses a **planner-worker** architecture. A single planner LLM coordina
 ```
 cli.py          Parse args, setup TUI, run prover, print cost
 prover.py       Planner loop, step dispatch, action handlers, Repo
-llm.py          LLMClient (Claude CLI), HFClient (OpenAI-compatible HTTP)
+llm.py          LLMClient (Claude CLI), CodexClient (Codex CLI), HFClient (OpenAI-compatible HTTP)
 prompts.py      All prompt templates, TOML parser, actions enum
 budget.py       Budget tracking (token or time limits)
 lean/
@@ -30,7 +30,7 @@ inspect.py      Read-only run browser
 **Workers** (spawned on demand, parallel):
 - Receive a task description from the planner
 - Can reference repo items via `[[wikilink]]` syntax (resolved before sending)
-- When `--lean-project` is set with a tool-capable worker model, workers have access to `lean_verify` and `lean_search` tools via MCP (Claude) or native tool calling (vLLM)
+- When `--lean-project` is set with a tool-capable worker model, workers have access to `lean_verify` and `lean_search` tools via MCP (Claude/Codex) or native tool calling (vLLM)
 - Report free-form results back to the planner
 
 **Repository** (`repo/` directory):
@@ -47,9 +47,10 @@ Entry point. Parses arguments, creates a `Prover` and `TUI`, installs signal han
 Subcommands:
 - `openprover <theorem>` - main proving loop
 - `openprover inspect [run_dir]` - browse a historical run
+- `openprover reverify [run_dir]` - rerun archived worker verification with a selected verifier backend
 - `openprover fetch-lean-data` - download Lean Explore search data and models
 
-The LLM client is constructed via a factory pattern: `Prover` calls `make_llm(archive_dir)` after setting up the work directory, so the archive path is correct from the start. Separate planner and worker models are supported via `--planner-model` and `--worker-model`.
+The LLM client is constructed via a factory pattern: `Prover` calls `make_llm(archive_dir)` after setting up the work directory, so the archive path is correct from the start. Separate planner and worker models are supported via `--planner-model` and `--worker-model`, backend providers can be selected independently via `--provider`, `--planner-provider`, and `--worker-provider` (for example `--provider codex --model gpt-5.4`), and reasoning effort can be set independently via `--reasoning-effort`, `--planner-reasoning-effort`, and `--worker-reasoning-effort`. When omitted, reasoning effort defaults to `high` for Claude/Codex backends and remains unset for `local`.
 
 Run configuration is saved to `run_config.toml` in the work directory on fresh starts and restored on resume. CLI flags override saved values.
 
@@ -68,7 +69,7 @@ The `Prover` class owns the proving loop and all state.
 **Init:** Creates or resumes a run directory (`runs/<slug>-<timestamp>/`). Loads or initializes the whiteboard. Creates the `Repo` instance. Resume is detected by checking for existing `WHITEBOARD.md` + `THEOREM.md`; step count inferred from `step_NNN` directories.
 
 When `lean_worker_tools` is enabled, sets up tool calling for workers:
-- **Claude CLI workers**: Configures an MCP server (`lean/mcp_server.py`) with `lean_verify` and `lean_search` tools
+- **Claude/Codex CLI workers**: Configures an MCP server (`lean/mcp_server.py`) with `lean_verify` and `lean_search` tools
 - **vLLM workers**: Initializes LeanExplore search service in-process and uses native OpenAI tool calling
 
 **Step flow** (`run` -> `_do_step`):
@@ -86,12 +87,12 @@ When `lean_worker_tools` is enabled, sets up tool calling for workers:
 | Handler | What it does |
 |---------|-------------|
 | `_handle_spawn` | Run worker tasks in parallel via `ThreadPoolExecutor` (up to `--parallelism`). Each worker gets its task description with wikilinks resolved. Results pushed to output window. |
-| `_handle_literature_search` | Spawn a web-enabled worker (Claude CLI with `WebSearch` + `WebFetch` tools). Results fed back to planner. |
+| `_handle_literature_search` | Spawn a web-enabled worker (Claude or Codex CLI with web search enabled). Results fed back to planner. |
 | `_handle_read_items` | Fetch full content of requested repo items, push to output. |
 | `_handle_write_items` | Create/update/delete repo items. Items with `format="lean"` are auto-verified via `lake env lean`. |
 | `_handle_write_whiteboard` | Update the whiteboard without spawning workers. |
 | `_handle_read_theorem` | Return THEOREM.md + THEOREM.lean + PROOF.md content to the planner. |
-| `_handle_submit_proof` | Save proof to `PROOF.md`. If Lean theorem exists, also assembles and verifies Lean proof via `lake env lean`, writes `PROOF.lean` on success. |
+| `_handle_submit_proof` | Save proof to `PROOF.md`, plus `PROOF_MANIFEST.json` and `PROOF_DEPENDENCIES.md` derived from the proof's `[[slug]]` references. If Lean theorem exists, also assembles and verifies Lean proof via `lake env lean`, writes `PROOF.lean` on success. |
 | `_handle_give_up` | Terminate. Only allowed after the give-up threshold (default 50% of budget). |
 
 **`Repo` class** (also in `prover.py`):
@@ -114,7 +115,7 @@ When `lean_worker_tools` is enabled, sets up tool calling for workers:
 
 For the vLLM path, tools are executed in a multi-turn loop: the LLM requests tool calls, `_execute_worker_tool()` dispatches to `_tool_lean_verify()` or `_tool_lean_search()`, results are appended to the conversation, and the LLM continues.
 
-For the Claude CLI path, tool execution is handled by the MCP server subprocess. Tool call events are detected from the stream and reported to the TUI via `add_worker_action()`.
+For the Claude/Codex CLI path, tool execution is handled by the MCP server subprocess. Tool call events are detected from the stream and reported to the TUI via `add_worker_action()`.
 
 **Other methods:**
 - `_write_discussion()`: Post-session analysis via LLM call
@@ -124,18 +125,18 @@ For the Claude CLI path, tool execution is handled by the MCP server subprocess.
 
 ### `llm.py`
 
-Two LLM client implementations with the same interface.
+Three LLM client implementations with the same interface.
 
 **`LLMClient`** (Claude CLI wrapper):
 
 Non-streaming:
 ```
-claude -p --model <model> --system-prompt <...> --output-format json --tools ""
+claude -p --model <model> --system-prompt <...> --effort <level> --output-format json --tools ""
 ```
 
 Streaming:
 ```
-claude -p --model <model> --system-prompt <...> --output-format stream-json --verbose --include-partial-messages --tools ""
+claude -p --model <model> --system-prompt <...> --effort <level> --output-format stream-json --verbose --include-partial-messages --tools ""
 ```
 Uses `Popen` + `readline()` (not the line iterator, which has read-ahead buffering that defeats real-time streaming). Parses NDJSON lines, dispatches `content_block_delta` text to the callback.
 
@@ -149,6 +150,17 @@ MCP tool calling: When `mcp_config` is set, adds `--mcp-config <json> --strict-m
 
 Archiving: Every call saved to `archive/calls/call_NNN.json` with full prompt, system prompt, schema, response, cost, timing, and errors.
 
+**`CodexClient`** (OpenAI Codex app-server wrapper):
+- Launches `codex app-server --listen stdio:// --session-source mcp`
+- Starts ephemeral threads/turns over the app-server RPC protocol instead of using `codex exec --json`
+- Passes reasoning effort through the `turn/start` `effort` field
+- Enables web search with thread config `{"web_search": "live"}` when `web_search=True`
+- Passes `mcp_config` through as thread config so Lean tools work through Codex MCP
+- Streams assistant text, reasoning text, and tool activity incrementally from app-server notifications into the TUI
+- Supports soft interrupt by sending `turn/interrupt`; interrupted turns return `finish_reason = "soft_interrupted"` with partial output preserved
+- Infers a 400k context window for GPT-5-family model ids and otherwise falls back to 200k
+- Archives the completed turn payload plus streamed output/thinking; cost currently remains `0.0` because app-server usage metadata is not surfaced through this integration
+
 **`HFClient`** (OpenAI-compatible HTTP, for vLLM):
 - Calls an OpenAI-compatible API at `--provider-url`
 - Health check on init (`/health` endpoint)
@@ -276,6 +288,8 @@ runs/<slug>-<timestamp>/
   THEOREM.lean                 - formal Lean statement (if --lean-theorem)
   WHITEBOARD.md                - latest whiteboard state (enables resume)
   PROOF.md                     - written only if proof found
+  PROOF_MANIFEST.json          - machine-readable proof -> repo dependency graph
+  PROOF_DEPENDENCIES.md        - proof section -> repo dependency summary
   PROOF.lean                   - formal Lean proof (if lean mode)
   DISCUSSION.md                - post-session analysis
   run_config.toml              - saved run configuration (for resume)
@@ -284,14 +298,18 @@ runs/<slug>-<timestamp>/
   steps/
     step_001/
       planner.toml             - planner's TOML decision
+      meta.toml                - planner/worker/verifier cost + backend metadata
       workers/
         task_0.md              - worker task description
         result_0.md            - worker output
-        worker_0_call.json     - archived LLM call
+        worker_0_call.md       - archived worker call with provider/model/effort frontmatter
+        verifier_0_call.md     - archived verifier call with provider/model/effort frontmatter
+        verifier_result_0.md   - verifier writeup / verdict
     step_002/...
-  archive/
-    calls/
-      call_001.json            - full LLM call record
+  reverify/
+    <timestamp>/
+      summary.md               - verdict summary for a replayed verifier run
+      step_001/worker_0/...    - copied task/output plus fresh verifier call archive
 ```
 
 **Slug format:** First 40 chars of theorem, lowercased, non-alphanumeric replaced with hyphens. Example: `sqrt2-irrational-20260220-143706`.
@@ -300,7 +318,9 @@ runs/<slug>-<timestamp>/
 
 ## Verification
 
-**Informal verification** (all modes): Workers can be tasked with verification by the planner. A verifier worker sees only the proof text (not the reasoning that produced it) and must end its response with `VERDICT: CORRECT` or `VERDICT: INCORRECT`. The planner is instructed to verify proofs before submitting.
+**Informal verification** (all modes): Workers can be tasked with verification by the planner. A verifier worker sees only the proof text (not the reasoning that produced it) and must end its response with `VERDICT: CORRECT` or `VERDICT: INCORRECT`. The planner is instructed to verify proofs before submitting. Verifier call archives persist the provider, requested model, actual model, and reasoning effort for later audit.
+
+**Re-verification**: `openprover reverify` walks archived worker tasks/results, reruns the verifier with a selected backend/model/effort, and writes a bundle under `run_dir/reverify/<timestamp>/`. By default it resumes the latest matching reverify bundle if present and revisits previously `CORRECT` items only. If one of those items fails re-verification, `--repair-broken` (enabled by default) makes OpenProver try to repair that item and then re-verify the repaired text. Pass `--no-repair-broken` for audit-only mode, or `--no-resume` to force a fresh bundle.
 
 **Formal verification** (lean modes): When `--lean-project` is provided, the system supports automatic Lean 4 verification:
 
@@ -316,6 +336,8 @@ Generated Lean files are placed in `<lean-project>/OpenProver-<random_id>/` with
 
 Task descriptions can reference repository items via `[[slug]]` syntax. Before a worker receives its task, `repo.resolve_wikilinks()` finds all references, fetches the content, and appends it as a "Referenced Materials" section. This lets the planner share proven lemmas, observations, or literature findings with workers without duplicating content in every task.
 
+Submitted proofs can also use explicit `[[slug]]` references. On `submit_proof`, OpenProver records direct proof references, recursively expands transitive repo dependencies, and writes both a JSON manifest and a human-readable reverse index so later audits can see which proof sections depend on which repo items.
+
 ## Adding a new action
 
 1. Add the action name to `ACTIONS` in `prompts.py`