diff --git a/plans/artdag-on-sx.md b/plans/artdag-on-sx.md
index 1f005f50..7264266a 100644
--- a/plans/artdag-on-sx.md
+++ b/plans/artdag-on-sx.md
@@ -20,8 +20,9 @@ the same SX substrates already serve the phases:
 - **Execute** (composable effects + content-addressed memo) → SX's own
   `perform`/`cek-resume` + a **persist**-backed content-addressed result cache;
   incremental recompute drops the cost of re-rendering to the dirty subgraph.
-- **Optimize** (fuse/dedup effect pipelines) → term rewriting (a later, optional
-  consumer of `maude-on-sx`'s engine — see `plans/maude-on-sx.md`).
+- **Optimize** (fuse/dedup effect pipelines) → term rewriting, the declarative
+  consumer of `maude-on-sx`'s engine — now ACTIVE as Phase 7 (lib/maude is on
+  this branch; fit proven in `lib/maude/tests/effects.sx`).
 
 End-state: a content-addressed dataflow engine in `lib/artdag/` with analyze, plan,
 incremental execute, effect-pipeline optimization, and a shared-cache federation
@@ -124,8 +125,7 @@ lib/artdag/optimize.sx                  lib/artdag/federation.sx
 - [x] optimizations are content-id-preserving where semantically identical; assert
   the optimized DAG produces identical results
 - [x] `lib/artdag/tests/optimize.sx` — DCE, CSE dedup, fusion equivalence
-- [ ] (optional/later) rule-based optimization via `maude-on-sx`'s rewriting engine —
-  flag the integration point, don't block on it
+- [x] (superseded by Phase 7) integration point flagged
 
 ## Phase 6 — Federation (shared content-addressed cache)
 
@@ -136,6 +136,47 @@ lib/artdag/optimize.sx                  lib/artdag/federation.sx
 - [x] revocation/invalidation — drop a remote result if its provenance is withdrawn
 - [x] `lib/artdag/tests/fed.sx` — remote cache hit, trust gating, invalidation
 
+## Phase 7 — Rule-based optimization via maude-on-sx  (ACTIVE — start here)
+
+`lib/maude/` is now present on this branch (term rewriting modulo assoc/comm/id;
+262 tests). The fit is PROVEN — see `lib/maude/tests/effects.sx`: artdag's
+optimise passes (fusion, no-op/dead-op elim, identity elim, CSE/idempotent
+dedup) expressed as equations, where the optimised pipeline IS the normal form
+and confluence ⇒ a stable content id. Reimplement Phase-5 optimisation
+declaratively and prove it equivalent to the hand-written `optimize.sx`.
+
+- [ ] `lib/artdag/maude-bridge.sx` — adapter between an effect DAG node and a
+  maude term: `(op, sorted-input-ids, params)` ⟷ `(mau/app op (args...))`.
+  Params become constant subterms; for commutative ops use a maude AC operator
+  so input order is irrelevant (mirror the content-id's order-insensitivity).
+  Round-trip `dag→term→dag` must be identity on canonical form.
+- [ ] `lib/artdag/optimize-rules.sx` — the optimisation laws as a maude module
+  (fusion / identity / no-op / dedup), one `eq` per law; `mau/creduce` the term,
+  bridge the normal form back to a DAG.
+- [ ] Equivalence: assert the maude-optimised DAG == `optimize.sx`'s output on
+  the existing fixtures (same nodes, same content ids) — the rule set must cover
+  at least the hand-written passes.
+- [ ] Confluence / CID-stability check: a syntactic critical-pair / local-
+  confluence checker over the optimisation `eq`s — different rewrite orders must
+  reach the same normal form, else the optimiser is CID-unstable. Full
+  AC-unification is OUT OF SCOPE; check syntactic overlaps + joinability and use
+  `mau/canon` as the joinability oracle for AC laws.
+- [ ] `lib/artdag/tests/maude-optimize.sx` — bridge round-trip, each law,
+  equivalence-with-`optimize.sx`, confluence of the rule set.
+- [ ] (later) cost-directed choice among confluent-equivalent forms; (optional)
+  miniKanren scheduling.
+
+maude is a READ-ONLY consumed substrate (like datalog/persist) — load it, don't
+edit it. Entry points: `mau/parse-module`, `mau/creduce`/`mau/creduce->str`,
+`mau/canon`/`mau/ac-equal?`, `mau/term->maude`, `mau/app`/`mau/const`/`mau/var`
++ accessors. Load order: see `lib/maude/conformance.conf` PRELOADS.
+Gotchas (from building it): `id:` affects matching/canon only, not auto-
+reduction — write explicit identity `eq`s or read `mau/canon`; `mau/match-all`/
+`search` enumerate ALL matches (exponential on many identical AC args — keep
+rule sets small + confluent), single-step rewriting is short-circuit and fast;
+juxtaposition `__`/multi-`_` mixfix unparsed (use explicit infix ops); `.` can't
+be an op token.
+
 ## Progress log
 
 - **Ext: public API facade** (`lib/artdag/api.sx`, total 158/158 unchanged).