diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf
index b82e4937..ebd1ae5c 100644
--- a/lib/maude/conformance.conf
+++ b/lib/maude/conformance.conf
@@ -15,6 +15,7 @@ PRELOADS=(
   lib/maude/rewrite.sx
   lib/maude/strategy.sx
   lib/maude/meta.sx
+  lib/maude/pretty.sx
 )
 
 SUITES=(
@@ -25,4 +26,5 @@ SUITES=(
   "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-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/pretty.sx b/lib/maude/pretty.sx
new file mode 100644
index 00000000..0d612988
--- /dev/null
+++ b/lib/maude/pretty.sx
@@ -0,0 +1,82 @@
+;; lib/maude/pretty.sx — mixfix surface-syntax printer.
+;;
+;; term->str renders the internal prefix form (`_+_(s_(X), 0)`); this renders
+;; terms back in Maude mixfix surface syntax (`((s X) + 0)`), driven by the
+;; operator forms in the module signature. Fully parenthesised — unambiguous
+;; rather than minimal. Constants and unknown ops fall back to prefix form.
+
+(define
+  mau/render-forms
+  (fn
+    (m)
+    (let
+      ((tbl {}))
+      (for-each
+        (fn
+          (op)
+          (dict-set! tbl (get op :name) (mau/op-form (get op :name))))
+        (mau/module-ops m))
+      tbl)))
+
+(define
+  mau/render-args
+  (fn
+    (forms args)
+    (cond
+      ((empty? args) "")
+      ((empty? (rest args)) (mau/render-term forms (first args)))
+      (else
+        (str
+          (mau/render-term forms (first args))
+          ", "
+          (mau/render-args forms (rest args)))))))
+
+(define
+  mau/render-term
+  (fn
+    (forms t)
+    (cond
+      ((mau/var? t) (mau/vname t))
+      ((mau/app? t)
+        (let
+          ((form (get forms (mau/op t))) (args (mau/args t)))
+          (cond
+            ((empty? args) (mau/op t))
+            ((and form (= (get form :kind) "infix") (= (len args) 2))
+              (str
+                "("
+                (mau/render-term forms (nth args 0))
+                " "
+                (get form :token)
+                " "
+                (mau/render-term forms (nth args 1))
+                ")"))
+            ((and form (= (get form :kind) "prefix") (= (len args) 1))
+              (str
+                "("
+                (get form :token)
+                " "
+                (mau/render-term forms (first args))
+                ")"))
+            ((and form (= (get form :kind) "postfix") (= (len args) 1))
+              (str
+                "("
+                (mau/render-term forms (first args))
+                " "
+                (get form :token)
+                ")"))
+            (else (str (mau/op t) "(" (mau/render-args forms args) ")")))))
+      (else (str t)))))
+
+(define
+  mau/term->maude
+  (fn (m t) (mau/render-term (mau/render-forms m) t)))
+
+;; reduce / rewrite then render in surface syntax
+(define
+  mau/red->maude
+  (fn (m src) (mau/term->maude m (mau/creduce-term m src))))
+
+(define
+  mau/rew->maude
+  (fn (m src) (mau/term->maude m (mau/rewrite-term m src))))
diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json
index f5ecaf27..57c17a4e 100644
--- a/lib/maude/scoreboard.json
+++ b/lib/maude/scoreboard.json
@@ -1,8 +1,8 @@
 {
   "lang": "maude",
-  "total_passed": 196,
+  "total_passed": 207,
   "total_failed": 0,
-  "total": 196,
+  "total": 207,
   "suites": [
     {"name":"parse","passed":65,"failed":0,"total":65},
     {"name":"reduce","passed":26,"failed":0,"total":26},
@@ -10,7 +10,8 @@
     {"name":"conditional","passed":19,"failed":0,"total":19},
     {"name":"rewrite","passed":21,"failed":0,"total":21},
     {"name":"strategy","passed":19,"failed":0,"total":19},
-    {"name":"meta","passed":18,"failed":0,"total":18}
+    {"name":"meta","passed":18,"failed":0,"total":18},
+    {"name":"pretty","passed":11,"failed":0,"total":11}
   ],
-  "generated": "2026-06-07T15:29:16+00:00"
+  "generated": "2026-06-07T15:31:52+00:00"
 }
diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md
index 82d57830..a7a3dbba 100644
--- a/lib/maude/scoreboard.md
+++ b/lib/maude/scoreboard.md
@@ -1,6 +1,6 @@
 # maude scoreboard
 
-**196 / 196 passing** (0 failure(s)).
+**207 / 207 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -11,3 +11,4 @@
 | rewrite | 21 | 21 | ok |
 | strategy | 19 | 19 | ok |
 | meta | 18 | 18 | ok |
+| pretty | 11 | 11 | ok |
diff --git a/lib/maude/tests/pretty.sx b/lib/maude/tests/pretty.sx
new file mode 100644
index 00000000..c152001d
--- /dev/null
+++ b/lib/maude/tests/pretty.sx
@@ -0,0 +1,50 @@
+;; lib/maude/tests/pretty.sx — mixfix surface-syntax printer.
+
+(define mpp-pass 0)
+(define mpp-fail 0)
+(define mpp-failures (list))
+
+(define
+  mpp-check!
+  (fn
+    (name got expected)
+    (if
+      (= got expected)
+      (set! mpp-pass (+ mpp-pass 1))
+      (do
+        (set! mpp-fail (+ mpp-fail 1))
+        (append!
+          mpp-failures
+          (str name "  expected: " expected "  got: " got))))))
+
+(define
+  mpp-m
+  (mau/parse-module
+    "fmod PEANO is\n  sort Nat .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op _+_ : Nat Nat -> Nat .\n  op _! : Nat -> Nat .\n  op f : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 + Y = Y .\n  eq s X + Y = s (X + Y) .\nendfm"))
+
+(define
+  mpp-render
+  (fn (src) (mau/term->maude mpp-m (mau/parse-term-in mpp-m src))))
+
+(mpp-check! "const" (mpp-render "0") "0")
+(mpp-check! "var" (mau/term->maude mpp-m (mau/var "X" "Nat")) "X")
+(mpp-check! "prefix" (mpp-render "s 0") "(s 0)")
+(mpp-check! "infix" (mpp-render "X + Y") "(X + Y)")
+(mpp-check! "nested" (mpp-render "s X + Y") "((s X) + Y)")
+(mpp-check! "paren" (mpp-render "s (X + Y)") "(s (X + Y))")
+;; postfix: built directly (the parser does not produce postfix applications)
+(mpp-check!
+  "postfix"
+  (mau/term->maude mpp-m (mau/app "_!" (list (mau/var "X" "Nat"))))
+  "(X !)")
+(mpp-check! "funcall" (mpp-render "f(0, s 0)") "f(0, (s 0))")
+(mpp-check! "prefix-form-infix" (mpp-render "_+_(0, 0)") "(0 + 0)")
+
+;; reduce then render in surface syntax
+(mpp-check!
+  "red-surface"
+  (mau/red->maude mpp-m "s 0 + s s 0")
+  "(s (s (s 0)))")
+(mpp-check! "red-zero" (mau/red->maude mpp-m "0 + 0") "0")
+
+(define mau-pretty-tests-run! (fn () {:failures mpp-failures :total (+ mpp-pass mpp-fail) :passed mpp-pass :failed mpp-fail}))
diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md
index fc9eebe8..d2553656 100644
--- a/plans/maude-on-sx.md
+++ b/plans/maude-on-sx.md
@@ -101,6 +101,11 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
 - [x] Build proofs / programs that manipulate Maude programs.
 - [x] Tests: meta-circular interpretation, generic theorem helpers.
 
+### Extensions (post-roadmap, toward the end-state goal)
+- [x] Mixfix surface-syntax printer (`lib/maude/pretty.sx`) — `mau/term->maude`
+  renders the internal prefix form back as Maude mixfix (`((s X) + 0)`),
+  driven by op forms; `mau/red->maude` / `mau/rew->maude`. 11 tests.
+
 ### Phase 8 — Propose `lib/guest/rewriting/`
 - [ ] Extract equational matching engine (the most reusable piece).
 - [ ] Extract normal-form-by-equations infrastructure.