diff --git a/lib/datalog/conformance.conf b/lib/datalog/conformance.conf
index af4e41b0..bd9b0612 100644
--- a/lib/datalog/conformance.conf
+++ b/lib/datalog/conformance.conf
@@ -9,6 +9,7 @@ PRELOADS=(
   lib/datalog/unify.sx
   lib/datalog/db.sx
   lib/datalog/builtins.sx
+  lib/datalog/strata.sx
   lib/datalog/eval.sx
 )
 
@@ -19,4 +20,5 @@ SUITES=(
   "eval:lib/datalog/tests/eval.sx:(dl-eval-tests-run!)"
   "builtins:lib/datalog/tests/builtins.sx:(dl-builtins-tests-run!)"
   "semi_naive:lib/datalog/tests/semi_naive.sx:(dl-semi-naive-tests-run!)"
+  "negation:lib/datalog/tests/negation.sx:(dl-negation-tests-run!)"
 )
diff --git a/lib/datalog/eval.sx b/lib/datalog/eval.sx
index 5fb30eb9..45c0fdb9 100644
--- a/lib/datalog/eval.sx
+++ b/lib/datalog/eval.sx
@@ -55,13 +55,24 @@
           results)))))
 
 ;; Naive matcher (for dl-saturate-naive! and dl-query post-saturation).
+(define
+  dl-match-negation
+  (fn
+    (inner db subst)
+    (let
+      ((walked (dl-apply-subst inner subst))
+        (matches (dl-match-positive inner db subst)))
+      (cond
+        ((= (len matches) 0) (list subst))
+        (else (list))))))
+
 (define
   dl-match-lit
   (fn
     (lit db subst)
     (cond
       ((and (dict? lit) (has-key? lit :neg))
-        (error "datalog: negation not yet supported (Phase 7)"))
+        (dl-match-negation (get lit :neg) db subst))
       ((dl-builtin? lit)
         (let
           ((s (dl-eval-builtin lit subst)))
@@ -194,7 +205,7 @@
             (options
               (cond
                 ((and (dict? lit) (has-key? lit :neg))
-                  (error "datalog: negation in semi-naive (Phase 7)"))
+                  (dl-match-negation (get lit :neg) db subst))
                 ((dl-builtin? lit)
                   (let
                     ((s (dl-eval-builtin lit subst)))
@@ -281,14 +292,14 @@
       candidates)))
 
 (define
-  dl-saturate!
+  dl-saturate-rules!
   (fn
-    (db)
+    (db rules)
     (let
       ((delta (dl-snapshot-facts db)))
       (do
         (define
-          dl-sn-step
+          dl-sr-step
           (fn
             ()
             (let
@@ -300,14 +311,50 @@
                     (for-each
                       (fn (cand) (append! pending cand))
                       (dl-collect-rule-candidates rule db delta)))
-                  (dl-rules db))
+                  rules)
                 (dl-commit-candidates! db pending new-delta)
                 (cond
                   ((dl-delta-empty? new-delta) nil)
-                  (else (do (set! delta new-delta) (dl-sn-step))))))))
-        (dl-sn-step)
+                  (else (do (set! delta new-delta) (dl-sr-step))))))))
+        (dl-sr-step)
         db))))
 
+;; Stratified driver: rejects non-stratifiable programs at saturation
+;; time, then iterates strata in increasing order, running semi-naive on
+;; the rules whose head sits in that stratum.
+(define
+  dl-saturate!
+  (fn
+    (db)
+    (let
+      ((err (dl-check-stratifiable db)))
+      (cond
+        ((not (nil? err)) (error (str "dl-saturate!: " err)))
+        (else
+          (let
+            ((strata (dl-compute-strata db)))
+            (let
+              ((grouped (dl-group-rules-by-stratum db strata)))
+              (let
+                ((groups (get grouped :groups))
+                  (max-s (get grouped :max)))
+                (do
+                  (define
+                    dl-strat-loop
+                    (fn
+                      (s)
+                      (when
+                        (<= s max-s)
+                        (let
+                          ((sk (str s)))
+                          (do
+                            (when
+                              (has-key? groups sk)
+                              (dl-saturate-rules! db (get groups sk)))
+                            (dl-strat-loop (+ s 1)))))))
+                  (dl-strat-loop 0)
+                  db)))))))))
+
 ;; ── Querying ─────────────────────────────────────────────────────
 
 (define
diff --git a/lib/datalog/scoreboard.json b/lib/datalog/scoreboard.json
index 12f28784..54be5726 100644
--- a/lib/datalog/scoreboard.json
+++ b/lib/datalog/scoreboard.json
@@ -1,15 +1,16 @@
 {
   "lang": "datalog",
-  "total_passed": 114,
+  "total_passed": 124,
   "total_failed": 0,
-  "total": 114,
+  "total": 124,
   "suites": [
     {"name":"tokenize","passed":26,"failed":0,"total":26},
     {"name":"parse","passed":18,"failed":0,"total":18},
     {"name":"unify","passed":28,"failed":0,"total":28},
     {"name":"eval","passed":15,"failed":0,"total":15},
     {"name":"builtins","passed":19,"failed":0,"total":19},
-    {"name":"semi_naive","passed":8,"failed":0,"total":8}
+    {"name":"semi_naive","passed":8,"failed":0,"total":8},
+    {"name":"negation","passed":10,"failed":0,"total":10}
   ],
-  "generated": "2026-05-08T08:12:42+00:00"
+  "generated": "2026-05-08T08:20:41+00:00"
 }
diff --git a/lib/datalog/scoreboard.md b/lib/datalog/scoreboard.md
index cac00351..802305ab 100644
--- a/lib/datalog/scoreboard.md
+++ b/lib/datalog/scoreboard.md
@@ -1,6 +1,6 @@
 # datalog scoreboard
 
-**114 / 114 passing** (0 failure(s)).
+**124 / 124 passing** (0 failure(s)).
 
 | Suite | Passed | Total | Status |
 |-------|--------|-------|--------|
@@ -10,3 +10,4 @@
 | eval | 15 | 15 | ok |
 | builtins | 19 | 19 | ok |
 | semi_naive | 8 | 8 | ok |
+| negation | 10 | 10 | ok |
diff --git a/lib/datalog/strata.sx b/lib/datalog/strata.sx
new file mode 100644
index 00000000..b5d08347
--- /dev/null
+++ b/lib/datalog/strata.sx
@@ -0,0 +1,297 @@
+;; lib/datalog/strata.sx — dependency graph, SCC analysis, stratum assignment.
+;;
+;; A program is stratifiable iff no cycle in its dependency graph passes
+;; through a negative edge. The stratum of relation R is the depth at which
+;; R can first be evaluated:
+;;
+;;   stratum(R) = max over edges (R → S) of:
+;;       stratum(S)         if the edge is positive
+;;       stratum(S) + 1     if the edge is negative
+;;
+;; All relations in the same SCC share a stratum (and the SCC must have only
+;; positive internal edges, else the program is non-stratifiable).
+
+;; Build dep graph: dict {head-rel-name -> ({:rel str :neg bool} ...)}.
+(define
+  dl-build-dep-graph
+  (fn
+    (db)
+    (let ((g {}))
+      (do
+        (for-each
+          (fn
+            (rule)
+            (let
+              ((head-rel (dl-rel-name (get rule :head))))
+              (when
+                (not (nil? head-rel))
+                (do
+                  (when
+                    (not (has-key? g head-rel))
+                    (dict-set! g head-rel (list)))
+                  (let ((existing (get g head-rel)))
+                    (for-each
+                      (fn
+                        (lit)
+                        (let
+                          ((target
+                             (cond
+                               ((and (dict? lit) (has-key? lit :neg))
+                                 (dl-rel-name (get lit :neg)))
+                               ((dl-builtin? lit) nil)
+                               ((and (list? lit) (> (len lit) 0))
+                                 (dl-rel-name lit))
+                               (else nil)))
+                            (neg?
+                              (and (dict? lit) (has-key? lit :neg))))
+                          (when
+                            (not (nil? target))
+                            (append!
+                              existing
+                              {:rel target :neg neg?}))))
+                      (get rule :body)))))))
+          (dl-rules db))
+        g))))
+
+;; All relations referenced — heads of rules + EDB names + body relations.
+(define
+  dl-all-relations
+  (fn
+    (db)
+    (let ((seen (list)))
+      (do
+        (for-each
+          (fn
+            (k)
+            (when (not (dl-member-string? k seen)) (append! seen k)))
+          (keys (get db :facts)))
+        (for-each
+          (fn
+            (rule)
+            (do
+              (let ((h (dl-rel-name (get rule :head))))
+                (when
+                  (and (not (nil? h)) (not (dl-member-string? h seen)))
+                  (append! seen h)))
+              (for-each
+                (fn
+                  (lit)
+                  (let
+                    ((t
+                       (cond
+                         ((and (dict? lit) (has-key? lit :neg))
+                           (dl-rel-name (get lit :neg)))
+                         ((dl-builtin? lit) nil)
+                         ((and (list? lit) (> (len lit) 0))
+                           (dl-rel-name lit))
+                         (else nil))))
+                    (when
+                      (and (not (nil? t)) (not (dl-member-string? t seen)))
+                      (append! seen t))))
+                (get rule :body))))
+          (dl-rules db))
+        seen))))
+
+;; reach: dict {from: dict {to: edge-info}} where edge-info is
+;;   {:any bool :neg bool}
+;; meaning "any path from `from` to `to`" and "exists a negative-passing
+;; path from `from` to `to`".
+;;
+;; Floyd-Warshall over the dep graph. The 'neg' flag propagates through
+;; concatenation: if any edge along the path is negative, the path's
+;; flag is true.
+(define
+  dl-build-reach
+  (fn
+    (graph nodes)
+    (let ((reach {}))
+      (do
+        (for-each
+          (fn (n) (dict-set! reach n {}))
+          nodes)
+        (for-each
+          (fn
+            (head)
+            (when
+              (has-key? graph head)
+              (for-each
+                (fn
+                  (edge)
+                  (let
+                    ((target (get edge :rel)) (n (get edge :neg)))
+                    (let ((row (get reach head)))
+                      (cond
+                        ((has-key? row target)
+                          (let ((cur (get row target)))
+                            (dict-set!
+                              row
+                              target
+                              {:any true :neg (or n (get cur :neg))})))
+                        (else
+                          (dict-set! row target {:any true :neg n}))))))
+                (get graph head))))
+          nodes)
+        (for-each
+          (fn
+            (k)
+            (for-each
+              (fn
+                (i)
+                (let ((row-i (get reach i)))
+                  (when
+                    (has-key? row-i k)
+                    (let ((ik (get row-i k)) (row-k (get reach k)))
+                      (for-each
+                        (fn
+                          (j)
+                          (when
+                            (has-key? row-k j)
+                            (let ((kj (get row-k j)))
+                              (let
+                                ((combined-neg (or (get ik :neg) (get kj :neg))))
+                                (cond
+                                  ((has-key? row-i j)
+                                    (let ((cur (get row-i j)))
+                                      (dict-set!
+                                        row-i
+                                        j
+                                        {:any true
+                                         :neg (or combined-neg (get cur :neg))})))
+                                  (else
+                                    (dict-set!
+                                      row-i
+                                      j
+                                      {:any true :neg combined-neg})))))))
+                        nodes)))))
+              nodes))
+          nodes)
+        reach))))
+
+;; Returns nil on success, or error message string on failure.
+(define
+  dl-check-stratifiable
+  (fn
+    (db)
+    (let
+      ((graph (dl-build-dep-graph db))
+        (nodes (dl-all-relations db)))
+      (let ((reach (dl-build-reach graph nodes)) (err nil))
+        (do
+          (for-each
+            (fn
+              (rule)
+              (when
+                (nil? err)
+                (let ((head-rel (dl-rel-name (get rule :head))))
+                  (for-each
+                    (fn
+                      (lit)
+                      (when
+                        (and (dict? lit) (has-key? lit :neg))
+                        (let ((tgt (dl-rel-name (get lit :neg))))
+                          (when
+                            (and (not (nil? tgt))
+                                 (dl-reach-cycle? reach head-rel tgt))
+                            (set!
+                              err
+                              (str "non-stratifiable: relation " head-rel
+                                   " transitively depends through negation on "
+                                   tgt
+                                   " which depends back on " head-rel))))))
+                    (get rule :body)))))
+            (dl-rules db))
+          err)))))
+
+(define
+  dl-reach-cycle?
+  (fn
+    (reach a b)
+    (and
+      (dl-reach-row-has? reach b a)
+      (dl-reach-row-has? reach a b))))
+
+(define
+  dl-reach-row-has?
+  (fn
+    (reach from to)
+    (let ((row (get reach from)))
+      (and (not (nil? row)) (has-key? row to)))))
+
+;; Compute stratum per relation. Iteratively propagate from EDB roots.
+;; Uses the per-relation max-stratum-of-deps formula. Stops when stable.
+(define
+  dl-compute-strata
+  (fn
+    (db)
+    (let
+      ((graph (dl-build-dep-graph db))
+        (nodes (dl-all-relations db))
+        (strata {}))
+      (do
+        (for-each (fn (n) (dict-set! strata n 0)) nodes)
+        (let ((changed true))
+          (do
+            (define
+              dl-cs-loop
+              (fn
+                ()
+                (when
+                  changed
+                  (do
+                    (set! changed false)
+                    (for-each
+                      (fn
+                        (head)
+                        (when
+                          (has-key? graph head)
+                          (for-each
+                            (fn
+                              (edge)
+                              (let
+                                ((tgt (get edge :rel))
+                                  (n (get edge :neg)))
+                                (let
+                                  ((tgt-strat
+                                     (if (has-key? strata tgt)
+                                       (get strata tgt) 0))
+                                    (cur (get strata head)))
+                                  (let
+                                    ((needed
+                                       (if n (+ tgt-strat 1) tgt-strat)))
+                                    (when
+                                      (> needed cur)
+                                      (do
+                                        (dict-set! strata head needed)
+                                        (set! changed true)))))))
+                            (get graph head))))
+                      nodes)
+                    (dl-cs-loop)))))
+            (dl-cs-loop)))
+        strata))))
+
+;; Group rules by their head's stratum. Returns dict {stratum-int -> rules}.
+(define
+  dl-group-rules-by-stratum
+  (fn
+    (db strata)
+    (let ((groups {}) (max-s 0))
+      (do
+        (for-each
+          (fn
+            (rule)
+            (let
+              ((head-rel (dl-rel-name (get rule :head))))
+              (let
+                ((s (if (has-key? strata head-rel)
+                       (get strata head-rel) 0)))
+                (do
+                  (when (> s max-s) (set! max-s s))
+                  (let
+                    ((sk (str s)))
+                    (do
+                      (when
+                        (not (has-key? groups sk))
+                        (dict-set! groups sk (list)))
+                      (append! (get groups sk) rule)))))))
+          (dl-rules db))
+        {:groups groups :max max-s}))))
diff --git a/lib/datalog/tests/negation.sx b/lib/datalog/tests/negation.sx
new file mode 100644
index 00000000..e4de6207
--- /dev/null
+++ b/lib/datalog/tests/negation.sx
@@ -0,0 +1,231 @@
+;; lib/datalog/tests/negation.sx — stratified negation tests.
+
+(define dl-nt-pass 0)
+(define dl-nt-fail 0)
+(define dl-nt-failures (list))
+
+(define
+  dl-nt-deep=?
+  (fn
+    (a b)
+    (cond
+      ((and (list? a) (list? b))
+        (and (= (len a) (len b)) (dl-nt-deq-l? a b 0)))
+      ((and (dict? a) (dict? b))
+        (let ((ka (keys a)) (kb (keys b)))
+          (and (= (len ka) (len kb)) (dl-nt-deq-d? a b ka 0))))
+      ((and (number? a) (number? b)) (= a b))
+      (else (equal? a b)))))
+
+(define
+  dl-nt-deq-l?
+  (fn
+    (a b i)
+    (cond
+      ((>= i (len a)) true)
+      ((not (dl-nt-deep=? (nth a i) (nth b i))) false)
+      (else (dl-nt-deq-l? a b (+ i 1))))))
+
+(define
+  dl-nt-deq-d?
+  (fn
+    (a b ka i)
+    (cond
+      ((>= i (len ka)) true)
+      ((let ((k (nth ka i)))
+         (not (dl-nt-deep=? (get a k) (get b k))))
+        false)
+      (else (dl-nt-deq-d? a b ka (+ i 1))))))
+
+(define
+  dl-nt-set=?
+  (fn
+    (a b)
+    (and
+      (= (len a) (len b))
+      (dl-nt-subset? a b)
+      (dl-nt-subset? b a))))
+
+(define
+  dl-nt-subset?
+  (fn
+    (xs ys)
+    (cond
+      ((= (len xs) 0) true)
+      ((not (dl-nt-contains? ys (first xs))) false)
+      (else (dl-nt-subset? (rest xs) ys)))))
+
+(define
+  dl-nt-contains?
+  (fn
+    (xs target)
+    (cond
+      ((= (len xs) 0) false)
+      ((dl-nt-deep=? (first xs) target) true)
+      (else (dl-nt-contains? (rest xs) target)))))
+
+(define
+  dl-nt-test!
+  (fn
+    (name got expected)
+    (if
+      (dl-nt-deep=? got expected)
+      (set! dl-nt-pass (+ dl-nt-pass 1))
+      (do
+        (set! dl-nt-fail (+ dl-nt-fail 1))
+        (append!
+          dl-nt-failures
+          (str
+            name
+            "\n    expected: " expected
+            "\n    got:      " got))))))
+
+(define
+  dl-nt-test-set!
+  (fn
+    (name got expected)
+    (if
+      (dl-nt-set=? got expected)
+      (set! dl-nt-pass (+ dl-nt-pass 1))
+      (do
+        (set! dl-nt-fail (+ dl-nt-fail 1))
+        (append!
+          dl-nt-failures
+          (str
+            name
+            "\n    expected (set): " expected
+            "\n    got:            " got))))))
+
+(define
+  dl-nt-throws?
+  (fn
+    (thunk)
+    (let
+      ((threw false))
+      (do
+        (guard
+          (e (#t (set! threw true)))
+          (thunk))
+        threw))))
+
+(define
+  dl-nt-run-all!
+  (fn
+    ()
+    (do
+      ;; Negation against EDB-only relation.
+      (dl-nt-test-set! "not against EDB"
+        (dl-query
+          (dl-program
+            "p(1). p(2). p(3). r(2).
+             q(X) :- p(X), not(r(X)).")
+          (list (quote q) (quote X)))
+        (list {:X 1} {:X 3}))
+
+      ;; Negation against derived relation — needs stratification.
+      (dl-nt-test-set! "not against derived rel"
+        (dl-query
+          (dl-program
+            "p(1). p(2). p(3). s(2).
+             r(X) :- s(X).
+             q(X) :- p(X), not(r(X)).")
+          (list (quote q) (quote X)))
+        (list {:X 1} {:X 3}))
+
+      ;; Two-step strata: r derives via s; q derives via not r.
+      (dl-nt-test-set! "two-step strata"
+        (dl-query
+          (dl-program
+            "node(a). node(b). node(c). node(d).
+             edge(a, b). edge(b, c). edge(c, a).
+             reach(X, Y) :- edge(X, Y).
+             reach(X, Z) :- edge(X, Y), reach(Y, Z).
+             unreachable(X) :- node(X), not(reach(a, X)).")
+          (list (quote unreachable) (quote X)))
+        (list {:X (quote d)}))
+
+      ;; Combine negation with arithmetic and comparison.
+      (dl-nt-test-set! "negation with arithmetic"
+        (dl-query
+          (dl-program
+            "n(1). n(2). n(3). n(4). n(5). odd(1). odd(3). odd(5).
+             even(X) :- n(X), not(odd(X)).")
+          (list (quote even) (quote X)))
+        (list {:X 2} {:X 4}))
+
+      ;; Empty negation result.
+      (dl-nt-test-set! "negation always succeeds"
+        (dl-query
+          (dl-program
+            "p(1). p(2). q(X) :- p(X), not(r(X)).")
+          (list (quote q) (quote X)))
+        (list {:X 1} {:X 2}))
+
+      ;; Negation always fails.
+      (dl-nt-test-set! "negation always fails"
+        (dl-query
+          (dl-program
+            "p(1). p(2). r(1). r(2). q(X) :- p(X), not(r(X)).")
+          (list (quote q) (quote X)))
+        (list))
+
+      ;; Stratifiability checks.
+      (dl-nt-test! "non-stratifiable rejected"
+        (dl-nt-throws?
+          (fn ()
+            (let ((db (dl-make-db)))
+              (do
+                (dl-add-rule!
+                  db
+                  {:head (list (quote p) (quote X))
+                   :body (list (list (quote q) (quote X))
+                               {:neg (list (quote r) (quote X))})})
+                (dl-add-rule!
+                  db
+                  {:head (list (quote r) (quote X))
+                   :body (list (list (quote p) (quote X)))})
+                (dl-add-fact! db (list (quote q) 1))
+                (dl-saturate! db)))))
+        true)
+
+      (dl-nt-test! "stratifiable accepted"
+        (dl-nt-throws?
+          (fn ()
+            (dl-program
+              "p(1). p(2). r(2).
+               q(X) :- p(X), not(r(X)).")))
+        false)
+
+      ;; Multi-stratum chain.
+      (dl-nt-test-set! "three-level strata"
+        (dl-query
+          (dl-program
+            "a(1). a(2). a(3). a(4).
+             b(X) :- a(X), not(c(X)).
+             c(X) :- d(X).
+             d(2).
+             d(4).")
+          (list (quote b) (quote X)))
+        (list {:X 1} {:X 3}))
+
+      ;; Safety violation: negation refers to unbound var.
+      (dl-nt-test! "negation safety violation"
+        (dl-nt-throws?
+          (fn ()
+            (dl-program
+              "p(1). q(X) :- p(X), not(r(Y)).")))
+        true))))
+
+(define
+  dl-negation-tests-run!
+  (fn
+    ()
+    (do
+      (set! dl-nt-pass 0)
+      (set! dl-nt-fail 0)
+      (set! dl-nt-failures (list))
+      (dl-nt-run-all!)
+      {:passed dl-nt-pass
+       :failed dl-nt-fail
+       :total (+ dl-nt-pass dl-nt-fail)
+       :failures dl-nt-failures})))
diff --git a/plans/datalog-on-sx.md b/plans/datalog-on-sx.md
index aa7dd632..cc92ddbf 100644
--- a/plans/datalog-on-sx.md
+++ b/plans/datalog-on-sx.md
@@ -162,17 +162,27 @@ large graphs.
       reachability query from a single root.
 
 ### Phase 7 — stratified negation
-- [ ] Dependency graph analysis: which relations depend on which (positively or negatively)
-- [ ] Stratification check: error if negation is in a cycle (non-stratifiable program)
-- [ ] `dl-stratify db` → SCC analysis → stratum ordering
-- [ ] Evaluation: process strata in order — lower stratum fully computed
-      before using its complement in a higher stratum
-- [ ] `not(P)` in rule body: at evaluation time, check P is NOT in the
-      derived EDB
-- [ ] Safety extension: head vars in negative literals must also appear in
-      some positive body literal of the same rule
-- [ ] Tests: non-member (`not(member(X,L))`), colored-graph
-      (`not(same-color(X,Y))`), stratification error detection
+- [x] Dependency graph: `dl-build-dep-graph db` returns `{head -> ({:rel
+      :neg} ...)}`. Built-ins drop out (they're not relations).
+- [x] Reachability via Floyd-Warshall in `dl-build-reach`; cycles
+      detected by `reach[A][B] && reach[B][A]`. Programs are
+      non-stratifiable iff any negative dependency falls inside an SCC.
+      `dl-check-stratifiable` returns nil on success or a clear message.
+- [x] `dl-compute-strata` propagates stratum numbers iteratively:
+      `stratum(R) = max over deps of (stratum(dep) + (1 if negated else 0))`.
+- [x] Saturator refactor: `dl-saturate-rules! db rules` is the semi-
+      naive worker; `dl-saturate! db` rejects non-stratifiable programs,
+      groups rules by head's stratum, and runs the worker on each
+      stratum in increasing order.
+- [x] `not(P)` in body: `dl-match-negation` walks the inner literal
+      under the current subst and uses `dl-match-positive` — succeeds
+      iff zero matches. Order-aware safety in `dl-rule-check-safety`
+      (already present from Phase 4) requires negation vars to be
+      bound by an earlier positive literal.
+- [x] Tests in `lib/datalog/tests/negation.sx` (10): EDB and IDB
+      negation, two-step strata, multi-level strata, with-arithmetic,
+      empty-result and always-fail cases, non-stratifiability
+      rejection, and a negation safety violation.
 
 ### Phase 8 — aggregation (Datalog+)
 - [ ] `count(X, Goal)` → number of distinct X satisfying Goal
@@ -220,6 +230,19 @@ large graphs.
 
 _Newest first._
 
+- 2026-05-08 — Phase 7 done (Phase 6 magic sets deferred — opt-in,
+  semi-naive default suffices for current test suite). New
+  `lib/datalog/strata.sx` (~290 LOC): dep graph build, Floyd-Warshall
+  reachability, SCC-via-mutual-reachability for non-stratifiability
+  detection, iterative stratum computation, rule grouping by head
+  stratum. eval.sx split: `dl-saturate-rules!` is the per-rule-set
+  semi-naive worker, `dl-saturate!` is now the stratified driver
+  (errors out on non-stratifiable programs). `dl-match-negation` in
+  eval.sx: succeeds iff inner positive match is empty. Stratum-keyed
+  dicts use `(str s)` since SX dicts only accept string/keyword keys.
+  10 negation tests cover EDB/IDB negation, multi-level strata,
+  non-stratifiability rejection, and a negation safety violation.
+
 - 2026-05-08 — Phase 5 done. `lib/datalog/eval.sx` rewritten to
   semi-naive default. `dl-saturate!` tracks a per-relation delta and
   on each iteration walks every positive body position substituting