# Coord-MCP Multi-Agent Coordination — TODO

**Source of truth for pending work.** Complements `COORD-MCP-STATE.md` (where
we are) and `COORD-MCP-DESIGN-LOG.md` (full design rationale + DD-1..DD-38).

Last updated: 2026-04-20.

---

## P0 — Active / next pickup

| # | Task | Repo | Est | Blocks |
|---|------|------|-----|--------|
| 33 | `client_kind` += `openai`/`mistral`; add `variant` free-form (opus-4.7, flash-2.5, leanstral, …) | boj-server | 0.5 d | 34 |
| 34 | Capability advertisement on register: `class` / `tier` / `prover_strengths` + `coord_get_peer_capabilities` FFI | boj-server | 1 d | cold-start routing |
| 007-mcp-1 | `coordRegister` HTTP write: `cartridges/007-mcp/ffi/oo7_mcp_ffi.zig` currently TCP-probes only. Rewrite to POST `http://127.0.0.1:7745/tools/coord_register`, parse token + peer_id into `g_coord_token_buf`/`g_peer_id_buf`. | 007-lang | 1 session | end-to-end 007 cartridge |
| 007-mcp-2 | Run `just cartridge-install` in 007-lang, commit resulting tree in boj-server. **Gate on #33+#34 shipping first** (shared-state in `local-coord-mcp/ffi/` + `adapter/`). | 007-lang → boj-server | 1 session | — |
| echidna-L3-w2-verify | Watch next `0 3 * * *` UTC nightly of `live-provers.yml`; fix red matrix cells in-place (likely: isabelle 500MB download, tlaps URL drift, fstar binary symlink). | echidna | 1 session | Wave-3 entry |

## P1 — Short term (weeks)

### Coord-MCP phase 1b refinements

- **Hash chain per envelope** — sender-side `prev_msg_hash`; server tracks chain head; break = instant reject. (DD-8 mechanism 1.)
- **Content sanity gate** — file-ref validity vs recent-FS cache + self-contradiction heuristic + risk-tier escalator patterns (`git push` → auto-promote Tier 3). (DD-8 mechanism 4, DD-14.)
- **Watchdog TTL enforcement** — 30 s apprentice, 5 min journeyman; `progress` heartbeat resets. (DD-20.)
- **Warn-drift broadcast on auto-release** via Opus review. (DD-21.)
- **Quarantine queue spill to VeriSimDB** when full; currently `MAX_QUARANTINE=32` hot cache only. (DD-17.)
- **Audit-echo anchor** — preserve old chain head on peer crash/restart; new peer = fresh chain. (DD-29.)
- **Drift detector** — flag `confidence > 0.8 AND effective_affinity < 0.3`. (DD-9 layer D.)
- **`coord_health` metrics tool** — active peers, pending quarantine, reject rate, claim depth.
- **Rejection rate limit hardening** — 5 rejects / 10 min per `client_kind` already lands cooldown; audit whether per-peer is better on heavy multi-session load.

### 007-mcp + 007-lang

- **Harvard DataExpr refactor** (D1) — split `crates/oo7-core/src :: DataExpr` into pure `DataExpr` + `DataFlow` control carrier. Restores `just contractile-check` green on fresh clones.
- **Adopt natsci-studio `intend.k9.ncl`** negotiation + accountability pledge in 007 (declared as horizon wish in new `Intentfile.a2ml`).
- ~~Sidecar revert~~ — executed this session per D4.

### Echidna — L3 completion

- **Wave-3 (Tier-3 weekly, 9 backends)** — per-backend Containerfiles (Podman):
  Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath.
  Handover hints in `verification-ecosystem/echidna/.machine_readable/6a2/STATE.a2ml [wave-3-handover-hints]`.
- **Wave-4 (Tier-4 quarterly, 19 backends)** — best-effort allow-fail placeholder; retain as mock-only unless a maintainer volunteers.
- **Dafny deep-wiring upgrade** — `provers/dafny.rs` is 165 LoC; live version-check passes but subprocess wrapper is stub-ish. (L3 prompt "Harden wiring depth".)
- **Real-Chapel CI job** — `chapel-ci.yml` tests against stubs only. Add a job that builds real `libechidna_chapel.so` from `chapel_poc/` and links Rust with `-Dstubs=false`. Allow-fail at first.
- **VeriSimDB record emission** from live-prover harness per `feedback_verisimdb_policy` — coordinate with `verisimdb` repo schema first.

### Estate-wide

- **6a2 canonical-location reconciliation** (D2) — for each repo with duplicate SCM files, diff root vs `.machine_readable/6a2/` copy; merge if divergent; `git rm` root. Global CLAUDE.md is authoritative: `.machine_readable/` only. Use `adjust/` contractile runner once the hook source migrates off the stale 6-verb set.

## P2 — Medium (Phase 2 formalisms over working v1)

- **Proof obligations P-04..P-07** in `cartridges/local-coord-mcp/abi/LocalCoord/Durability.idr`: record format; CRC truncation; **P-06 replay-equivalence (keystone)**; quarantine state machine. ~6 days.
- **Idris2 session types** for supervisor/attestation choreography in `abi/LocalCoord/Protocol.idr`. Makes protocol compliance a compile-time property.
- **Deontic / dyadic types** for supervision rules — formalise "tier 4 forbidden for apprentice" as a type-level obligation.
- **Gatekeeper / scheduler split** (DD-38) — separate the master's approve-veto role from the dispatch-routing role. Small-team stays merged; big team splits. RFC deferred to when cross-model dispatch demands it.
- **Task #2** — wire `boj_cartridge_invoke` to real FFI (low priority; HTTP path works fine today).
- **Task #7b** — swap `coord_durability.zig` backend to `verisimdb-mcp` FFI once that FFI is real. Typed log helpers stay as the API. (DD-31.)

## P3 — Phase 3: formal foundations

- **Agda echo-types formalisation** of audit + summary + hash-chain as echo types, via `EchoChoreo` / `EchoEpistemic` / `EchoTropical` bridges. Dogfoods `echo-types/` as a non-toy consumer.
- **Tropical types** as modeling lens — TTL = tropical max; trust composition = tropical min; tier promotion = max; attention budget = inf over priorities. (Appendix J.)
- **Epistemic types** explicit: rename `context_fetch_id` → `knowledge_witness`; document per-role epistemic policy in `envelope-design.adoc`.

## P4 — Phase 4: v2 federation (trigger: first joint IDApTIK/ASS session)

- **Envelope v2** with `site_id` + `federation.authoritative_site` + `federation.project_id` + `federation.handoff_ceremony_id`.
- **Authoritative-site model** (DD-22) — one site holds primacy per project; peer defers on code-ownership. Motivation: prevent IDApTIK-style mission drift.
- **Security stack** — SDP (Secure Device Provisioning) + Stapeln container + HTTP capability gateway + high-security options.
- **Primacy handoff ceremony** — explicit protocol, choreographic + epistemic transfer.
- **Cross-site attestation + trust composition** — tropical min for transitive trust.
- **Integrate with Umoja federation layer** (gossip + hash attestation) for cross-machine transport.

## Non-goals / explicitly deferred

- HTTP capability gateway + SDP for local-only v1 (overkill).
- Auto-modifying affinities without Opus + user review (always loop back).
- Cross-machine transport in v1 envelope.
- Cost-aware scheduling / credit-burn tracking (separate feature; can consume capability metadata later).
- Choreographic / epistemic / echo / tropical type _enforcement_ (Phase 2+/3 modeling layers only).

---

## Decisions — agreed 2026-04-20 (was: open questions)

User agreed these four decisions as the way forward. Logged here so
future sessions do not re-litigate them. Rationale lines are the
original recommendations retained verbatim.

| # | Decision | Rationale | Follow-up |
|---|----------|-----------|-----------|
| D1 | **Refactor** `DataExpr` in `crates/oo7-core/src` — split pure `DataExpr` from `DataFlow` control carrier. | Control-flow variants in a data-expression enum is a structural Harvard-invariant violation, not stylistic. `variance_schema` would codify the mistake. Refactor is 1–2 h in a well-factored crate; variance only justified if the merger is load-bearing on a benchmarked hot path (not the case). | **P1 task added** — 007-lang crate refactor. `just contractile-check` currently red on fresh clones; turns green after split. |
| D2 | **Canonical SCM-file location is `.machine_readable/6a2/`.** Root-level copies are drift and must be removed. | Global `CLAUDE.md`: *"CRITICAL: SCM files MUST be in `.machine_readable/` directory ONLY. Never create STATE.scm, META.scm, … in the repository root."* | **P1 task added** — diff root vs 6a2/ copies per repo; merge if divergent; `git rm` root. Estate-wide sweep. |
| D3 | **Wait on `just cartridge-install` in boj-server** until coord-mcp Tasks #33 + #34 ship. | Shared-state risk: `cartridges/local-coord-mcp/ffi/local_coord_ffi.zig` + `adapter/local_coord_adapter.zig` are owned by the sequential session for #33/#34 (Peer struct, ClientKind enum). Running install now risks conflicts on their live working tree. | **Gate locked** — 007-mcp-2 in P0 table blocks on #33+#34. |
| D4 | **Revert** modified `audits/canonical-proof-suite/` + `proofs/canonical-proof-suite/` in 007-lang. | They are `just canonical-proof-suite` probe-timing artefacts, not session scope. The parallel session itself flagged them as non-scope. Committing conflates measurement noise with substantive proof state. Regenerable if needed. | **Executed this session** — `git checkout --` in 007-lang. |

## Task status snapshot (complete / pending / deferred)

**Complete (22 tasks):** #1, #3, #4, #5, #6, #7, #8, #9, #10, #11, #12, #13, #14, #15, #16, #17, #32, #35, #36, #37, k9-svc spot-fix, echidna L3 Wave-1 + Wave-2.

**Pending P0/P1:** #33, #34, 007-mcp-1/2, echidna Wave-2 CI verification, 6a2 reconciliation, Harvard DataExpr, sidecar revert, intend.k9.ncl adoption.

**Deferred:** #2, #7b, P-04..P-07 proofs, Idris2 session types, DD-38 split, all Phase 3/4 items.
