diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf
index 959cb205..e8ca5d13 100644
--- a/lib/maude/conformance.conf
+++ b/lib/maude/conformance.conf
@@ -13,6 +13,7 @@ PRELOADS=(
   lib/maude/conditional.sx
   lib/maude/fire.sx
   lib/maude/rewrite.sx
+  lib/maude/searchpath.sx
   lib/maude/strategy.sx
   lib/maude/meta.sx
   lib/maude/pretty.sx
@@ -25,6 +26,7 @@ SUITES=(
   "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)"
   "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)"
   "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)"
+  "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)"
   "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)"
   "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)"
   "pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)"
diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json
index 0a41a831..ac74ee99 100644
--- a/lib/maude/scoreboard.json
+++ b/lib/maude/scoreboard.json
@@ -1,18 +1,19 @@
 {
   "lang": "maude",
-  "total_passed": 213,
+  "total_passed": 221,
   "total_failed": 0,
-  "total": 213,
+  "total": 221,
   "suites": [
     {"name":"parse","passed":65,"failed":0,"total":65},
     {"name":"reduce","passed":26,"failed":0,"total":26},
     {"name":"matching","passed":28,"failed":0,"total":28},
     {"name":"conditional","passed":19,"failed":0,"total":19},
     {"name":"rewrite","passed":21,"failed":0,"total":21},
+    {"name":"searchpath","passed":8,"failed":0,"total":8},
     {"name":"strategy","passed":19,"failed":0,"total":19},
     {"name":"meta","passed":18,"failed":0,"total":18},
     {"name":"pretty","passed":11,"failed":0,"total":11},
     {"name":"run","passed":6,"failed":0,"total":6}
   ],
-  "generated": "2026-06-07T15:33:57+00:00"
+  "generated": "2026-06-07T15:36:28+00:00"
 }
diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md
index 14b03e2a..66199e2a 100644
--- a/lib/maude/scoreboard.md
+++ b/lib/maude/scoreboard.md
@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**213 / 213 passing** (0 failure(s)).
+**221 / 221 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -9,6 +9,7 @@
 | matching | 28 | 28 | ok |
 | conditional | 19 | 19 | ok |
 | rewrite | 21 | 21 | ok |
+| searchpath | 8 | 8 | ok |
 | strategy | 19 | 19 | ok |
 | meta | 18 | 18 | ok |
 | pretty | 11 | 11 | ok |
diff --git a/lib/maude/searchpath.sx b/lib/maude/searchpath.sx
new file mode 100644
index 00000000..a0d1fe5f
--- /dev/null
+++ b/lib/maude/searchpath.sx
@@ -0,0 +1,96 @@
+;; lib/maude/searchpath.sx — reachability search returning the witness path.
+;;
+;; mau/search (rewrite.sx) answers yes/no. For puzzle solvers you want the
+;; actual sequence of states from start to goal. mau/search-path runs the same
+;; BFS but threads the path so far; it returns the list of canonical states
+;; start..goal (shortest by step count) or nil if unreachable within depth.
+
+(define mau/reverse2 (fn (xs) (mau/rev-acc xs (list))))
+
+(define
+  mau/rev-acc
+  (fn
+    (xs acc)
+    (if (empty? xs) acc (mau/rev-acc (rest xs) (cons (first xs) acc)))))
+
+;; find a frontier path whose current state (its head) matches the goal canon
+(define
+  mau/path-hit
+  (fn
+    (theory frontier goal)
+    (cond
+      ((empty? frontier) nil)
+      ((= (mau/canon theory (first (first frontier))) goal)
+        (first frontier))
+      (else (mau/path-hit theory (rest frontier) goal)))))
+
+(define
+  mau/bfs-path
+  (fn
+    (theory eqs rules frontier seen goal depth)
+    (let
+      ((hit (mau/path-hit theory frontier goal)))
+      (cond
+        ((not (= hit nil)) hit)
+        ((<= depth 0) nil)
+        ((empty? frontier) nil)
+        (else
+          (let
+            ((newf (list)) (newseen seen))
+            (for-each
+              (fn
+                (path)
+                (for-each
+                  (fn
+                    (succ)
+                    (let
+                      ((c (mau/canon theory succ)))
+                      (when
+                        (not (mau/member? c newseen))
+                        (do
+                          (set! newseen (cons c newseen))
+                          (append! newf (cons succ path))))))
+                  (mau/all-successors theory eqs rules (first path))))
+              frontier)
+            (mau/bfs-path
+              theory
+              eqs
+              rules
+              newf
+              newseen
+              goal
+              (- depth 1))))))))
+
+(define
+  mau/search-path
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((theory (mau/build-theory m))
+        (eqs (mau/module-eqs m))
+        (rules (mau/module-rules m)))
+      (let
+        ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel))
+          (goal
+            (mau/canon
+              theory
+              (mau/cnormalize
+                theory
+                eqs
+                (mau/parse-term-in m goal-src)
+                mau/reduce-fuel))))
+        (let
+          ((res (mau/bfs-path theory eqs rules (list (list start)) (list (mau/canon theory start)) goal max-depth)))
+          (if
+            (= res nil)
+            nil
+            (map (fn (t) (mau/canon theory t)) (mau/reverse2 res))))))))
+
+;; number of steps in the shortest solution (nil if unreachable)
+(define
+  mau/search-length
+  (fn
+    (m start-src goal-src max-depth)
+    (let
+      ((p (mau/search-path m start-src goal-src max-depth)))
+      (if (= p nil) nil (- (len p) 1)))))
diff --git a/lib/maude/tests/searchpath.sx b/lib/maude/tests/searchpath.sx
new file mode 100644
index 00000000..7a5fa2bd
--- /dev/null
+++ b/lib/maude/tests/searchpath.sx
@@ -0,0 +1,66 @@
+;; lib/maude/tests/searchpath.sx — search returning the witness path.
+
+(define msp-pass 0)
+(define msp-fail 0)
+(define msp-failures (list))
+
+(define
+  msp-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! msp-pass (+ msp-pass 1))
+      (do
+        (set! msp-fail (+ msp-fail 1))
+        (append!
+          msp-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  msp-ndet
+  (mau/parse-module
+    "mod NDET is\n  sort S .\n  ops a b c d goal : -> S .\n  rl [r1] : a => b .\n  rl [r2] : a => c .\n  rl [r3] : b => d .\n  rl [r4] : c => goal .\nendm"))
+
+;; shortest path a -> c -> goal
+(msp-check!
+  "path-to-goal"
+  (mau/search-path msp-ndet "a" "goal" 5)
+  (list "a" "c" "goal"))
+(msp-check!
+  "path-length"
+  (mau/search-length msp-ndet "a" "goal" 5)
+  2)
+(msp-check!
+  "path-self"
+  (mau/search-path msp-ndet "a" "a" 3)
+  (list "a"))
+(msp-check!
+  "path-one-step"
+  (mau/search-path msp-ndet "a" "b" 3)
+  (list "a" "b"))
+(msp-check!
+  "path-unreachable"
+  (mau/search-path msp-ndet "d" "goal" 5)
+  nil)
+(msp-check!
+  "path-depth-limited"
+  (mau/search-path msp-ndet "a" "goal" 1)
+  nil)
+
+;; a counter that ticks up: path shows each state
+(define
+  msp-walk
+  (mau/parse-module
+    "mod WALK is\n  sort Pos .\n  op z : -> Pos .\n  op s : Pos -> Pos .\n  op p : Pos -> Pos .\n  var X : Pos .\n  rl [step] : p(X) => p(s(X)) .\nendm"))
+
+(msp-check!
+  "walk-path"
+  (mau/search-path msp-walk "p(z)" "p(s(s(z)))" 5)
+  (list "p(z)" "p(s(z))" "p(s(s(z)))"))
+(msp-check!
+  "walk-length"
+  (mau/search-length msp-walk "p(z)" "p(s(s(s(z))))" 6)
+  3)
+
+(define mau-searchpath-tests-run! (fn () {:failures msp-failures :total (+ msp-pass msp-fail) :passed msp-pass :failed msp-fail}))
diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md
index d1cd7e70..d5dda65d 100644
--- a/plans/maude-on-sx.md
+++ b/plans/maude-on-sx.md
@@ -109,6 +109,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
   a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands
   (`... in MOD : TERM` qualifier accepted) and execute them, rendering results
   in surface syntax. Runs an idiomatic `.maude` file end-to-end. 6 tests.
+- [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` /
+  `mau/search-length` return the shortest sequence of states start..goal (the
+  solution moves), not just yes/no. 8 tests.
 
 ### Phase 8 — Propose `lib/guest/rewriting/`
 - [ ] Extract equational matching engine (the most reusable piece).