diff --git a/lib/acl/api.sx b/lib/acl/api.sx
index d0ec64a2..acb8c97b 100644
--- a/lib/acl/api.sx
+++ b/lib/acl/api.sx
@@ -25,7 +25,21 @@
         (set! acl-current-db (acl-build-db (list))))
       acl-current-db)))
 
-;; Public decision against the current db.
+;; Public decision against the current db (pure, no logging).
 (define
   acl/permit?
   (fn (subj act res) (acl-permit? (acl-ensure-db!) subj act res)))
+
+;; Decision-with-proof against the current db. See lib/acl/explain.sx.
+(define
+  acl/explain
+  (fn (subj act res) (acl-explain (acl-ensure-db!) subj act res)))
+
+;; Audited decision: logs the outcome to the append-only audit log and returns
+;; the boolean. See lib/acl/audit.sx.
+(define
+  acl/audit
+  (fn (subj act res) (acl-audit-decide! (acl-ensure-db!) subj act res)))
+
+;; Recent audited decisions (chronological).
+(define acl/audit-tail (fn (n) (acl-audit-tail n)))
diff --git a/lib/acl/audit.sx b/lib/acl/audit.sx
new file mode 100644
index 00000000..506a6786
--- /dev/null
+++ b/lib/acl/audit.sx
@@ -0,0 +1,82 @@
+;; lib/acl/audit.sx — append-only decision log.
+;;
+;; Every decision routed through acl-audit-decide! is appended to an in-memory
+;; log with a monotonic sequence number (no wall-clock — deterministic and
+;; testable; a host can stamp time at the serializer boundary). The log is
+;; append-only: there is no mutate or delete, only append, tail, clear, and
+;; serialize-for-disk.
+
+(define acl-audit-log (list))
+(define acl-audit-seq 0)
+
+(define
+  acl-audit-clear!
+  (fn
+    ()
+    (do (set! acl-audit-log (list)) (set! acl-audit-seq 0) nil)))
+
+;; Append a decision record. Returns the record.
+(define
+  acl-audit-record!
+  (fn
+    (subj act res allowed?)
+    (let
+      ((entry {:allowed? allowed? :act act :subj subj :res res :seq acl-audit-seq}))
+      (do
+        (set! acl-audit-seq (+ acl-audit-seq 1))
+        (append! acl-audit-log entry)
+        entry))))
+
+;; Decide against db, log the outcome, and return the boolean. This is the
+;; audited path; acl-permit? remains the pure, side-effect-free decision.
+(define
+  acl-audit-decide!
+  (fn
+    (db subj act res)
+    (let
+      ((allowed? (acl-permit? db subj act res)))
+      (do (acl-audit-record! subj act res allowed?) allowed?))))
+
+(define acl-audit-count (fn () (len acl-audit-log)))
+
+;; Most recent n entries (in chronological order). n >= log size returns all.
+(define
+  acl-audit-tail
+  (fn
+    (n)
+    (let
+      ((total (len acl-audit-log)))
+      (if
+        (<= total n)
+        acl-audit-log
+        (acl-audit-drop acl-audit-log (- total n))))))
+
+(define
+  acl-audit-drop
+  (fn
+    (xs k)
+    (if (<= k 0) xs (acl-audit-drop (rest xs) (- k 1)))))
+
+;; Serialize the whole log to a disk-ready string: one record per line,
+;; "seq\tsubj\tact\tres\tallowed?". A host writes this; reload is out of scope.
+(define
+  acl-audit-serialize
+  (fn
+    ()
+    (reduce
+      (fn
+        (acc e)
+        (str
+          acc
+          (get e :seq)
+          "\t"
+          (get e :subj)
+          "\t"
+          (get e :act)
+          "\t"
+          (get e :res)
+          "\t"
+          (get e :allowed?)
+          "\n"))
+      ""
+      acl-audit-log)))
diff --git a/lib/acl/conformance.conf b/lib/acl/conformance.conf
index 86dbb133..229fe970 100644
--- a/lib/acl/conformance.conf
+++ b/lib/acl/conformance.conf
@@ -17,10 +17,13 @@ PRELOADS=(
   lib/acl/schema.sx
   lib/acl/facts.sx
   lib/acl/engine.sx
+  lib/acl/explain.sx
+  lib/acl/audit.sx
   lib/acl/api.sx
 )
 
 SUITES=(
   "direct:lib/acl/tests/direct.sx:(acl-direct-tests-run!)"
   "inherit:lib/acl/tests/inherit.sx:(acl-inherit-tests-run!)"
+  "explain:lib/acl/tests/explain.sx:(acl-explain-tests-run!)"
 )
diff --git a/lib/acl/explain.sx b/lib/acl/explain.sx
new file mode 100644
index 00000000..c452e520
--- /dev/null
+++ b/lib/acl/explain.sx
@@ -0,0 +1,125 @@
+;; lib/acl/explain.sx — proof-tree reconstruction over the saturated db.
+;;
+;; lib/datalog/ records derived facts but not their provenance, so the proof is
+;; reconstructed here by goal-directed search over the *saturated* db: for a
+;; ground goal we find the first ACL rule (in rule order) whose body holds, take
+;; the first solution binding its remaining variables, and recurse on each body
+;; literal. Negated literals are recorded as verified `:neg-ok` leaves.
+;;
+;; CANONICAL DERIVATION: the Datalog derivation graph is a DAG (a fact may hold
+;; many ways). We pick ONE canonical proof — first matching rule, first solution
+;; — matching the rule order in lib/acl/engine.sx (direct/EDB rules first). A
+;; depth cap guards against pathological cyclic data producing unbounded search.
+;;
+;; A proof node is one of:
+;;   {:fact <lit> :via "edb"}                       — base EDB fact
+;;   {:fact <lit> :rule <head> :body (<node|negleaf> ...)}  — derived
+;;   {:neg-ok <lit>}                                — negation verified to fail
+;;   {:fact <lit> :truncated true}                  — depth cap hit
+
+(define acl-proof-max-depth 64)
+
+;; Substitute a body literal, descending into {:neg ...} dicts (dl-apply-subst
+;; does not recurse into dicts, which would leak the neg's free vars).
+(define
+  acl-subst-lit
+  (fn
+    (lit s)
+    (if
+      (and (dict? lit) (has-key? lit :neg))
+      {:neg (dl-apply-subst (get lit :neg) s)}
+      (dl-apply-subst lit s))))
+
+(define
+  acl-lit-edb?
+  (fn
+    (lit)
+    (and
+      (list? lit)
+      (> (len lit) 0)
+      (symbol? (first lit))
+      (has-key? acl-edb-arity (symbol->string (first lit))))))
+
+(define
+  acl-subst-zip!
+  (fn
+    (d ks vs)
+    (when
+      (> (len ks) 0)
+      (do
+        (dict-set! d (symbol->string (first ks)) (first vs))
+        (acl-subst-zip! d (rest ks) (rest vs))))))
+
+;; Bind a rule head's variables to a ground goal's arguments (positional).
+(define
+  acl-bind-head
+  (fn
+    (head goal)
+    (let
+      ((d {}))
+      (do (acl-subst-zip! d (rest head) (rest goal)) d))))
+
+(define
+  acl-subst-union
+  (fn
+    (a b)
+    (let
+      ((d {}))
+      (do
+        (for-each (fn (k) (dict-set! d k (get a k))) (keys a))
+        (for-each (fn (k) (dict-set! d k (get b k))) (keys b))
+        d))))
+
+(define acl-prove (fn (db goal) (acl-prove-d db goal 0)))
+
+(define
+  acl-prove-d
+  (fn
+    (db goal depth)
+    (cond
+      ((> depth acl-proof-max-depth) {:truncated true :fact goal})
+      ((acl-lit-edb? goal)
+        (if (> (len (dl-query db goal)) 0) {:via "edb" :fact goal} nil))
+      (else (acl-prove-rules db goal acl-rules depth)))))
+
+(define
+  acl-prove-rules
+  (fn
+    (db goal rules depth)
+    (if
+      (= (len rules) 0)
+      nil
+      (let
+        ((p (dl-rule-from-list (first rules))))
+        (if
+          (= (first (get p :head)) (first goal))
+          (let
+            ((hs (acl-bind-head (get p :head) goal)))
+            (let
+              ((qbody (map (fn (l) (acl-subst-lit l hs)) (get p :body))))
+              (let
+                ((sols (dl-query db qbody)))
+                (if
+                  (> (len sols) 0)
+                  (acl-prove-build db goal p hs (first sols) depth)
+                  (acl-prove-rules db goal (rest rules) depth)))))
+          (acl-prove-rules db goal (rest rules) depth))))))
+
+(define
+  acl-prove-build
+  (fn
+    (db goal p hs sol depth)
+    (let ((full (acl-subst-union hs sol))) {:body (map (fn (l) (let ((g (acl-subst-lit l full))) (if (and (dict? g) (has-key? g :neg)) {:neg-ok (get g :neg)} (acl-prove-d db g (+ depth 1))))) (get p :body)) :rule (get p :head) :fact goal})))
+
+;; Public decision-with-proof. Returns:
+;;   {:allowed? <bool> :proof <node|nil> :reason <eff_deny proof|nil>}
+;; When permitted, :proof is the permit derivation. When denied, :proof is nil
+;; and :reason carries the blocking eff_deny proof if one exists (an explicit or
+;; inherited deny), else nil (simply no grant).
+(define
+  acl-explain
+  (fn
+    (db subj act res)
+    (let
+      ((proof (acl-prove db (list (quote permit) subj act res))))
+      (if (= proof nil) {:allowed? false :proof nil :reason (acl-prove db (list (quote eff_deny) subj act res))} {:allowed? true :proof proof :reason nil}))))
diff --git a/lib/acl/scoreboard.json b/lib/acl/scoreboard.json
index 919e8b91..96c70d5b 100644
--- a/lib/acl/scoreboard.json
+++ b/lib/acl/scoreboard.json
@@ -1,11 +1,12 @@
 {
   "lang": "acl",
-  "total_passed": 54,
+  "total_passed": 89,
   "total_failed": 0,
-  "total": 54,
+  "total": 89,
   "suites": [
     {"name":"direct","passed":24,"failed":0,"total":24},
-    {"name":"inherit","passed":30,"failed":0,"total":30}
+    {"name":"inherit","passed":30,"failed":0,"total":30},
+    {"name":"explain","passed":35,"failed":0,"total":35}
   ],
-  "generated": "2026-06-06T16:35:53+00:00"
+  "generated": "2026-06-06T16:46:37+00:00"
 }
diff --git a/lib/acl/scoreboard.md b/lib/acl/scoreboard.md
index 03601f35..70299462 100644
--- a/lib/acl/scoreboard.md
+++ b/lib/acl/scoreboard.md
@@ -1,8 +1,9 @@
 # acl scoreboard
 
-**54 / 54 passing** (0 failure(s)).
+**89 / 89 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
 | direct | 24 | 24 | ok |
 | inherit | 30 | 30 | ok |
+| explain | 35 | 35 | ok |
diff --git a/lib/acl/tests/explain.sx b/lib/acl/tests/explain.sx
new file mode 100644
index 00000000..a58a740e
--- /dev/null
+++ b/lib/acl/tests/explain.sx
@@ -0,0 +1,316 @@
+;; lib/acl/tests/explain.sx — Phase 3: proof correctness + audit completeness.
+
+(define acl-et-pass 0)
+(define acl-et-fail 0)
+(define acl-et-failures (list))
+
+;; Name-based deep equality. The host `=` compares symbols by interned
+;; identity, which is unstable across substitution/saturation; comparing by
+;; name (as the datalog suite does) makes structural assertions deterministic.
+(define
+  acl-et-eq?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (acl-et-eq-l? a b 0)))
+      ((and (dict? a) (dict? b))
+        (let
+          ((ka (keys a)) (kb (keys b)))
+          (and (= (len ka) (len kb)) (acl-et-eq-d? a b ka 0))))
+      ((and (symbol? a) (symbol? b))
+        (= (symbol->string a) (symbol->string b)))
+      (else (= a b)))))
+
+(define
+  acl-et-eq-l?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (acl-et-eq? (nth a i) (nth b i))) false)
+      (else (acl-et-eq-l? a b (+ i 1))))))
+
+(define
+  acl-et-eq-d?
+  (fn
+    (a b ka i)
+    (cond
+      ((>= i (len ka)) true)
+      ((let ((k (nth ka i))) (not (acl-et-eq? (get a k) (get b k))))
+        false)
+      (else (acl-et-eq-d? a b ka (+ i 1))))))
+
+(define
+  acl-et-check!
+  (fn
+    (name got expected)
+    (if
+      (acl-et-eq? got expected)
+      (set! acl-et-pass (+ acl-et-pass 1))
+      (do
+        (set! acl-et-fail (+ acl-et-fail 1))
+        (append!
+          acl-et-failures
+          (str name "\n    expected: " expected "\n    got:      " got))))))
+
+;; --- proof-tree walkers ---
+
+;; True if EDB fact `target` appears as a base leaf anywhere in the proof.
+(define
+  acl-et-has-leaf?
+  (fn
+    (node target)
+    (cond
+      ((= node nil) false)
+      ((and (dict? node) (has-key? node :via))
+        (acl-et-eq? (get node :fact) target))
+      ((and (dict? node) (has-key? node :body))
+        (acl-et-any-leaf? (get node :body) target))
+      (else false))))
+
+(define
+  acl-et-any-leaf?
+  (fn
+    (nodes target)
+    (cond
+      ((= (len nodes) 0) false)
+      ((acl-et-has-leaf? (first nodes) target) true)
+      (else (acl-et-any-leaf? (rest nodes) target)))))
+
+;; True if the proof records a verified negation (deny did not fire).
+(define
+  acl-et-has-negok?
+  (fn
+    (node)
+    (cond
+      ((= node nil) false)
+      ((and (dict? node) (has-key? node :neg-ok)) true)
+      ((and (dict? node) (has-key? node :body))
+        (acl-et-any-negok? (get node :body)))
+      (else false))))
+
+(define
+  acl-et-any-negok?
+  (fn
+    (nodes)
+    (cond
+      ((= (len nodes) 0) false)
+      ((acl-et-has-negok? (first nodes)) true)
+      (else (acl-et-any-negok? (rest nodes))))))
+
+(define
+  acl-et-run-all!
+  (fn
+    ()
+    (do
+      (let
+        ((db (acl-build-db (list (acl-grant (quote u) (quote read) (quote p))))))
+        (let
+          ((e (acl-explain db (quote u) (quote read) (quote p))))
+          (do
+            (acl-et-check! "direct: allowed?" (get e :allowed?) true)
+            (acl-et-check!
+              "direct: proof root fact"
+              (get (get e :proof) :fact)
+              (list (quote permit) (quote u) (quote read) (quote p)))
+            (acl-et-check!
+              "direct: grant leaf present"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote grant) (quote u) (quote read) (quote p)))
+              true)
+            (acl-et-check!
+              "direct: negation verified"
+              (acl-et-has-negok? (get e :proof))
+              true)
+            (acl-et-check!
+              "direct: reason nil when allowed"
+              (get e :reason)
+              nil))))
+      (let
+        ((db (acl-build-db (list (acl-member-of (quote alice) (quote team)) (acl-member-of (quote team) (quote org)) (acl-grant (quote org) (quote read) (quote doc))))))
+        (let
+          ((e (acl-explain db (quote alice) (quote read) (quote doc))))
+          (do
+            (acl-et-check! "group: allowed?" (get e :allowed?) true)
+            (acl-et-check!
+              "group: member_of alice leaf"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote member_of) (quote alice) (quote team)))
+              true)
+            (acl-et-check!
+              "group: member_of team leaf"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote member_of) (quote team) (quote org)))
+              true)
+            (acl-et-check!
+              "group: grant org leaf at base"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote grant) (quote org) (quote read) (quote doc)))
+              true))))
+      (let
+        ((db (acl-build-db (list (acl-child-of (quote sec) (quote book)) (acl-grant (quote u) (quote read) (quote book))))))
+        (let
+          ((e (acl-explain db (quote u) (quote read) (quote sec))))
+          (do
+            (acl-et-check! "resource: allowed?" (get e :allowed?) true)
+            (acl-et-check!
+              "resource: child_of leaf"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote child_of) (quote sec) (quote book)))
+              true)
+            (acl-et-check!
+              "resource: grant on parent leaf"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote grant) (quote u) (quote read) (quote book)))
+              true))))
+      (let
+        ((db (acl-build-db (list (acl-member-of (quote bob) (quote editor)) (acl-role-grant (quote editor) (quote edit) (quote page1))))))
+        (let
+          ((e (acl-explain db (quote bob) (quote edit) (quote page1))))
+          (do
+            (acl-et-check! "role: allowed?" (get e :allowed?) true)
+            (acl-et-check!
+              "role: member_of leaf"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list (quote member_of) (quote bob) (quote editor)))
+              true)
+            (acl-et-check!
+              "role: role_grant leaf"
+              (acl-et-has-leaf?
+                (get e :proof)
+                (list
+                  (quote role_grant)
+                  (quote editor)
+                  (quote edit)
+                  (quote page1)))
+              true))))
+      (let
+        ((db (acl-build-db (list (acl-grant (quote u) (quote edit) (quote p)) (acl-deny (quote u) (quote edit) (quote p))))))
+        (let
+          ((e (acl-explain db (quote u) (quote edit) (quote p))))
+          (do
+            (acl-et-check! "deny: not allowed" (get e :allowed?) false)
+            (acl-et-check! "deny: no proof" (get e :proof) nil)
+            (acl-et-check!
+              "deny: reason root is eff_deny"
+              (get (get e :reason) :fact)
+              (list (quote eff_deny) (quote u) (quote edit) (quote p)))
+            (acl-et-check!
+              "deny: reason has deny leaf"
+              (acl-et-has-leaf?
+                (get e :reason)
+                (list (quote deny) (quote u) (quote edit) (quote p)))
+              true))))
+      (let
+        ((db (acl-build-db (list (acl-member-of (quote alice) (quote team)) (acl-grant (quote alice) (quote read) (quote doc)) (acl-deny (quote team) (quote read) (quote doc))))))
+        (let
+          ((e (acl-explain db (quote alice) (quote read) (quote doc))))
+          (do
+            (acl-et-check!
+              "inherited deny: not allowed"
+              (get e :allowed?)
+              false)
+            (acl-et-check!
+              "inherited deny: reason has member_of leaf"
+              (acl-et-has-leaf?
+                (get e :reason)
+                (list (quote member_of) (quote alice) (quote team)))
+              true)
+            (acl-et-check!
+              "inherited deny: reason has group deny leaf"
+              (acl-et-has-leaf?
+                (get e :reason)
+                (list (quote deny) (quote team) (quote read) (quote doc)))
+              true))))
+      (let
+        ((db (acl-build-db (list))))
+        (let
+          ((e (acl-explain db (quote u) (quote read) (quote p))))
+          (do
+            (acl-et-check! "no grant: not allowed" (get e :allowed?) false)
+            (acl-et-check! "no grant: proof nil" (get e :proof) nil)
+            (acl-et-check! "no grant: reason nil" (get e :reason) nil))))
+      (let
+        ((db (acl-build-db (list (acl-grant (quote u) (quote read) (quote p)) (acl-deny (quote u) (quote edit) (quote p))))))
+        (do
+          (acl-audit-clear!)
+          (acl-et-check! "audit: starts empty" (acl-audit-count) 0)
+          (acl-et-check!
+            "audit decide allowed returns true"
+            (acl-audit-decide! db (quote u) (quote read) (quote p))
+            true)
+          (acl-et-check!
+            "audit decide denied returns false"
+            (acl-audit-decide! db (quote u) (quote edit) (quote p))
+            false)
+          (acl-audit-decide! db (quote u) (quote comment) (quote p))
+          (acl-et-check!
+            "audit: count after three decisions"
+            (acl-audit-count)
+            3)
+          (acl-et-check!
+            "audit: tail size respects n"
+            (len (acl-audit-tail 2))
+            2)
+          (acl-et-check!
+            "audit: tail returns most recent"
+            (get (first (acl-audit-tail 1)) :act)
+            (quote comment))
+          (acl-et-check!
+            "audit: first record seq is 0"
+            (get (first (acl-audit-tail 3)) :seq)
+            0)
+          (acl-et-check!
+            "audit: allowed flag recorded"
+            (get (first (acl-audit-tail 3)) :allowed?)
+            true)
+          (acl-et-check!
+            "audit: serialize line count"
+            (len (acl-et-lines (acl-audit-serialize)))
+            3)
+          (acl-audit-clear!)
+          (acl-et-check!
+            "audit: clear resets count"
+            (acl-audit-count)
+            0))))))
+
+;; count newline-terminated lines in a serialized log
+(define acl-et-lines (fn (s) (acl-et-count-nl s 0 0)))
+(define
+  acl-et-count-nl
+  (fn
+    (s i n)
+    (if
+      (>= i (len s))
+      (if (= n 0) (list) (acl-et-rangelist n))
+      (acl-et-count-nl
+        s
+        (+ i 1)
+        (if (= (slice s i (+ i 1)) "\n") (+ n 1) n)))))
+(define
+  acl-et-rangelist
+  (fn
+    (n)
+    (if
+      (<= n 0)
+      (list)
+      (cons n (acl-et-rangelist (- n 1))))))
+
+(define
+  acl-explain-tests-run!
+  (fn
+    ()
+    (do
+      (set! acl-et-pass 0)
+      (set! acl-et-fail 0)
+      (set! acl-et-failures (list))
+      (acl-et-run-all!)
+      {:failures acl-et-failures :total (+ acl-et-pass acl-et-fail) :passed acl-et-pass :failed acl-et-fail})))
diff --git a/plans/acl-on-sx.md b/plans/acl-on-sx.md
index d8e531fa..4ee50474 100644
--- a/plans/acl-on-sx.md
+++ b/plans/acl-on-sx.md
@@ -15,7 +15,7 @@ and federation extension. Reuses `lib/datalog/` evaluator and term model where p
 
 ## Status (rolling)
 
-`bash lib/acl/conformance.sh` → **54/54** (Phases 1-2 complete)
+`bash lib/acl/conformance.sh` → **89/89** (Phases 1-3 complete)
 
 ## Ground rules
 
@@ -98,11 +98,27 @@ cyclic membership/containment reaches a fixpoint rather than looping (tested).
 
 ## Phase 3 — Explanation + audit
 
-- [ ] `(acl/explain subj act res)` → `{:allowed? T :proof <tree>}`
-- [ ] proof tree extracts from Datalog's derivation
-- [ ] `lib/acl/audit.sx` — append-only decision log (in-memory + serializer for disk)
-- [ ] `(acl/audit-tail n)` for recent decisions
-- [ ] `lib/acl/tests/explain.sx` — proof correctness, audit completeness
+- [x] `(acl/explain subj act res)` → `{:allowed? T :proof <tree>}`
+- [x] proof tree extracts from Datalog's derivation
+- [x] `lib/acl/audit.sx` — append-only decision log (in-memory + serializer for disk)
+- [x] `(acl/audit-tail n)` for recent decisions
+- [x] `lib/acl/tests/explain.sx` — proof correctness, audit completeness
+
+### proof reconstruction (the choice)
+
+`lib/datalog/` records derived facts but not provenance, so `lib/acl/explain.sx`
+reconstructs the proof by goal-directed search over the *saturated* db: for a
+ground goal, find the first ACL rule (in `acl-rules` order) whose body holds,
+take the first `dl-query` solution binding the rest, recurse on each body
+literal; negated literals become verified `:neg-ok` leaves. The Datalog
+derivation graph is a DAG (a fact may hold many ways) — we pick ONE **canonical
+proof: first-rule, first-solution**, with EDB/direct rules ordered first so
+proofs bottom out quickly. A depth cap (64) guards pathological cyclic data.
+`acl-explain` returns `{:allowed? :proof :reason}`; on denial `:reason` carries
+the blocking `eff_deny` proof (explicit or inherited) when one exists, else nil
+(no grant). Audit log is append-only with monotonic seq numbers (no wall-clock,
+for determinism); `acl-audit-decide!` is the logged path, `acl-permit?` stays
+pure.
 
 ## Phase 4 — Federation
 
@@ -149,11 +165,23 @@ cyclic membership/containment reaches a fixpoint rather than looping (tested).
     ACL-specific (group/resource/role vocabulary); mod-sx will have its own. So
     the `lib/guest/rules/` extraction stays at the build/decide level, not the
     ruleset level.
+- **Phase 3 complete (89/89, +35 explain).** Added `explain.sx` (proof
+  reconstruction, see policy section above), `audit.sx` (append-only log), and
+  extended `api.sx` with `acl/explain`/`acl/audit`/`acl/audit-tail`. No engine
+  changes — explanation reads the same saturated db the decision uses.
+  - **Substrate gotcha:** the host `=` compares symbols by interned identity,
+    which is *unstable* across `dl-query` saturation/substitution within a
+    single image — the same two structurally-equal symbol-lists compared `=`
+    true once and false moments later in the REPL. Conformance runs in a fresh
+    process per suite so it's deterministic there, but test assertions now use a
+    name-based `acl-et-eq?` (compare symbols via `symbol->string`), matching the
+    datalog suite's `dl-api-deep=?` convention. Worth flagging to the kernel
+    owners but out of acl scope.
   - **Tooling note:** sx-tree path-based edit tools (`sx_replace_node`,
     `sx_read_subtree` with a path) ignored the path argument in this worktree
-    (always resolved to index 0 / `[0,..]`). `sx_write_file`, `sx_validate`,
-    `sx_find_all`, `sx_eval` all work; used full-file rewrites instead of path
-    edits.
+    (always resolved to index 0 / `[0,..]`), in BOTH `(a b c)` and `(a,b,c)`
+    forms. `sx_write_file`, `sx_validate`, `sx_find_all`, `sx_summarise`,
+    `sx_eval` all work; used full-file rewrites instead of path edits throughout.
 
 ## Blockers