diff --git a/proof/ROOT b/proof/ROOT
index 7bbaac4..35c49e6 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -37,6 +37,7 @@ session "StarForth" = "HOL-Library" +
     StarForth_Defer_Words
     StarForth_Log_Words
     StarForth_Q48_Words
+    StarForth_Inference_Words
     StarForth_Loop1_Heat
     StarForth_Loop2_Window
     StarForth_Loop3_Decay
diff --git a/proof/StarForth_Inference_Words.thy b/proof/StarForth_Inference_Words.thy
new file mode 100644
index 0000000..b67cbd9
--- /dev/null
+++ b/proof/StarForth_Inference_Words.thy
@@ -0,0 +1,252 @@
+theory StarForth_Inference_Words
+  imports StarForth_Base
+begin
+
+(* =========================================================================
+   Mirrors: src/word_source/inference_words.c
+   Registers: Q.VARIANCE INFER-DECAY-SLOPE INFER-WINDOW-WIDTH
+              WINDOW-DIVERSITY INFER-RUN INFER-WINDOW@ INFER-DECAY@
+              INFER-VARIANCE@ INFER-FIT@ INFER-EARLY-EXIT@ L8-MODE
+              L8-UPDATE L8-APPLY L8-TABLE-FORCE BAYES-CACHE-MEAN/LOWER/UPPER
+              BAYES-BUCKET-MEAN/LOWER/UPPER
+
+   ── Scope ─────────────────────────────────────────────────────────────
+   Fully modelled: the five INFER-*@ output accessors, which read straight
+   from `vm->last_inference_outputs` -- exactly `last_inference ::
+   inference_outputs_state option` in vm_state (StarForth_Base.thy),
+   already modelled with matching field names for every value these words
+   read.
+
+   Guard/shape only: Q.VARIANCE, INFER-DECAY-SLOPE, INFER-WINDOW-WIDTH
+   (pop 2, bounds-check the array reference) -- and a genuine finding
+   about that bounds check, see below. L8-UPDATE, L8-TABLE-FORCE (pop
+   shape only; computed/target-subsystem effect not modelled).
+
+   Not modelled: WINDOW-DIVERSITY, L8-MODE, L8-APPLY, the six
+   BAYES-CACHE-*/BAYES-BUCKET-* words, and INFER-RUN. See per-word notes.
+
+   ── Finding: array_ptr sets vm->error but the caller pushes anyway ──────
+   `array_ptr` (line 74) sets `vm->error = 1` AND returns NULL on any
+   bounds failure. All three of its callers (Q.VARIANCE/INFER-DECAY-SLOPE/
+   INFER-WINDOW-WIDTH) check only the returned pointer, not `vm->error`,
+   before pushing a 0 placeholder -- so on an invalid array reference the
+   word both sets the error flag AND pushes a value, unlike the "error OR
+   push, never both" shape virtually every other guarded word in this
+   sweep follows. Modelled faithfully: the error and the push both happen.
+
+   ── Finding: L8-MODE reads a DIFFERENT L8 representation than vm_state
+      models ──────────────────────────────────────────────────────────
+   `vm->ssm_l8_state` (cast from `void*` to `ssm_l8_state_t*`) is NOT the
+   same field as `ssm_l8 :: ssm_l8_state` already in vm_state
+   (StarForth_Base.thy, used by StarForth_Concurrent.thy/StarForth_
+   Transition.thy) -- that abstract record models a 4-mode `ssm_mode`
+   datatype (`C0`/`C1`/`C2`/`C3`), whereas this file's `current_mode` is
+   documented as a legacy 16-mode int (`L8-MODE` pushes `0-15`), and
+   `L8-TABLE-FORCE`'s own comment additionally describes a THIRD,
+   currently-live representation: a 128-config adaptive table the
+   heartbeat's bandit selection actually drives, which the legacy 16-mode
+   `L8-UPDATE`/`L8-APPLY` path is explicitly said to be overwritten by.
+   So there are (at least) three L8 representations in play across the
+   real system -- the abstract model's 4-mode `ssm_l8`, this file's
+   legacy 16-mode `ssm_l8_state_t`, and the 128-config adaptive table --
+   and none of this file's L8 words touch the one `ssm_l8` field this
+   proof suite actually models. Not modelled as a result; flagged as an
+   open question about which representation `ssm_l8` was originally meant
+   to track, worth raising directly rather than guessing.
+   ======================================================================== *)
+
+(* ── INFER-WINDOW@ / INFER-DECAY@ / INFER-VARIANCE@ / INFER-FIT@ /
+   INFER-EARLY-EXIT@ ( -- n|q|flag ) : read last_inference, 0 if None ──── *)
+
+definition forth_infer_window_fetch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_infer_window_fetch vm =
+    vm\<lparr>data_stack :=
+        word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_adaptive_window_width io)
+        # data_stack vm\<rparr>"
+
+definition forth_infer_decay_fetch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_infer_decay_fetch vm =
+    vm\<lparr>data_stack :=
+        word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_adaptive_decay_slope io)
+        # data_stack vm\<rparr>"
+
+definition forth_infer_variance_fetch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_infer_variance_fetch vm =
+    vm\<lparr>data_stack :=
+        word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_window_variance_q48 io)
+        # data_stack vm\<rparr>"
+
+definition forth_infer_fit_fetch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_infer_fit_fetch vm =
+    vm\<lparr>data_stack :=
+        word_of_nat (case last_inference vm of None \<Rightarrow> 0 | Some io \<Rightarrow> io_fit_quality_q48 io)
+        # data_stack vm\<rparr>"
+
+definition forth_infer_early_exit_fetch :: "vm_state \<Rightarrow> vm_state" where
+  "forth_infer_early_exit_fetch vm =
+    vm\<lparr>data_stack :=
+        to_forth_bool (case last_inference vm of None \<Rightarrow> False | Some io \<Rightarrow> io_early_exited io)
+        # data_stack vm\<rparr>"
+
+lemma infer_window_fetch_none:
+  assumes "last_inference vm = None"
+  shows "data_stack (forth_infer_window_fetch vm) = 0 # data_stack vm"
+  using assms by (simp add: forth_infer_window_fetch_def)
+
+lemma infer_window_fetch_some:
+  assumes "last_inference vm = Some io"
+  shows "data_stack (forth_infer_window_fetch vm) = word_of_nat (io_adaptive_window_width io) # data_stack vm"
+  using assms by (simp add: forth_infer_window_fetch_def)
+
+lemma infer_decay_fetch_none:
+  assumes "last_inference vm = None"
+  shows "data_stack (forth_infer_decay_fetch vm) = 0 # data_stack vm"
+  using assms by (simp add: forth_infer_decay_fetch_def)
+
+lemma infer_decay_fetch_some:
+  assumes "last_inference vm = Some io"
+  shows "data_stack (forth_infer_decay_fetch vm) = word_of_nat (io_adaptive_decay_slope io) # data_stack vm"
+  using assms by (simp add: forth_infer_decay_fetch_def)
+
+lemma infer_variance_fetch_none:
+  assumes "last_inference vm = None"
+  shows "data_stack (forth_infer_variance_fetch vm) = 0 # data_stack vm"
+  using assms by (simp add: forth_infer_variance_fetch_def)
+
+lemma infer_variance_fetch_some:
+  assumes "last_inference vm = Some io"
+  shows "data_stack (forth_infer_variance_fetch vm) = word_of_nat (io_window_variance_q48 io) # data_stack vm"
+  using assms by (simp add: forth_infer_variance_fetch_def)
+
+lemma infer_fit_fetch_none:
+  assumes "last_inference vm = None"
+  shows "data_stack (forth_infer_fit_fetch vm) = 0 # data_stack vm"
+  using assms by (simp add: forth_infer_fit_fetch_def)
+
+lemma infer_fit_fetch_some:
+  assumes "last_inference vm = Some io"
+  shows "data_stack (forth_infer_fit_fetch vm) = word_of_nat (io_fit_quality_q48 io) # data_stack vm"
+  using assms by (simp add: forth_infer_fit_fetch_def)
+
+lemma infer_early_exit_fetch_none:
+  assumes "last_inference vm = None"
+  shows "data_stack (forth_infer_early_exit_fetch vm) = 0 # data_stack vm"
+  using assms by (simp add: forth_infer_early_exit_fetch_def)
+
+lemma infer_early_exit_fetch_some_true:
+  assumes "last_inference vm = Some io" "io_early_exited io"
+  shows "data_stack (forth_infer_early_exit_fetch vm) = -1 # data_stack vm"
+  using assms by (simp add: forth_infer_early_exit_fetch_def)
+
+lemma infer_early_exit_fetch_some_false:
+  assumes "last_inference vm = Some io" "\<not> io_early_exited io"
+  shows "data_stack (forth_infer_early_exit_fetch vm) = 0 # data_stack vm"
+  using assms by (simp add: forth_infer_early_exit_fetch_def)
+
+lemma infer_fetch_words_no_overflow_guard: True
+  \<comment> \<open>All five push unconditionally, no ds_full check -- another instance
+     of the recurring missing-overflow-guard pattern.\<close>
+  by simp
+
+(* ── Q.VARIANCE / INFER-DECAY-SLOPE / INFER-WINDOW-WIDTH
+   ( addr u -- q|n ) : guard/pop2 shape + the error-and-push quirk ──────── *)
+(* C: no upfront dsp guard -- relies on VM_POP itself (see StarForth_Q48_
+   Words.thy's build-flag stack-safety finding, same VM_POP/VM_PUSH macro
+   usage here). Pops u then addr; array_ptr validates and, on failure,
+   sets vm->error AND returns NULL, after which the caller pushes 0
+   regardless of the error flag (see file header finding). Modelled here
+   assuming the underlying pop always succeeds (i.e. at least 2 elements
+   present, matching this suite's usual convention of not re-deriving the
+   VM_POP/vm_pop underflow case per word); the array-bounds branch is
+   modelled precisely since it's this word's own logic, not a macro. *)
+
+definition forth_q_variance_guard :: "vm_state \<Rightarrow> vm_state" where
+  "forth_q_variance_guard vm =
+    (case data_stack vm of
+       u # addr # xs \<Rightarrow>
+         (if u \<le>s 0 \<or> unat addr \<ge> VM_MEMORY_SIZE \<or> unat addr + unat u * 8 > VM_MEMORY_SIZE
+          then set_error (vm\<lparr>data_stack := 0 # xs\<rparr>)
+          else vm\<lparr>data_stack := xs\<rparr>)
+     | _ \<Rightarrow> set_error vm)"
+
+lemma q_variance_invalid_array_errors_and_pushes_zero:
+  assumes "data_stack vm = u # addr # xs"
+  assumes "u \<le>s 0 \<or> unat addr \<ge> VM_MEMORY_SIZE \<or> unat addr + unat u * 8 > VM_MEMORY_SIZE"
+  shows "vm_error (forth_q_variance_guard vm)"
+    and "data_stack (forth_q_variance_guard vm) = 0 # xs"
+  using assms by (simp_all add: forth_q_variance_guard_def set_error_def)
+
+lemma q_variance_valid_array_pops_only:
+  assumes "data_stack vm = u # addr # xs"
+  assumes "\<not> (u \<le>s 0 \<or> unat addr \<ge> VM_MEMORY_SIZE \<or> unat addr + unat u * 8 > VM_MEMORY_SIZE)"
+  shows "data_stack (forth_q_variance_guard vm) = xs"
+  using assms by (simp add: forth_q_variance_guard_def)
+
+lemma q_variance_result_value_not_modelled: True
+  \<comment> \<open>compute_variance_q48 -- a real variance computation over raw VM
+     memory, not modelled. INFER-DECAY-SLOPE/INFER-WINDOW-WIDTH share this
+     exact guard shape (infer_decay_slope_q48/find_variance_inflection
+     also not modelled) -- one shared guard definition covers all three,
+     matching the file's own `array_ptr` helper being shared.\<close>
+  by simp
+
+(* ── L8-UPDATE ( entropy cv temporal stability -- ) : pop4 shape only ───── *)
+(* C: no dsp guard at all; if `l8` is NULL, pops all four anyway (four
+   bare VM_POP calls) and returns; if non-NULL, pops all four via
+   q48_pop_inf (same VM_POP) and calls ssm_l8_update -- either way,
+   exactly four elements are popped whenever the stack has \<ge> 4. *)
+
+definition forth_l8_update_guard :: "vm_state \<Rightarrow> vm_state" where
+  "forth_l8_update_guard vm =
+    (case data_stack vm of
+       a # b # c # d # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma l8_update_pops_four:
+  assumes "data_stack vm = a # b # c # d # xs"
+  shows "data_stack (forth_l8_update_guard vm) = xs"
+  by (simp add: forth_l8_update_guard_def assms)
+
+lemma l8_update_target_not_modelled: True
+  \<comment> \<open>ssm_l8_update mutates *vm->ssm_l8_state -- see file header's L8
+     representation-mismatch finding; not the vm_state field `ssm_l8`.\<close>
+  by simp
+
+(* ── L8-TABLE-FORCE ( config_idx -- ) : pop1 shape only ─────────────────── *)
+(* C: pops idx unconditionally BEFORE checking l8/cfg for NULL. *)
+
+definition forth_l8_table_force_guard :: "vm_state \<Rightarrow> vm_state" where
+  "forth_l8_table_force_guard vm =
+    (case data_stack vm of
+       idx # xs \<Rightarrow> vm\<lparr>data_stack := xs\<rparr>
+     | _ \<Rightarrow> set_error vm)"
+
+lemma l8_table_force_pops_one:
+  assumes "data_stack vm = idx # xs"
+  shows "data_stack (forth_l8_table_force_guard vm) = xs"
+  by (simp add: forth_l8_table_force_guard_def assms)
+
+lemma l8_table_force_target_not_modelled: True
+  \<comment> \<open>ssm_l8_force_config mutates the 128-config adaptive table -- a THIRD
+     L8 representation, see file header finding.\<close>
+  by simp
+
+(* ── Everything else -- NOT MODELLED ──────────────────────────────────── *)
+
+lemma window_diversity_not_modelled: True \<comment> \<open>WINDOW-DIVERSITY: rolling_window_measure_diversity computes a fresh value from rw_history (a modelled field, but the diversity ALGORITHM over it is not) -- distinct from the already-stored rw_last_diversity. No overflow guard either.\<close>
+  by simp
+lemma infer_run_not_modelled: True \<comment> \<open>INFER-RUN: allocates last_inference_outputs on first call, walks the dictionary read-only for heat stats, then runs inference_engine_run -- a whole-subsystem algorithm. This is the ONLY word that writes `last_inference`, so no fetch-after-INFER-RUN lemma can be stated.\<close>
+  by simp
+lemma l8_mode_not_modelled: True \<comment> \<open>L8-MODE: reads vm->ssm_l8_state's legacy 16-mode int -- see file header's representation-mismatch finding. No overflow guard.\<close>
+  by simp
+lemma l8_apply_not_modelled: True \<comment> \<open>L8-APPLY: no-op if !l8||!cfg, else ssm_apply_mode -- targets the same unmodelled legacy L8 state as L8-UPDATE.\<close>
+  by simp
+lemma bayes_cache_mean_not_modelled: True \<comment> \<open>BAYES-CACHE-MEAN: hotwords_posterior_cache_hits over the unmodelled hot-words cache subsystem (StarForth_Physics_Benchmark_Words.thy). No overflow guard.\<close>
+  by simp
+lemma bayes_cache_lower_not_modelled: True by simp
+lemma bayes_cache_upper_not_modelled: True by simp
+lemma bayes_bucket_mean_not_modelled: True by simp
+lemma bayes_bucket_lower_not_modelled: True by simp
+lemma bayes_bucket_upper_not_modelled: True by simp
+
+end