diff --git a/.claude/dev-cycle-profile.yml b/.claude/dev-cycle-profile.yml
index 60472d1..84b7785 100644
--- a/.claude/dev-cycle-profile.yml
+++ b/.claude/dev-cycle-profile.yml
@@ -7,6 +7,7 @@ paths:
   design_ledger: design/INDEX.md
   design_contracts: design/contracts
   design_models: design/models
+  glossary: design/glossary.md
   code_roots: [crates, runtime]
   bench_dir: bench
   public_interface: [README.md, design, docs, examples]
diff --git a/design/glossary.md b/design/glossary.md
new file mode 100644
index 0000000..285d7ef
--- /dev/null
+++ b/design/glossary.md
@@ -0,0 +1,161 @@
+# Glossary
+
+Canonical nomenclature for AILang. Use the **canonical term**; never
+use a term under **Avoid**. If you need a concept that is not listed
+here, reuse the closest existing term — do not silently coin a new
+one. New entries are added only to record nomenclature already in
+consistent use; see `~/dev/skills/docs/glossary-convention.md`.
+
+This file is the source of truth for the project's nomenclature: where
+any other document (including the design ledger) names a concept
+differently, the canonical entry and its **Avoid** list win.
+
+---
+
+## Authoring forms and identity
+
+### Form-A
+**Avoid:** Form A, authoring surface, authoring projection, surface syntax, .ailx
+The textual authoring projection an LLM author writes, stored in
+`.ail` files; it round-trips byte-isomorphically to its [[JSON-AST]].
+The retired `.ailx` extension named the same form.
+
+### Form-B
+**Avoid:** Form B, prose projection, prose surface, display projection, human prose
+The lossy, human-readable prose projection of a module, for display
+only — there is no Form-B parser, so it is never an authoring surface.
+
+### JSON-AST
+**Avoid:** canonical JSON, canonical JSON-AST
+The canonical, hashable, content-addressed structured form of a
+module, serialised on disk as `.ail.json`. Derived in-process from
+[[Form-A]] via `ailang_surface::parse`; the two forms are
+byte-isomorphic.
+
+### round-trip
+**Avoid:** roundtrip
+The invariant that parsing [[Form-A]] and printing it back is the
+identity (`parse ∘ print = id`), which keeps [[Form-A]] and the
+[[JSON-AST]] byte-isomorphic.
+
+### content-addressed
+**Avoid:** —
+Identified by the hash of the [[JSON-AST]], so a symbol can be verified
+without spending context window reading its body.
+
+## Memory model
+
+### RC
+**Avoid:** —
+Reference counting — the canonical and only production allocator (CLI
+default `--alloc=rc`). Pairs with [[uniqueness]] analysis to elide
+counts where ownership is provably unique.
+
+### uniqueness
+**Avoid:** linearity, linear types
+The static, post-typecheck dataflow analysis proving a value is
+uniquely owned, so its [[RC]] operations can be elided and in-place
+reuse is safe.
+
+### mode
+**Avoid:** ownership mode, uniqueness mode
+The `own`/`borrow` annotation on a function parameter position
+declaring how the function consumes that argument. Modes belong to
+parameter positions, not to types in general.
+
+### clone
+**Avoid:** RC clone, RC inc
+The explicit source term (`(clone x)`) that duplicates ownership of a
+value by incrementing its [[RC]].
+
+### drop
+**Avoid:** dec, RC dec
+The [[RC]] decrement emitted when a value leaves scope, plus the
+shallow-dec emitted before a tail call.
+
+### escape analysis
+**Avoid:** —
+The per-function pre-pass that decides whether an allocation can live
+on the stack instead of the heap.
+
+### frozen value layout
+**Avoid:** frozen layout, box layout
+The pinned in-memory layout of a frozen (immutable, shareable) value,
+held stable across the [[embedding ABI]].
+
+### mut-local
+**Avoid:** mutable variable, mutable local binding, mut variable
+A mutable local binding (`mut`); mutation is confined to locals, with
+no mutable variables or assignment across binders.
+
+## Types, classes, dispatch
+
+### typeclass
+**Avoid:** type class, type-class
+The narrow, Haskell-lite class system (`ClassDef` / `InstanceDef`
+declarations) — the sole ad-hoc-polymorphism mechanism.
+
+### monomorphisation
+**Avoid:** —
+The sole specialiser: every class method is resolved to a concrete
+instance body at compile time, so there is no runtime
+[[method dispatch]].
+
+### method dispatch
+**Avoid:** virtual dispatch, dictionary passing, vtable
+Type-directed resolution of a class method to its instance body; in
+AILang it is resolved statically by [[monomorphisation]], never by
+runtime dictionaries or vtables.
+
+### superclass
+**Avoid:** super-class, parent class
+A class constraint that another class requires of its instances.
+
+## Effects
+
+### effect set
+**Avoid:** effect row, effect annotation
+The explicit set of algebraic effects a function may perform, declared
+in its type. AILang has no effect-row variables, so the set is closed.
+
+### effect-op
+**Avoid:** effect op, effect operation
+A single named operation of an effect (its perform site), whose
+signature may carry a `borrow`/`own` default.
+
+## Kernel tier and codegen
+
+### kernel-tier
+**Avoid:** kernel tier
+The privileged tier of modules (e.g. [[prelude]], `raw_buf`) that may
+carry [[intrinsic]] bodies and are auto-imported with bare-name
+visibility.
+
+### prelude
+**Avoid:** —
+The [[kernel-tier]] standard module auto-imported into every module.
+
+### intrinsic
+**Avoid:** compiler-supplied body
+A function whose body is marked `(intrinsic)` in a [[kernel-tier]]
+source and is emitted by a codegen [[intercept]] rather than written
+in AILang.
+
+### intercept
+**Avoid:** —
+An entry in the codegen `INTERCEPTS` registry that supplies LLVM IR
+for an [[intrinsic]]-marked function; the registry and the
+`(intrinsic)` markers stand in a checked bijection.
+
+### MIR
+**Avoid:** —
+The post-[[monomorphisation]] typed intermediate representation
+(`MirModule`) produced by `lower_to_mir`, sitting between
+type-checking and codegen.
+
+## Embedding
+
+### embedding ABI
+**Avoid:** embedding-ABI
+The stable C ABI for calling compiled AILang from a host language,
+shipped as a `staticlib`.