|
| 1 | +# Coord-MCP Multi-Agent Coordination — TODO |
| 2 | + |
| 3 | +**Source of truth for pending work.** Complements `COORD-MCP-STATE.md` (where |
| 4 | +we are) and `COORD-MCP-DESIGN-LOG.md` (full design rationale + DD-1..DD-38). |
| 5 | + |
| 6 | +Last updated: 2026-04-20. |
| 7 | + |
| 8 | +--- |
| 9 | + |
| 10 | +## P0 — Active / next pickup |
| 11 | + |
| 12 | +| # | Task | Repo | Est | Blocks | |
| 13 | +|---|------|------|-----|--------| |
| 14 | +| 33 | `client_kind` += `openai`/`mistral`; add `variant` free-form (opus-4.7, flash-2.5, leanstral, …) | boj-server | 0.5 d | 34 | |
| 15 | +| 34 | Capability advertisement on register: `class` / `tier` / `prover_strengths` + `coord_get_peer_capabilities` FFI | boj-server | 1 d | cold-start routing | |
| 16 | +| 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 | |
| 17 | +| 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 | — | |
| 18 | +| 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 | |
| 19 | + |
| 20 | +## P1 — Short term (weeks) |
| 21 | + |
| 22 | +### Coord-MCP phase 1b refinements |
| 23 | + |
| 24 | +- **Hash chain per envelope** — sender-side `prev_msg_hash`; server tracks chain head; break = instant reject. (DD-8 mechanism 1.) |
| 25 | +- **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.) |
| 26 | +- **Watchdog TTL enforcement** — 30 s apprentice, 5 min journeyman; `progress` heartbeat resets. (DD-20.) |
| 27 | +- **Warn-drift broadcast on auto-release** via Opus review. (DD-21.) |
| 28 | +- **Quarantine queue spill to VeriSimDB** when full; currently `MAX_QUARANTINE=32` hot cache only. (DD-17.) |
| 29 | +- **Audit-echo anchor** — preserve old chain head on peer crash/restart; new peer = fresh chain. (DD-29.) |
| 30 | +- **Drift detector** — flag `confidence > 0.8 AND effective_affinity < 0.3`. (DD-9 layer D.) |
| 31 | +- **`coord_health` metrics tool** — active peers, pending quarantine, reject rate, claim depth. |
| 32 | +- **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. |
| 33 | + |
| 34 | +### 007-mcp + 007-lang |
| 35 | + |
| 36 | +- **Harvard DataExpr refactor** (D1) — split `crates/oo7-core/src :: DataExpr` into pure `DataExpr` + `DataFlow` control carrier. Restores `just contractile-check` green on fresh clones. |
| 37 | +- **Adopt natsci-studio `intend.k9.ncl`** negotiation + accountability pledge in 007 (declared as horizon wish in new `Intentfile.a2ml`). |
| 38 | +- ~~Sidecar revert~~ — executed this session per D4. |
| 39 | + |
| 40 | +### Echidna — L3 completion |
| 41 | + |
| 42 | +- **Wave-3 (Tier-3 weekly, 9 backends)** — per-backend Containerfiles (Podman): |
| 43 | + Tamarin, ProVerif, Imandra, SCIP, OR-Tools, HOL4, ACL2, Twelf, Metamath. |
| 44 | + Handover hints in `verification-ecosystem/echidna/.machine_readable/6a2/STATE.a2ml [wave-3-handover-hints]`. |
| 45 | +- **Wave-4 (Tier-4 quarterly, 19 backends)** — best-effort allow-fail placeholder; retain as mock-only unless a maintainer volunteers. |
| 46 | +- **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".) |
| 47 | +- **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. |
| 48 | +- **VeriSimDB record emission** from live-prover harness per `feedback_verisimdb_policy` — coordinate with `verisimdb` repo schema first. |
| 49 | + |
| 50 | +### Estate-wide |
| 51 | + |
| 52 | +- **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. |
| 53 | + |
| 54 | +## P2 — Medium (Phase 2 formalisms over working v1) |
| 55 | + |
| 56 | +- **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. |
| 57 | +- **Idris2 session types** for supervisor/attestation choreography in `abi/LocalCoord/Protocol.idr`. Makes protocol compliance a compile-time property. |
| 58 | +- **Deontic / dyadic types** for supervision rules — formalise "tier 4 forbidden for apprentice" as a type-level obligation. |
| 59 | +- **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. |
| 60 | +- **Task #2** — wire `boj_cartridge_invoke` to real FFI (low priority; HTTP path works fine today). |
| 61 | +- **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.) |
| 62 | + |
| 63 | +## P3 — Phase 3: formal foundations |
| 64 | + |
| 65 | +- **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. |
| 66 | +- **Tropical types** as modeling lens — TTL = tropical max; trust composition = tropical min; tier promotion = max; attention budget = inf over priorities. (Appendix J.) |
| 67 | +- **Epistemic types** explicit: rename `context_fetch_id` → `knowledge_witness`; document per-role epistemic policy in `envelope-design.adoc`. |
| 68 | + |
| 69 | +## P4 — Phase 4: v2 federation (trigger: first joint IDApTIK/ASS session) |
| 70 | + |
| 71 | +- **Envelope v2** with `site_id` + `federation.authoritative_site` + `federation.project_id` + `federation.handoff_ceremony_id`. |
| 72 | +- **Authoritative-site model** (DD-22) — one site holds primacy per project; peer defers on code-ownership. Motivation: prevent IDApTIK-style mission drift. |
| 73 | +- **Security stack** — SDP (Secure Device Provisioning) + Stapeln container + HTTP capability gateway + high-security options. |
| 74 | +- **Primacy handoff ceremony** — explicit protocol, choreographic + epistemic transfer. |
| 75 | +- **Cross-site attestation + trust composition** — tropical min for transitive trust. |
| 76 | +- **Integrate with Umoja federation layer** (gossip + hash attestation) for cross-machine transport. |
| 77 | + |
| 78 | +## Non-goals / explicitly deferred |
| 79 | + |
| 80 | +- HTTP capability gateway + SDP for local-only v1 (overkill). |
| 81 | +- Auto-modifying affinities without Opus + user review (always loop back). |
| 82 | +- Cross-machine transport in v1 envelope. |
| 83 | +- Cost-aware scheduling / credit-burn tracking (separate feature; can consume capability metadata later). |
| 84 | +- Choreographic / epistemic / echo / tropical type _enforcement_ (Phase 2+/3 modeling layers only). |
| 85 | + |
| 86 | +--- |
| 87 | + |
| 88 | +## Decisions — agreed 2026-04-20 (was: open questions) |
| 89 | + |
| 90 | +User agreed these four decisions as the way forward. Logged here so |
| 91 | +future sessions do not re-litigate them. Rationale lines are the |
| 92 | +original recommendations retained verbatim. |
| 93 | + |
| 94 | +| # | Decision | Rationale | Follow-up | |
| 95 | +|---|----------|-----------|-----------| |
| 96 | +| 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. | |
| 97 | +| 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. | |
| 98 | +| 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. | |
| 99 | +| 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. | |
| 100 | + |
| 101 | +## Task status snapshot (complete / pending / deferred) |
| 102 | + |
| 103 | +**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. |
| 104 | + |
| 105 | +**Pending P0/P1:** #33, #34, 007-mcp-1/2, echidna Wave-2 CI verification, 6a2 reconciliation, Harvard DataExpr, sidecar revert, intend.k9.ncl adoption. |
| 106 | + |
| 107 | +**Deferred:** #2, #7b, P-04..P-07 proofs, Idris2 session types, DD-38 split, all Phase 3/4 items. |
0 commit comments