diff --git a/docs/superpowers/specs/2026-09-13-libvct-design.md b/docs/superpowers/specs/2026-09-13-libvct-design.md
index 7bc6064..91cb485 100644
--- a/docs/superpowers/specs/2026-09-13-libvct-design.md
+++ b/docs/superpowers/specs/2026-09-13-libvct-design.md
@@ -33,7 +33,7 @@ The design thesis: because HIR hands VIR a fully annotated "dictionary" of facts
 - **Windows / MSVC.** Linux/POSIX-first; gcc and clang only.
 - **LLVM bitcode.** The LLVM backend emits textual `.ll` only; the caller runs `llvm-as`.
 - **LLVM debug metadata.** No `!llvm.dbg` in v1; debug mapping exists on the C path via `#line`.
-- **A user-facing VIR.** VIR is internal and intentionally hostile to hand-authoring.
+- **A hand-authored VIR.** VIR is internal and intentionally hostile to hand-authoring. A textual form exists solely for tools and round-trip tests (§9.8); it is not a supported authoring surface.
 - **Consuming LLVM IR or Vox's existing IR.** libVCT owns its IR definition.
 
 ### 1.3 Glossary
@@ -135,7 +135,7 @@ Every attribute carries an `attr_source` bit recording whether it was suggested
 | `is_addressed` | Address taken by pointer/reference. |
 | `escapes` | Value escapes its defining scope. |
 | `is_runtime_mutable` | May change at runtime. |
-| `may_change_at_runtime` | Alias of intent: value is not frozen. |
+| `may_change_at_runtime` | The observable value may differ between reads/executions (external state). Distinct from `is_runtime_mutable`, which means the storage is written at runtime. |
 | `complex` | Frontend-provided; gates the `NoOptimize` request. |
 
 ### 3.2 Requests
@@ -312,7 +312,7 @@ HIR carries a real high-level `defer` statement. The optimizer inlines the defer
 
 - **Input:** annotated HIR with **complete, epoch-valid** traits.
 - **Output:** VIR — basic blocks, phi-nodes, def-use, SSA.
-- Lowering **validates trait completeness**. A missing or contradictory trait raises an **internal-compiler-error** diagnostic (see §11).
+- Lowering **validates trait completeness**. A missing or contradictory trait raises an **internal-compiler-error** diagnostic (see §10.5).
 - Deterministic; parallelizable per function.
 
 ### 5.2 Form
@@ -365,7 +365,7 @@ Well-formed SSA:
 - phi arity equals predecessor count,
 - a single def per value.
 
-Verified in debug builds (§12).
+Verified in debug builds (§11).
 
 ---
 
@@ -771,8 +771,8 @@ The HIR cascade proceeds as follows:
 
 1. HIR comptime-evaluates `x = 4` → `is_comptime`, `is_constant`, `const_value = 4`.
 2. `y = x + 4` unfolds to `y = 8` → `is_comptime`.
-3. `foo(x, y)` is proven small → HIR issues an `Inline` **request**; `z` becomes `8 + ...` constant → comptime.
-4. `a = sqrt(z)` → `a = sqrt(8)` comptime → `a = 3.4641016151377544`.
+3. `foo(x, y)` is proven small → HIR issues an `Inline` **request**; after inlining, `z = 4 + 8 = 12` → comptime.
+4. `a = sqrt(z)` → `a = sqrt(12)` comptime → `a = 3.4641016151377544`.
 5. The whole program collapses to `println(3.4641016151377544)`.
 
 VIR then optimizes the `println` call. The emitted C is effectively a single call with the folded constant. This demonstrates trait propagation HIR → VIR and the request lifecycle (`Inline` accepted).