diff --git a/lib/prolog/tests/programs/append.pl b/lib/prolog/tests/programs/append.pl
new file mode 100644
index 00000000..938666e6
--- /dev/null
+++ b/lib/prolog/tests/programs/append.pl
@@ -0,0 +1,5 @@
+%% append/3 — list concatenation, classic Prolog
+%% Two clauses: empty-prefix base case + recursive cons-prefix.
+%% Bidirectional — works in all modes: build, check, split.
+append([], L, L).
+append([H|T], L, [H|R]) :- append(T, L, R).
diff --git a/lib/prolog/tests/programs/append.sx b/lib/prolog/tests/programs/append.sx
new file mode 100644
index 00000000..bc3fab58
--- /dev/null
+++ b/lib/prolog/tests/programs/append.sx
@@ -0,0 +1,114 @@
+;; lib/prolog/tests/programs/append.sx — append/3 test runner
+;;
+;; Mirrors the Prolog source in append.pl (embedded as a string here because
+;; the SX runtime has no file-read primitive yet).
+
+(define pl-ap-test-count 0)
+(define pl-ap-test-pass 0)
+(define pl-ap-test-fail 0)
+(define pl-ap-test-failures (list))
+
+(define
+  pl-ap-test!
+  (fn
+    (name got expected)
+    (begin
+      (set! pl-ap-test-count (+ pl-ap-test-count 1))
+      (if
+        (= got expected)
+        (set! pl-ap-test-pass (+ pl-ap-test-pass 1))
+        (begin
+          (set! pl-ap-test-fail (+ pl-ap-test-fail 1))
+          (append!
+            pl-ap-test-failures
+            (str name "\n    expected: " expected "\n    got:      " got)))))))
+
+(define
+  pl-ap-term-to-sx
+  (fn
+    (t)
+    (cond
+      ((pl-num? t) (pl-num-val t))
+      ((pl-atom? t) (pl-atom-name t))
+      (true (list :complex)))))
+
+(define
+  pl-ap-list-walked
+  (fn
+    (w)
+    (cond
+      ((and (pl-atom? w) (= (pl-atom-name w) "[]")) (list))
+      ((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
+        (cons
+          (pl-ap-term-to-sx (first (pl-args w)))
+          (pl-ap-list-walked (nth (pl-args w) 1))))
+      (true (list :not-list)))))
+
+(define pl-ap-list-to-sx (fn (t) (pl-ap-list-walked (pl-walk-deep t))))
+
+(define
+  pl-ap-goal
+  (fn
+    (src env)
+    (pl-instantiate (nth (first (pl-parse (str "g :- " src "."))) 2) env)))
+
+(define
+  pl-ap-prog-src
+  "append([], L, L). append([H|T], L, [H|R]) :- append(T, L, R).")
+
+(define pl-ap-db (pl-mk-db))
+
+(pl-db-load! pl-ap-db (pl-parse pl-ap-prog-src))
+
+(define pl-ap-env-1 {})
+(define pl-ap-goal-1 (pl-ap-goal "append([], [a, b], X)" pl-ap-env-1))
+(pl-solve-once! pl-ap-db pl-ap-goal-1 (pl-mk-trail))
+
+(pl-ap-test!
+  "append([], [a, b], X) → X = [a, b]"
+  (pl-ap-list-to-sx (dict-get pl-ap-env-1 "X"))
+  (list "a" "b"))
+
+(define pl-ap-env-2 {})
+(define pl-ap-goal-2 (pl-ap-goal "append([1, 2], [3, 4], X)" pl-ap-env-2))
+(pl-solve-once! pl-ap-db pl-ap-goal-2 (pl-mk-trail))
+
+(pl-ap-test!
+  "append([1, 2], [3, 4], X) → X = [1, 2, 3, 4]"
+  (pl-ap-list-to-sx (dict-get pl-ap-env-2 "X"))
+  (list 1 2 3 4))
+
+(pl-ap-test!
+  "append([1], [2, 3], [1, 2, 3]) succeeds"
+  (pl-solve-once!
+    pl-ap-db
+    (pl-ap-goal "append([1], [2, 3], [1, 2, 3])" {})
+    (pl-mk-trail))
+  true)
+
+(pl-ap-test!
+  "append([1, 2], [3], [1, 2, 4]) fails"
+  (pl-solve-once!
+    pl-ap-db
+    (pl-ap-goal "append([1, 2], [3], [1, 2, 4])" {})
+    (pl-mk-trail))
+  false)
+
+(pl-ap-test!
+  "append(X, Y, [1, 2, 3]) backtracks 4 times"
+  (pl-solve-count!
+    pl-ap-db
+    (pl-ap-goal "append(X, Y, [1, 2, 3])" {})
+    (pl-mk-trail))
+  4)
+
+(define pl-ap-env-6 {})
+(define pl-ap-goal-6 (pl-ap-goal "append(X, [3], [1, 2, 3])" pl-ap-env-6))
+(pl-solve-once! pl-ap-db pl-ap-goal-6 (pl-mk-trail))
+
+(pl-ap-test!
+  "append(X, [3], [1, 2, 3]) deduces X = [1, 2]"
+  (pl-ap-list-to-sx (dict-get pl-ap-env-6 "X"))
+  (list 1 2))
+
+(define pl-append-tests-run! (fn () {:failed pl-ap-test-fail :passed pl-ap-test-pass :total pl-ap-test-count :failures pl-ap-test-failures}))
diff --git a/plans/prolog-on-sx.md b/plans/prolog-on-sx.md
index 5cf35264..4ee19ea1 100644
--- a/plans/prolog-on-sx.md
+++ b/plans/prolog-on-sx.md
@@ -56,7 +56,7 @@ Representation choices (finalise in phase 1, document here):
 - [x] Built-ins: `=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2` inside `;`, `call/1`, `write/1`, `nl/0` — all 11 done. `write/1` and `nl/0` use a global `pl-output-buffer` string + `pl-output-clear!` for testability; `pl-format-term` walks deep then renders atoms/nums/strs/compounds/vars (var → `_<id>`). Note: cut-transparency via `;` not testable yet without operator support — `;(,(a,!), b)` parser-rejects because `,` is body-operator-only; revisit in phase 4.
 - [x] Arithmetic `is/2` with `+ - * / mod abs` — `pl-eval-arith` walks deep, recurses on compounds, dispatches on functor; binary `+ - * / mod`, binary AND unary `-`, unary `abs`. `is/2` evaluates RHS, wraps as `("num" v)`, unifies via `pl-solve-eq!`. 11 tests cover each op + nested + ground LHS match/mismatch + bound-var-on-RHS chain.
 - [ ] Classic programs in `lib/prolog/tests/programs/`:
-  - [ ] `append.pl` — list append (with backtracking)
+  - [x] `append.pl` — list append (with backtracking) — `lib/prolog/tests/programs/append.{pl,sx}`. 6 tests cover: build (`append([], L, X)`, `append([1,2], [3,4], X)`), check ground match/mismatch, full split-backtracking (`append(X, Y, [1,2,3])` → 4 solutions), single-deduce (`append(X, [3], [1,2,3])` → X=[1,2]).
   - [ ] `reverse.pl` — naive reverse
   - [ ] `member.pl` — generate all solutions via backtracking
   - [ ] `nqueens.pl` — 8-queens
@@ -88,6 +88,7 @@ Representation choices (finalise in phase 1, document here):
 
 _Newest first. Agent appends on every commit._
 
+- 2026-04-25 — `append.pl` first classic program. `lib/prolog/tests/programs/append.pl` is the canonical 2-clause source; `append.sx` embeds the source as a string (no file-read primitive in SX yet) and runs 6 tests covering build, check, full split-backtrack (4 solutions), and deduction modes. Helpers `pl-ap-list-to-sx` / `pl-ap-term-to-sx` convert deep-walked Prolog lists (`("compound" "." (h t))` / `("atom" "[]")`) to SX lists for structural assertion. Total 154 (+6).
 - 2026-04-25 — `is/2` arithmetic landed. `pl-eval-arith` recursively evaluates ground RHS expressions (binary `+ - * /`, `mod`; binary+unary `-`; unary `abs`); `is/2` wraps the value as `("num" v)` and unifies via `pl-solve-eq!`, so it works in all three modes — bind unbound LHS, check ground LHS for equality, propagate from earlier var bindings on RHS. 11 tests, total 148 (+11). Without operator support, expressions must be written prefix: `is(X, +(2, *(3, 4)))`.
 - 2026-04-25 — `write/1` + `nl/0` landed using global string buffer (`pl-output-buffer` + `pl-output-clear!` + `pl-output-write!`). `pl-format-term` walks deep + dispatches on atom/num/str/compound/var; `pl-format-args` recursively comma-joins. 7 new tests cover atom/num/compound formatting, conjunction order, var-walk, and `nl`. Built-ins box (`=/2`, `\\=/2`, `true/0`, `fail/0`, `!/0`, `,/2`, `;/2`, `->/2`, `call/1`, `write/1`, `nl/0`) now ticked. Total 137 (+7).
 - 2026-04-25 — `->/2` if-then-else landed (both `;(->(C,T), E)` and standalone `->(C, T)` ≡ `(C -> T ; fail)`). `pl-solve-or!` now special-cases `->` in left arg → `pl-solve-if-then-else!`. Cond runs in a fresh local cut-box (ISO opacity for cut inside cond). Then-branch can backtrack, else-branch can backtrack, but cond commits to first solution. 9 new tests covering both forms, both branches, binding visibility, cond-commit, then-backtrack, else-backtrack. Total 130 (+9).