diff --git a/proof/ROOT b/proof/ROOT
index 7992935..17e9ec5 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -4,6 +4,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Base
     StarForth_Q48_16
     StarForth_Stack_Words
+    StarForth_Double_Words
     StarForth_Arithmetic_Words
     StarForth_Logical_Words
     StarForth_Return_Stack_Words
diff --git a/proof/StarForth_Double_Words.thy b/proof/StarForth_Double_Words.thy
new file mode 100644
index 0000000..cadc0ea
--- /dev/null
+++ b/proof/StarForth_Double_Words.thy
@@ -0,0 +1,206 @@
+theory StarForth_Double_Words
+  imports StarForth_Base
+begin
+
+(* =========================================================================
+   POST-XX: Double-Cell Stack Manipulation Words
+   Mirrors: src/word_source/double_words.c (partial -- see SCOPE below)
+            src/test_runner/modules/double_words_test.c
+
+   SCOPE, decided 2026-08-13: double_words.c has 20 registered words in
+   three categories. Only the first is modeled here:
+
+   1. Pure double-cell DATA-STACK shuffles (2DROP, 2DUP, 2SWAP, 2OVER,
+      2ROT) -- modeled below. These only rearrange data_stack list
+      elements; nothing about their correctness depends on cell's exact
+      representation or on any vm_state field this theory doesn't already
+      track.
+
+   2. Double-cell RETURN-STACK transfer (2>R, 2R>, 2R@) -- NOT modeled.
+      The real C (double_words.c:330-382) branches on
+      "vm->ecw_nesting > 0" (execute_colon_word re-entrancy depth), a VM
+      field that does not exist anywhere in StarForth_Base.thy's
+      vm_state record. Modeling these words correctly requires adding
+      ecw_nesting to vm_state first -- a model-extension decision, not
+      something to add as a side effect of this file.
+
+   3. Double-precision ARITHMETIC (S>D, D+, D-, DNEGATE, DABS, DMAX,
+      DMIN, D<, D=, D0=, D0<, D2*, D2/) -- NOT modeled. The real C
+      implementations (double_words.c:56-250ish) depend on cell_t being
+      a fixed-width (64-bit, "signed long") wrapping integer type --
+      D+/D- explicitly do carry/borrow detection via "unsigned long"
+      arithmetic and wraparound, DNEGATE uses bitwise complement (~) with
+      wraparound. This theory's "type_synonym cell = int" (StarForth_Base)
+      is unbounded/arbitrary-precision, not a fixed-width wrapping type,
+      so none of this carry/wraparound reasoning is even expressible as
+      currently modeled. Correctly formalizing these words needs a
+      foundational decision -- change cell's representation to a 64-bit
+      word type (matching StarForth_Q48_16.thy's own "64 word" approach)
+      or add explicit range side-conditions everywhere -- that ripples
+      into all 23 already-verified theories built on today's plain-int
+      cell. Not decided or attempted here; flagged for a dedicated pass.
+
+   Every word modeled below is a direct structural analog of an
+   already-covered single-cell word in StarForth_Stack_Words.thy (DUP,
+   SWAP, OVER, ROT) or StarForth_Return_Stack_Words.thy, just operating
+   on cell PAIRS instead of single cells. Convention throughout, matching
+   the C comments: a double d is pushed as (dlow dhigh) with dhigh on
+   top -- i.e. in this list's head=TOS convention, a double at the top of
+   stack is "dhigh # dlow # rest".
+
+   None of the C implementations below check ds_full before pushing
+   (confirmed by reading double_words.c in full) -- not modeled here
+   either, to stay faithful to the real source rather than inventing a
+   guard that doesn't exist.
+   ======================================================================== *)
+
+(* ── 2DROP ( d -- ) ─────────────────────────────────────────────────────── *)
+(* src/word_source/double_words.c:250-258. Guard: dsp \<ge> 1 (at least two
+   cells present). *)
+
+definition forth_2drop :: "vm_state \<Rightarrow> vm_state" where
+  "forth_2drop vm =
+    (case data_stack vm of
+       _ # _ # rest \<Rightarrow> vm\<lparr>data_stack := rest\<rparr>
+     | _            \<Rightarrow> set_error vm)"
+
+lemma two_drop_normal:
+  assumes "data_stack vm = dhigh # dlow # rest"
+  shows "data_stack (forth_2drop vm) = rest"
+  by (simp add: forth_2drop_def assms)
+
+lemma two_drop_underflow_nil:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_2drop vm)"
+  by (simp add: forth_2drop_def set_error_def assms)
+
+lemma two_drop_underflow_one:
+  assumes "data_stack vm = [x]"
+  shows "vm_error (forth_2drop vm)"
+  by (simp add: forth_2drop_def set_error_def assms)
+
+(* ── 2DUP ( d -- d d ) ──────────────────────────────────────────────────── *)
+(* src/word_source/double_words.c:260-272. Guard: dsp \<ge> 1. *)
+
+definition forth_2dup :: "vm_state \<Rightarrow> vm_state" where
+  "forth_2dup vm =
+    (case data_stack vm of
+       dhigh # dlow # rest \<Rightarrow>
+         vm\<lparr>data_stack := dhigh # dlow # dhigh # dlow # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma two_dup_normal:
+  assumes "data_stack vm = dhigh # dlow # rest"
+  shows "data_stack (forth_2dup vm) = dhigh # dlow # dhigh # dlow # rest"
+  by (simp add: forth_2dup_def assms)
+
+lemma two_dup_depth:
+  assumes "data_stack vm = dhigh # dlow # rest"
+  shows "length (data_stack (forth_2dup vm)) = length (data_stack vm) + 2"
+  by (simp add: forth_2dup_def assms)
+
+lemma two_dup_underflow_nil:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_2dup vm)"
+  by (simp add: forth_2dup_def set_error_def assms)
+
+lemma two_dup_underflow_one:
+  assumes "data_stack vm = [x]"
+  shows "vm_error (forth_2dup vm)"
+  by (simp add: forth_2dup_def set_error_def assms)
+
+(* ── 2SWAP ( d1 d2 -- d2 d1 ) ───────────────────────────────────────────── *)
+(* src/word_source/double_words.c:274-290. Guard: dsp \<ge> 3 (four cells). *)
+
+definition forth_2swap :: "vm_state \<Rightarrow> vm_state" where
+  "forth_2swap vm =
+    (case data_stack vm of
+       d2high # d2low # d1high # d1low # rest \<Rightarrow>
+         vm\<lparr>data_stack := d1high # d1low # d2high # d2low # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma two_swap_normal:
+  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
+  shows "data_stack (forth_2swap vm) = d1high # d1low # d2high # d2low # rest"
+  by (simp add: forth_2swap_def assms)
+
+lemma two_swap_depth_preserved:
+  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
+  shows "length (data_stack (forth_2swap vm)) = length (data_stack vm)"
+  by (simp add: forth_2swap_def assms)
+
+(* 2SWAP is its own inverse. *)
+lemma two_swap_involutive:
+  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
+  assumes "data_stack vm' = data_stack (forth_2swap vm)"
+  shows "data_stack (forth_2swap vm') = data_stack vm"
+  using assms by (simp add: forth_2swap_def)
+
+lemma two_swap_underflow_nil:
+  assumes "data_stack vm = []"
+  shows "vm_error (forth_2swap vm)"
+  by (simp add: forth_2swap_def set_error_def assms)
+
+lemma two_swap_underflow_one:
+  assumes "data_stack vm = [x]"
+  shows "vm_error (forth_2swap vm)"
+  by (simp add: forth_2swap_def set_error_def assms)
+
+lemma two_swap_underflow_two:
+  assumes "data_stack vm = [x, y]"
+  shows "vm_error (forth_2swap vm)"
+  by (simp add: forth_2swap_def set_error_def assms)
+
+lemma two_swap_underflow_three:
+  assumes "data_stack vm = [x, y, z]"
+  shows "vm_error (forth_2swap vm)"
+  by (simp add: forth_2swap_def set_error_def assms)
+
+(* ── 2OVER ( d1 d2 -- d1 d2 d1 ) ────────────────────────────────────────── *)
+(* src/word_source/double_words.c:292-305. Guard: dsp \<ge> 3. *)
+
+definition forth_2over :: "vm_state \<Rightarrow> vm_state" where
+  "forth_2over vm =
+    (case data_stack vm of
+       d2high # d2low # d1high # d1low # rest \<Rightarrow>
+         vm\<lparr>data_stack := d1high # d1low # d2high # d2low # d1high # d1low # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma two_over_normal:
+  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
+  shows "data_stack (forth_2over vm)
+       = d1high # d1low # d2high # d2low # d1high # d1low # rest"
+  by (simp add: forth_2over_def assms)
+
+lemma two_over_depth:
+  assumes "data_stack vm = d2high # d2low # d1high # d1low # rest"
+  shows "length (data_stack (forth_2over vm)) = length (data_stack vm) + 2"
+  by (simp add: forth_2over_def assms)
+
+(* ── 2ROT ( d1 d2 d3 -- d2 d3 d1 ) ──────────────────────────────────────── *)
+(* src/word_source/double_words.c:307-327. Guard: dsp \<ge> 5 (six cells).
+   Hand-verified against the doc comment's own semantics: d1 (deepest)
+   moves to the top, d2 and d3 shift down keeping their relative order. *)
+
+definition forth_2rot :: "vm_state \<Rightarrow> vm_state" where
+  "forth_2rot vm =
+    (case data_stack vm of
+       d3high # d3low # d2high # d2low # d1high # d1low # rest \<Rightarrow>
+         vm\<lparr>data_stack :=
+              d1high # d1low # d3high # d3low # d2high # d2low # rest\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma two_rot_normal:
+  assumes "data_stack vm
+         = d3high # d3low # d2high # d2low # d1high # d1low # rest"
+  shows "data_stack (forth_2rot vm)
+       = d1high # d1low # d3high # d3low # d2high # d2low # rest"
+  by (simp add: forth_2rot_def assms)
+
+lemma two_rot_depth_preserved:
+  assumes "data_stack vm
+         = d3high # d3low # d2high # d2low # d1high # d1low # rest"
+  shows "length (data_stack (forth_2rot vm)) = length (data_stack vm)"
+  by (simp add: forth_2rot_def assms)
+
+end