diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md
index c21c5f9..54fb716 100644
--- a/design/models/0007-kernel-extensions.md
+++ b/design/models/0007-kernel-extensions.md
@@ -406,20 +406,25 @@ existing memory-model — RC + uniqueness as the canonical
 mutation story.
 
 The `own → own` signature of `RawBuf.set` is a *threading
-discipline*, not runtime-enforced single-use. The mode annotations
-drive the borrow/consume analysis and the in-place-vs-copy codegen
-decision; they do not make a second consume of the same owned
-binder a check-time error. An author who hands the same owned
-buffer to two consuming calls
-(`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))`)
-gets two bindings aliasing one slab — the second mutation is
-visible through the first. This is the same non-enforcement that
-holds for every owned value in the language (owned `Str`, owned
-ADTs); `RawBuf`'s in-place `own → own` surface is merely the first
-place the alias produces a *mutated-in-place* surprise rather than
-a benign re-read. Single-use of an owned buffer is the author's
-responsibility. Full linear enforcement, if wanted, is tracked
-separately (Issue #22 territory).
+discipline* enforced by the uniqueness/linearity check where that
+check is active, not a runtime guard. The mode annotations drive
+the borrow/consume analysis and the in-place-vs-copy codegen
+decision. Where the linearity check runs — a fn whose parameters
+all carry explicit `own`/`borrow` modes — a second consume of the
+same owned binder *is* rejected at check time (`use-after-consume`):
+a helper `(fn f (params (own (RawBuf Int))) …)` that hands its
+buffer to two consuming calls is caught. The check has an
+activation gate, though: it does not run on a fn with no parameters
+(a paramless top-level `main`) or one with implicit-mode parameters.
+A double-consume written directly in such an unchecked context —
+`(let a (RawBuf.set buf 0 1)) (let b (RawBuf.set buf 1 2))` inside a
+paramless `main` — is not caught, and the two bindings alias one
+slab (the second mutation is visible through the first). `RawBuf`'s
+in-place `own → own` surface is the first place this alias produces
+a *mutated-in-place* surprise rather than a benign re-read. Single-
+use of an owned buffer in an unchecked context is the author's
+responsibility. Tightening the activation gate, or full linear
+enforcement, is tracked separately (Issue #22 territory).
 
 Storage at the LLVM-IR level is type-specialised: the Rust
 intercept registered for `RawBuf` dispatches on the element type