diff --git a/proof/ROOT b/proof/ROOT
index 43a57c6..76f8cc3 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -11,6 +11,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Return_Stack_Words
     StarForth_Memory_Words
     StarForth_Dictionary_Words
+    StarForth_Dictionary_Manipulation_Words
     StarForth_Mutex
     StarForth_Transition
     StarForth_Loop1_Heat
diff --git a/proof/StarForth_Dictionary_Manipulation_Words.thy b/proof/StarForth_Dictionary_Manipulation_Words.thy
new file mode 100644
index 0000000..e787fe0
--- /dev/null
+++ b/proof/StarForth_Dictionary_Manipulation_Words.thy
@@ -0,0 +1,234 @@
+theory StarForth_Dictionary_Manipulation_Words
+  imports StarForth_Base
+begin
+
+(* =========================================================================
+   POST-07: Dictionary Manipulation Words
+   Mirrors: src/word_source/dictionary_manipulation_words.c
+
+   This file splits sharply into two classes:
+
+   1. Mode/flag words ([, ], SMUDGE, HIDDEN, INTERPRET) -- provable against
+      the existing vm_mode / dictionary / latest_id fields.
+
+   2. Raw-pointer dictionary-navigation words (>BODY, >NAME, NAME>, >LINK,
+      LINK>, CFA, LFA, NFA, PFA, TRAVERSE, FIND, ') -- NOT modelled. Every
+      one of these casts a cell_t directly to/from a C `DictEntry*` and
+      walks struct fields (name_len, link, the byte after the header) that
+      have no counterpart in the abstract `dict_entry` record (StarForth_
+      Base.thy:293), which is indexed abstractly by word_id, not by a raw
+      memory address at all. This is the same class of gap already flagged
+      for control_words.c's vm_ip/return-stack-as-raw-pointers (see that
+      file's resume-point note) -- formalizing it would mean re-deriving
+      the C struct layout (header size, name_len byte, link pointer
+      arithmetic, body alignment) as a second, address-based dictionary
+      model living alongside the existing word_id-based one. Out of scope
+      for this pass; flagged per-word below as documented gaps, not lemmas.
+
+      Per CLAUDE.md: `dictionary_m_word_find` (registered as "FIND") is the
+      real, tested, non-standard FIND word ("parses from input stream").
+      This file only *reads* it for modelling purposes here -- consistent
+      with "never modify FIND", since nothing in proof/ touches the C
+      source.
+
+   ── Genuine findings, not fixed ──────────────────────────────────────────
+   1. `[`, `]`, `STATE`, and `INTERPRET` all read/write a `static cell_t
+      state_variable` at FILE SCOPE (line 49) -- NOT `vm->state_var`
+      (include/vm.h:431, the real per-VM STATE field actively used by
+      vm.c/vm_core.c/vm_bootstrap.c/capsule_loader.c on both hosted and
+      kernel builds). This static is a single process-wide variable, not
+      even per-VM: in the Tripod multi-VM fleet, EVERY VM's `[`/`]`/
+      `INTERPRET` mutates the SAME shared cell, and `STATE` pushes ITS
+      address (a bare host pointer, not a VM address) -- identical across
+      every VM instance. `vm->state_var` itself is correctly toggled
+      elsewhere in the real interpreter loop, so the dictionary-space
+      compile/interpret bookkeeping isn't broken, but these four FORTH
+      words are effectively wired to a dead, cross-VM-shared shadow
+      variable instead of the VM's own state. Modelled below using only
+      `vm_mode` (which `[`/`]` DO correctly set) -- the dead static write
+      has no vm_state counterpart and is simply omitted, not "fixed".
+   2. `dictionary_m_word_hidden`'s `#else` fallback branch (taken only if
+      `WORD_HIDDEN` is undefined -- it is always defined per include/vm.h:
+      181, so this branch is dead in every build configuration seen) calls
+      `dictionary_word_smudge`, which does not exist: the real function in
+      this file is `static void dictionary_m_word_smudge` (note the `_m_`
+      and `static` -- not externally callable even if the name were right).
+      Latent compile-time bug, unreachable under current WORD_HIDDEN
+      always-defined builds. Not modelled (dead branch), not fixed.
+   ======================================================================== *)
+
+(* ── [ ( -- ) : enter interpretation mode ─────────────────────────────── *)
+(* C: vm->mode = MODE_INTERPRET; state_variable = 0 (dead static, see above). *)
+
+definition forth_left_bracket :: "vm_state \<Rightarrow> vm_state" where
+  "forth_left_bracket vm = vm\<lparr>vm_mode := ModeInterpret\<rparr>"
+
+lemma left_bracket_sets_interpret:
+  "vm_mode (forth_left_bracket vm) = ModeInterpret"
+  by (simp add: forth_left_bracket_def)
+
+lemma left_bracket_data_stack_unchanged:
+  "data_stack (forth_left_bracket vm) = data_stack vm"
+  by (simp add: forth_left_bracket_def)
+
+lemma left_bracket_never_errors:
+  "vm_error (forth_left_bracket vm) = vm_error vm"
+  by (simp add: forth_left_bracket_def)
+
+(* ── ] ( -- ) : enter compilation mode ─────────────────────────────────── *)
+(* C: vm->mode = MODE_COMPILE; state_variable = -1 (dead static, see above). *)
+
+definition forth_right_bracket :: "vm_state \<Rightarrow> vm_state" where
+  "forth_right_bracket vm = vm\<lparr>vm_mode := ModeCompile\<rparr>"
+
+lemma right_bracket_sets_compile:
+  "vm_mode (forth_right_bracket vm) = ModeCompile"
+  by (simp add: forth_right_bracket_def)
+
+lemma right_bracket_data_stack_unchanged:
+  "data_stack (forth_right_bracket vm) = data_stack vm"
+  by (simp add: forth_right_bracket_def)
+
+lemma right_bracket_never_errors:
+  "vm_error (forth_right_bracket vm) = vm_error vm"
+  by (simp add: forth_right_bracket_def)
+
+(* ── [ then ] / ] then [ : mode is exactly what was set last ─────────────── *)
+
+lemma bracket_right_then_left:
+  "vm_mode (forth_left_bracket (forth_right_bracket vm)) = ModeInterpret"
+  by (simp add: forth_left_bracket_def)
+
+lemma bracket_left_then_right:
+  "vm_mode (forth_right_bracket (forth_left_bracket vm)) = ModeCompile"
+  by (simp add: forth_right_bracket_def)
+
+(* ── STATE ( -- addr ) -- NOT MODELLED ────────────────────────────────── *)
+
+lemma state_not_modelled: True
+  \<comment> \<open>STATE pushes `(cell_t)(uintptr_t)&state_variable` -- the address of a
+     bare host C static, not a VM address and not `vm->state_addr`/
+     `vm->state_var` (which DO exist in the abstract model and ARE the real
+     per-VM state, see the file-level finding above). There is nothing in
+     vm_state for this word to legitimately push; modelling it would mean
+     inventing a fake address for a variable outside the VM's own address
+     space entirely. Left undocumented as a lemma, gap only.\<close>
+  by simp
+
+(* ── SMUDGE ( -- ) : compile-only guard, empty body ──────────────────────── *)
+(* C: error unless vm->mode == MODE_COMPILE; the "existing body that toggles
+   the smudge bit" is literally absent (comment placeholder only, no code).
+   So the word's entire effect, when it doesn't error, is: nothing. *)
+
+definition forth_smudge :: "vm_state \<Rightarrow> vm_state" where
+  "forth_smudge vm = (if vm_mode vm \<noteq> ModeCompile then set_error vm else vm)"
+
+lemma smudge_requires_compile_mode:
+  assumes "vm_mode vm \<noteq> ModeCompile"
+  shows "vm_error (forth_smudge vm)"
+  by (simp add: forth_smudge_def set_error_def assms)
+
+lemma smudge_in_compile_mode_is_noop:
+  assumes "vm_mode vm = ModeCompile"
+  shows "forth_smudge vm = vm"
+  by (simp add: forth_smudge_def assms)
+
+(* ── HIDDEN ( -- ) : set WORD_HIDDEN (0x40) on the latest word ──────────── *)
+(* C: error unless vm->mode == MODE_COMPILE; error if vm->latest is NULL;
+   else e->flags |= WORD_HIDDEN (the #else dead-branch, see file note #2,
+   is unreachable and not modelled). *)
+
+definition WORD_HIDDEN :: nat where "WORD_HIDDEN = 0x40"
+
+definition forth_hidden :: "vm_state \<Rightarrow> vm_state" where
+  "forth_hidden vm =
+    (if vm_mode vm \<noteq> ModeCompile
+     then set_error vm
+     else case latest_id vm of
+            None \<Rightarrow> set_error vm
+          | Some wid \<Rightarrow>
+              (case dictionary vm wid of
+                 None \<Rightarrow> set_error vm
+               | Some e \<Rightarrow>
+                   vm\<lparr>dictionary := (dictionary vm)
+                        (wid := Some (e\<lparr>de_flags := de_flags e OR WORD_HIDDEN\<rparr>))\<rparr>))"
+
+lemma hidden_requires_compile_mode:
+  assumes "vm_mode vm \<noteq> ModeCompile"
+  shows "vm_error (forth_hidden vm)"
+  by (simp add: forth_hidden_def set_error_def assms)
+
+lemma hidden_requires_latest:
+  assumes "vm_mode vm = ModeCompile"
+  assumes "latest_id vm = None"
+  shows "vm_error (forth_hidden vm)"
+  by (simp add: forth_hidden_def set_error_def assms)
+
+lemma hidden_requires_latest_present_in_dict:
+  assumes "vm_mode vm = ModeCompile"
+  assumes "latest_id vm = Some wid"
+  assumes "dictionary vm wid = None"
+  shows "vm_error (forth_hidden vm)"
+  by (simp add: forth_hidden_def set_error_def assms)
+
+lemma hidden_sets_flag:
+  assumes "vm_mode vm = ModeCompile"
+  assumes "latest_id vm = Some wid"
+  assumes "dictionary vm wid = Some e"
+  shows "\<exists>e'. dictionary (forth_hidden vm) wid = Some e' \<and>
+              de_flags e' = de_flags e OR WORD_HIDDEN"
+  using assms by (simp add: forth_hidden_def)
+
+lemma hidden_data_stack_unchanged:
+  "data_stack (forth_hidden vm) = data_stack vm"
+  by (auto simp: forth_hidden_def set_error_def split: option.split)
+
+(* ── INTERPRET ( -- ) ──────────────────────────────────────────────────── *)
+(* C: vm->mode = MODE_INTERPRET; state_variable = 0 (dead static, see file
+   note). Comment in the C source admits the word does not itself invoke
+   the interpreter loop ("This word exists mainly for completeness and mode
+   setting") -- so its real effect is identical to `[`. *)
+
+definition forth_interpret :: "vm_state \<Rightarrow> vm_state" where
+  "forth_interpret = forth_left_bracket"
+
+lemma interpret_is_left_bracket:
+  "forth_interpret vm = forth_left_bracket vm"
+  by (simp add: forth_interpret_def)
+
+lemma interpret_sets_interpret_mode:
+  "vm_mode (forth_interpret vm) = ModeInterpret"
+  by (simp add: forth_interpret_def forth_left_bracket_def)
+
+(* ── Raw-pointer dictionary navigation -- NOT MODELLED ────────────────────
+   See the file-level note at the top: >BODY, >NAME, NAME>, >LINK, LINK>,
+   CFA, LFA, NFA, PFA, TRAVERSE, FIND, ' all cast cell_t <-> DictEntry* and
+   walk struct-layout details (name_len, link, header-relative body offset)
+   absent from the word_id-indexed abstract dict_entry model. Each gets a
+   named sentinel lemma so the gap is greppable per word, matching the
+   SP@/SP! convention in StarForth_Dictionary_Words.thy. *)
+
+lemma to_body_not_modelled: True    \<comment> \<open>>BODY: xt -> DictEntry* -> data field addr (struct-relative pointer arithmetic).\<close>
+  by simp
+lemma to_name_not_modelled: True    \<comment> \<open>>NAME: xt -> DictEntry* -> &entry->name (struct field address).\<close>
+  by simp
+lemma name_to_not_modelled: True    \<comment> \<open>NAME>: linear scan of vm->latest chain by raw name-field pointer identity.\<close>
+  by simp
+lemma to_link_not_modelled: True    \<comment> \<open>>LINK (= LFA): addr -> DictEntry* -> &entry->link (struct field address).\<close>
+  by simp
+lemma link_from_not_modelled: True  \<comment> \<open>LINK>: dereferences a DictEntry** raw pointer.\<close>
+  by simp
+lemma cfa_not_modelled: True        \<comment> \<open>CFA: identity cast addr -> DictEntry* -> xt; no abstract counterpart needed but the cast itself is untyped.\<close>
+  by simp
+lemma nfa_not_modelled: True        \<comment> \<open>NFA: same struct-field address as >NAME.\<close>
+  by simp
+lemma pfa_not_modelled: True        \<comment> \<open>PFA: get_body_address -- header size + name_len + alignment arithmetic.\<close>
+  by simp
+lemma traverse_not_modelled: True   \<comment> \<open>TRAVERSE: raw byte-pointer arithmetic over a length-prefixed name field.\<close>
+  by simp
+lemma find_not_modelled: True       \<comment> \<open>FIND: parses input stream (vm_parse_word) + vm_find_word lookup, neither modelled anywhere in this suite yet. Per CLAUDE.md this is the real, tested, non-standard FIND -- read-only reference here, the C is untouched.\<close>
+  by simp
+lemma tick_not_modelled: True       \<comment> \<open>' (tick): identical parse+lookup dependency as FIND, plus a not-found error path FIND itself doesn't have.\<close>
+  by simp
+
+end