diff --git a/docs/docs/proposals/index.md b/docs/docs/proposals/index.md
index 20f228c..7d4ce18 100755
--- a/docs/docs/proposals/index.md
+++ b/docs/docs/proposals/index.md
@@ -121,6 +121,21 @@ to the same shape:
 - [Proposal D — keep `@unchecked`](guarantee-marker/unchecked.md): the original
   name. *rejected: says neither who nor what.*
 
+#### [A shared vocabulary](shared-vocabulary/index.md)
+
+One catalog of the names several programs agree on (encodings, guarantees,
+facts and their values, conformance features, annotations, diagnostic codes,
+CI targets), with sets as queries over it, read by core, the runtimes, the
+generators, the language server, the Observatory and the docs. Two parts,
+read in order:
+
+- [The catalog](shared-vocabulary/catalog.md): entries, kinds, sets,
+  relations, and where the catalog lives. *draft.*
+- [Granular `@unverified`](shared-vocabulary/granular-unverified.md): an
+  optional keyed form naming each guarantee with its own reason, at the
+  scope that guarantee has, checked against what core computes. Revisits part
+  of the guarantee-marker decision. *draft.*
+
 ### Connections
 
 - [Connections](connections.md): what a connection carries beyond one client
diff --git a/docs/docs/proposals/shared-vocabulary/catalog.md b/docs/docs/proposals/shared-vocabulary/catalog.md
new file mode 100644
index 0000000..dc4284b
--- /dev/null
+++ b/docs/docs/proposals/shared-vocabulary/catalog.md
@@ -0,0 +1,190 @@
+# The catalog
+
+Status: **draft** · part of [A shared vocabulary](index.md)
+
+**The idea:** every name that more than one program needs to agree on is an
+entry in one catalog. Code refers to an entry by its id, and each set of names
+is a query over the catalog rather than a hand-kept list.
+
+## An entry
+
+```cue
+facts: struct_fields: {
+    kind:        "fact"
+    applies_to:  "format"
+    title:       "struct fields"
+    description: "How a struct's fields are written: in declaration order, or by name."
+    values: {
+        by_position: "fields back to back, in declaration order"
+        by_name:     "each field keyed by its name"
+    }
+    proven_by: "vectors"
+    since:     "spec-0.6"
+    status:    "stable"
+}
+
+encodings: "jsonrpc@1": {
+    kind:    "framing"
+    aliases: ["jsonrpc", "json-rpc"]
+    facts: {calls: "by_name", directions: "both", payload: "json"}
+    vectors: true
+    tags: ["official"]
+    status: "stable"
+}
+
+guarantees: bounded_size: {
+    kind:        "guarantee"
+    title:       "bounded size"
+    description: "Every value has a maximum size, so a decoder refuses an oversized one before allocating it."
+    scopes: ["protocol", "function", "argument", "type"]
+}
+```
+
+Illustrative, in CUE since the conformance specs already use it. The model is
+what matters, not the syntax.
+
+| Field | Meaning |
+|---|---|
+| **id** | The stable name. For a wire name it is the published spelling and never changes; a rename adds an entry and deprecates the old one. |
+| **kind** | `format`, `framing`, `handshake`, `guarantee`, `fact`, `feature`, `annotation`, `setting`, `diagnostic`, `fuzz-target`, `bench`, `report`, and more as needed. |
+| **tags** | Free labels that sets are built from: `official`, `nightly`, `1.0`, `no_std`, `experimental`. |
+| **title, description** | One source for hover text, docs tables, diagnostics and generated comments. |
+| **values** | For a fact or setting, the value domain, each value with its meaning. |
+| **aliases** | Other accepted spellings, resolved to the id (`json-rpc` → `jsonrpc@1`). |
+| **status, since** | `experimental`, `stable` or `deprecated (use X)`, and the catalog or spec version it arrived in. |
+| **relations** | References to other entries: an encoding's facts, the guarantees a handshake establishes, the scopes a guarantee applies at. |
+
+## Kinds worth covering
+
+Every kind where one source would remove copies. In rough order of value:
+
+1. **Encodings, handshakes, their facts and value domains.** These are the
+   most duplicated, and the most dangerous to get wrong.
+2. **Guarantees.** Core's `Guarantee`, the `accept_unverified` lists, the
+   language server's acceptance code, the docs and granular `@unverified`.
+3. **Conformance features and report keys.** `features.json`, the spec
+   versions, and the Observatory's expected reports.
+4. **Annotations and settings keys.** Today unknown ones are silently ignored
+   (core#171, core#178). With entries they can be refused, completed in the
+   editor and documented from one place.
+5. **Diagnostic codes**, with explanations for the CLI and the language
+   server.
+6. **Fuzz, bench and other CI targets.** The CI matrices, the Observatory's
+   `expect:` lists and the READMEs are generated from a set.
+
+## Sets
+
+A set is a query, so it can't drift from the entries (illustrative):
+
+```cue
+sets: {
+    wire_formats:     [for id, e in encodings if e.kind == "format" {id}]
+    nightly_fuzz:     [for id, e in targets if e.kind == "fuzz-target" && list.Contains(e.tags, "nightly") {id}]
+    format_facts:     [for id, f in facts if f.applies_to == "format" {id}]
+    "spec-0.10":      [for id, f in features if f.since <= "spec-0.10" {id}]
+}
+```
+
+A consumer asks for a set by name. Generated code exposes the sets that code
+needs as constants: a `&[&str]`, an enum, a TypeScript union.
+
+## Relations
+
+**Leaning: plain references.** The catalog could stop at *what exists*, or it
+could also state the rules that connect entries:
+
+- a handshake **establishes** guarantees (`comline@1` → schema and encoding agreement);
+- an encoding with vectors **keeps** `encoding_conformance`;
+- a framing's `payload` must **fit** a format's `output` (the encoding-pair rule);
+- `comline@2`'s `same_version_differs = warn` **gives up** `version_honesty`.
+
+Today each of these is code in core (`unverified::causes`, `misfit`), and
+some are repeated in the generators. Stating them as data means the compiler,
+the conformance engine, the language server and the docs all apply one set of
+rules, and a third party's declarations get the same rules. The cost is that
+the rule language has to stay small. So the catalog states the relations that
+are plain references (establishes, keeps, gives up, applies to, scopes), and
+logic that compares values (`fit`) stays in code that reads the catalog.
+
+## Where it lives
+
+**Leaning: a spec repository, `specification`.** Third parties never edit the catalog: they
+declare their own entries (`com.acme.f@1`) in `config.idp`, in the same shape.
+What they need from it is what they implement against: the names, the facts
+and their domains, and the conformance cases that prove them. That is the
+spec, and today its other half, the conformance specs and vectors, sits in
+`runtime/conformance`, although a Go or Swift runtime implements against those
+and not against the Rust runtime.
+
+So the vocabulary lives in **one spec repository** with:
+
+- the catalog (CUE);
+- the conformance specs (`profile.cue`, `features.json`) and vectors, moved out
+  of `runtime/conformance`;
+- compiler conformance cases (see [granular `@unverified`](granular-unverified.md#testing-the-invariant));
+- generated outputs: a `no_std` Rust crate, a TypeScript module, and JSON for
+  everything else.
+
+It is versioned as the spec ("spec 0.10" is already how the conformance
+corpus is versioned). Everyone, this project's own core, runtime and
+generators included, pins the spec the way a third party would. The Rust
+conformance engine and reference stay in `runtime`.
+
+The options that were weighed:
+
+| | Spec repository | Vocabulary-only repository | In `core` |
+|---|---|---|---|
+| What a third party pins | the whole spec: names, facts, vectors and cases | the names, and the vectors separately from `runtime` | a Rust compiler's repository, and every core release |
+| Language-neutral | yes: CUE and JSON | yes | no |
+| Cost | one more repository, plus moving the conformance corpus | one more repository | lowest |
+
+**Format: CUE as the source.** It is already used for the conformance specs,
+it validates (a fact's value must be in its domain), it computes sets, and it
+exports JSON. Generated outputs are committed and checked in CI, the same way
+`comline.h` is checked against cbindgen.
+
+## Versioning
+
+The spec version and the IR format version stay **independent**:
+
+- **The spec version** (the vocabulary, the conformance corpus and the compiler
+  cases) says what implementations must agree on.
+- **The IR format version** (`CURRENT_IR_FORMAT_VERSION` in core's CAS) changes
+  only when the frozen IR's *shape* changes.
+- **Each frozen version records the spec version** it was frozen against.
+- **The spec is append-only for anything frozen.** Wire names never change.
+  Guarantees, facts and values can be added and deprecated, but never removed
+  or redefined, so an old frozen version always reads correctly under a newer
+  spec. From 1.0 this is what lets a newer release read an older one's IR
+  (core#146).
+
+## How each consumer reads it
+
+| Consumer | Reads | Replaces |
+|---|---|---|
+| **core** | Generated Rust: guarantees, facts, value domains, official encodings, aliases, annotations, settings keys, diagnostic codes. At build time, a package's own encoding declarations merge in with the same shape. | `Guarantee::name`, `encodings/profile.rs`, `official.rs`'s tables, `official_units.json` |
+| **runtime** | Generated Rust constants: `FORMAT_*`, `FRAMING_*`, `HANDSHAKE_*`, the conformance `Fact` names, feature ids. | `contract/names.rs`, `Fact::name`, `features.json` |
+| **conformance specs** | The CUE directly. | the fact domains in `profile.cue` |
+| **generators** | Generated Rust/TS: names, plus titles for generated docs. | strings in `generation`, comline-rust and comline-typescript |
+| **language server** | Generated Rust: completion, hover and quick fixes, deprecations with replacements. | its own lists and acceptance strings |
+| **Observatory** | JSON: the expected report keys per set. | `expect:` lists in workflows |
+| **CI** | Generated matrices (fuzz targets, bench targets). | hand-kept YAML lists |
+| **docs** | Generated tables (encodings, facts, guarantees, features). | hand-kept tables |
+
+## The case for it
+
+- **One edit per change.** Adding a fact value, deprecating an alias or adding
+  a fuzz target touches the catalog and nothing else.
+- **Unknown names become errors.** Typos in annotations, settings keys and
+  acceptances stop passing silently.
+- **Tooling for free.** The language server and docs get descriptions and
+  deprecations without separate upkeep.
+- **Third parties are judged by the same rules,** as with the encoding-pair facts.
+
+## The case against
+
+- **One more thing to version and pin,** in a project where revs already cascade
+  across repositories.
+- **Generated code in every repository** needs a regeneration check in CI.
+- **Rules as data** can grow into a language of its own if relations aren't
+  kept to plain references.
diff --git a/docs/docs/proposals/shared-vocabulary/granular-unverified.md b/docs/docs/proposals/shared-vocabulary/granular-unverified.md
new file mode 100644
index 0000000..870e4c7
--- /dev/null
+++ b/docs/docs/proposals/shared-vocabulary/granular-unverified.md
@@ -0,0 +1,244 @@
+# Granular `@unverified`
+
+Status: **draft** · part of [A shared vocabulary](index.md) · revisits part
+of [Marking a given-up guarantee](../guarantee-marker/index.md)
+
+**The question.** `@unverified = "reason"` marks a whole protocol, with one
+reason, and core works out which guarantees it gives up. Should the author
+be able to name the guarantees, give each its own reason, and mark less than
+a whole protocol, without making it any easier to lose a guarantee unnoticed?
+
+## What was decided, and what it already covers
+
+[Proposal C](../guarantee-marker/unverified.md) was chosen over naming the
+guarantees ([A](../guarantee-marker/waives.md), [B](../guarantee-marker/assumes.md)),
+because naming them "would only repeat" what core computes. Two refinements
+closed most of the risk:
+
+- a consumer's `accept_unverified` records the **set** core worked out, so a
+  dependency that gives up one more guarantee needs a new acceptance;
+- the set is **frozen** into the compiled schema, so the author's own version
+  comparison reports it growing as a major change.
+
+Those stay. This proposal doesn't reopen *whether* core computes the set.
+
+## What it doesn't cover
+
+1. **One reason for everything.** A protocol that gives up
+   `encoding_conformance` (a framing without vectors) and `bounded_size` (an
+   unbounded `bytes` argument) explains both in one string. Generated docs and
+   hover text can't say which reason belongs to which guarantee, and for a
+   third-party encoding they can't name the cause at all (generation#93).
+2. **The scope is always the protocol.** `bounded_size` comes from a type: one
+   unbounded argument anywhere a protocol reaches marks the whole protocol,
+   and the diagnostic says only "a string, list or nesting it reaches has no
+   maximum".
+3. **The schema text doesn't say what's given up.** This was accepted for C,
+   on the grounds that tooling shows it. With a shared vocabulary, writing it
+   costs little, and a reviewer reading a diff sees it without tooling.
+4. **The author's acknowledgement is implicit.** The version comparison catches
+   the set growing *between releases*. While a change is being developed, a
+   marker written for one guarantee silently covers a second.
+5. **Chains across packages aren't explicit.** When package A's type gives up a
+   guarantee, B uses it, and C uses B, nothing requires B and C to see A's
+   cause and acknowledge it themselves.
+
+## The safety invariant
+
+Everything below serves one rule, which has to hold with no exceptions:
+
+> **If a package compiles, every guarantee given up anywhere a protocol
+> reaches, through any chain of types and packages, has been acknowledged in
+> that package and accepted by every consumer of that protocol. Every
+> acknowledgement and acceptance is pinned to the exact causes it covered,
+> so any change upstream asks again.**
+
+## Proposal
+
+### Two forms, at any scope
+
+`@unverified = "reason"` stays valid. An optional keyed form names
+guarantees. Both can be written at any scope a given-up guarantee allows:
+
+```ids
+@framing = "com.acme.f@1"
+@unverified(encoding_conformance = "com.acme.f@1 ships no vectors yet")
+protocol Billing {
+    function charge(order: Order) -> Receipt;
+
+    function upload(
+        @unverified(bounded_size = "legacy gateway blob, sized by the gateway")
+        data: bytes
+    );
+}
+```
+
+- **Plain:** acknowledges whatever core computes at that scope, as today.
+- **Keyed:** each key is a guarantee from the vocabulary, each value its
+  reason. Against what core computes:
+    - a computed guarantee that isn't named is an **error**;
+    - a named guarantee that isn't given up is a **warning**, like a needless
+      marker today;
+    - an unknown key is an **error**, with spellings suggested from the vocabulary.
+
+### Scopes come from each guarantee
+
+A guarantee's scopes follow from where its cause sits, and are stated in its
+catalog entry. A new guarantee declares its own scopes, and core needs no
+special case for it.
+
+| Guarantee | Comes from | Scopes |
+|---|---|---|
+| `schema_agreement`, `encoding_agreement` | the handshake | package, protocol |
+| `version_honesty` | `comline@2` policies | package, protocol |
+| `encoding_conformance` | the format and framing | package, protocol |
+| `bounded_size` | types | protocol, function, argument, field, type |
+
+A marker at a scope its guarantee doesn't allow is an error.
+
+### Coverage: outer covers inner, strict on request
+
+By default a marker covers causes inside it: a protocol-level `bounded_size`
+covers one unbounded argument, exactly as today, so nothing existing breaks.
+Tooling suggests the narrower placement.
+
+A package can opt into **strict** (`annotations.unverified.strict = true`). The
+keyed form is then required, and each marker must sit at the innermost scope
+where its cause is. That suits packages that want every given-up guarantee
+named where it happens.
+
+### Chains: once per package, never inherited
+
+Computing stays transitive, and **a marker never subtracts** from it. Core
+walks every type a protocol reaches, into dependencies' frozen IR, and finds
+every cause. A marker only acknowledges.
+
+Acknowledgement is **per package, never inherited:**
+
+```text
+A::Blob = bytes              A marks it:  @unverified(bounded_size = "legacy gateway")
+B::Upload { data: A::Blob }  B must acknowledge it (on Upload, the field, or a protocol reaching it)
+C::Order  { blob: B::Upload } C must acknowledge it too
+```
+
+- Each package whose types or protocols reach a cause acknowledges it **once**,
+  anywhere on the path inside that package. Within one package the author
+  already sees the path; every package boundary asks again.
+- A's reason travels along as the **origin**, and is shown at every hop, but
+  A's marker satisfies only A.
+- Diagnostics, `inspect`, hover and generated docs show the whole chain:
+  *"`C::Orders` gives up `bounded_size`: `C::Order.blob` → `B::Upload.data` →
+  `A::Blob` (`bytes` without a maximum). A's reason: 'legacy gateway'."*
+
+### Pinned to the causes
+
+An acknowledgement, and a consumer's acceptance, records what it covered: each
+guarantee with the **chain to each cause**. If A adds a second unbounded field,
+or B swaps `A::Blob` for another unverified type, the record no longer
+matches, and B, C and every consumer get an error until they acknowledge
+again. A guarantee can't be lost by reuse, however many packages it passes
+through.
+
+What's frozen is therefore (guarantee, scope path, chain to the cause,
+reason). Narrowing a marker is not a major change, since nothing more is
+given up. Widening one, or adding a cause, is.
+
+### Package-default causes: acknowledged next to the cause
+
+A package setting can give a guarantee up for every protocol that inherits
+it, for example `handshake = "none"` in `config.idp`. Its acknowledgement sits
+beside that setting:
+
+```text
+handshake = "none"
+unverified = { schema_agreement = "the gateway pins schemas by contract",
+               encoding_agreement = "the gateway pins schemas by contract" }
+```
+
+- It covers **only the causes that come from that setting**, and only for the
+  protocols that inherit it. A protocol with its own handshake isn't
+  covered, and neither is any other cause (an unbounded type, a framing
+  without vectors).
+- Each covered protocol's frozen record says it was acknowledged at package
+  scope, with the reason.
+- It is pinned like any other marker: if the setting changes, it no longer
+  matches and the build asks again.
+- A blanket package marker covering everything in a package is ruled out.
+  That is exactly the gap this proposal closes.
+
+### Acceptance stays per protocol
+
+`accept_unverified = { Billing = [...] }` accepts the protocol's whole frozen
+set, inner scopes and chains included. It is pinned like an acknowledgement,
+so a new inner cause still asks for re-acceptance.
+
+### A newer spec that finds an existing loss
+
+The spec can add a guarantee (say, a future "transport fit"), and an existing
+protocol may turn out to give it up although its schema didn't change.
+
+- **Safety:** markers and acceptances are pinned to a set that no longer
+  matches, so the author and every consumer are asked again. Nothing passes
+  silently.
+- **Version honesty:** `diff` recomputes both versions under the newer spec
+  before comparing, so the version comparison doesn't report a major change
+  the author didn't make. The frozen IR keeps the types and parameters this
+  needs.
+
+### Fail closed
+
+If the build can't see a dependency's declarations or IR, it counts the
+guarantee as given up and refuses. An editor's incomplete view can show a
+warning instead, but a build never judges with less than the full picture.
+Any path that does is a safety bug. Known today: `compat` and `diff` don't see
+a dependency's encoding declarations (core#206).
+
+## Testing the invariant
+
+Today there are unit tests (`core/tests/package/unverified.rs`), fuzz targets
+for parsing and compiling robustness, and runtime vectors proving that decoders
+refuse values over a bound. Nothing tests the invariant across package graphs.
+This proposal adds:
+
+1. **A property test with an independent oracle,** in core. It generates
+   random package graphs (bounded and unbounded types, chains across
+   packages, markers at random scopes, acceptances, upstream changes) and checks
+   that *the build succeeds exactly when the oracle says every hop acknowledged
+   and every consumer accepted*. It's the same differential idea as the
+   runtime's `ffi_vs_core`.
+2. **A fuzz target** running the same check over arbitrary graphs, in core's
+   nightly fuzz CI.
+3. **Compiler conformance cases** in the spec repository: schema graphs with
+   their expected given-up sets, chains and errors, as data. Any compiler, the
+   language server or another tool must reproduce them, the way runtimes must
+   reproduce bytes today.
+4. **An audit** of every place that judges guarantees (the validator,
+   `compat`, `diff`, `inspect`, the language server) for any path that can see
+   less than the full picture.
+
+## Options considered
+
+| | A. Today, plus narrower scopes | B. Plain or keyed (proposed) | C. Keyed only |
+|---|---|---|---|
+| Existing schemas | unchanged | unchanged | all must be rewritten |
+| Says what's given up, in the text | no | when keyed, always under strict | always |
+| A reason per guarantee | no | yes | yes |
+| Catches a second guarantee while developing | no | when keyed, and always under strict | yes |
+| Repeats what core computes | no | only where the author chooses | always, which was the objection to the earlier Proposal A |
+
+## Depends on
+
+- **The vocabulary**, for guarantee names, descriptions and scopes.
+- **Keyed annotation values** (core#124). Today an annotation's value is a
+  scalar, and a list is parsed as validator calls.
+- **Markers on arguments and fields.** Check this against how bounds attach
+  today (core#98).
+
+## The word
+
+`@unverified` for both forms. The objection to the earlier `@waives(…)` was to
+naming guarantees at all, not to the word. Now that naming is optional and
+checked, the choice is about readability. `@unverified(bounded_size = "…")`
+reads accurately: Comline doesn't verify it. And one word already runs through
+the annotation, `accept_unverified`, `annotations.unverified` and the
+`unverified::*` diagnostic codes.
diff --git a/docs/docs/proposals/shared-vocabulary/index.md b/docs/docs/proposals/shared-vocabulary/index.md
new file mode 100644
index 0000000..81a899b
--- /dev/null
+++ b/docs/docs/proposals/shared-vocabulary/index.md
@@ -0,0 +1,118 @@
+# A shared vocabulary
+
+Status: **draft** · two parts, read in order:
+[the catalog](catalog.md), then [granular `@unverified`](granular-unverified.md)
+
+**The question.** Comline names many things that several programs have to
+agree on: encodings, handshakes, guarantees, facts and their values,
+conformance features, annotations, settings keys, diagnostic codes, and fuzz,
+bench and report targets. Every repository that needs a name writes it out
+as a string and keeps its own list of the sets it belongs to. **Can those names,
+and the sets made from them, be defined once and shared by core, the compiler,
+the runtimes, the generators, the language server, the Observatory and the
+docs?**
+
+A second question depends on the first. `@unverified` marks a protocol as
+giving up guarantees, but the author can't say *which* ones, give each its
+own reason, or mark less than a whole protocol. Once guarantees are entries in
+a shared vocabulary, a marker can refer to them.
+
+## What it looks like today
+
+A name is a literal, copied wherever it's needed:
+
+| Name | Kind | Written in |
+|---|---|---|
+| `packed@1`, `comline@2` | encoding, handshake | runtime (~46 files), core (~20), docs (~40), language server |
+| `framing-datagram` | conformance feature | runtime, core, comline-typescript, docs |
+| `struct_fields`, `unknown_variant` | fact | core's `encodings/profile.rs`, runtime's conformance `profile.rs` (an enum and a hand-written `match` to strings), the conformance CUE specs, docs |
+| `schema_agreement`, `bounded_size` | guarantee | core's `Guarantee` (an enum and a `match`), `config.idp` acceptances, the language server, docs |
+| `packed_canonical` | fuzz target | the fuzz `Cargo.toml`, two lists in `fuzz.yml`, the fuzz README, the seed generator |
+
+Sets are kept by hand too. *Which fuzz targets exist*, *which features a spec
+version covers*, *which values `calls` can take* and *which names are wire
+formats* each live in a CI matrix, a JSON file, a `match` arm or a completion
+list. Adding or renaming a name means finding every copy, and nothing checks
+that the copies agree.
+
+Some of the structure already exists. The conformance specs' `profile.cue`
+gives each fact its value domain and how it is proven. Core's
+`encodings/profile.rs` lists the same facts again, and resolves aliases
+(`jsonrpc`, `json-rpc`) in `official.rs`.
+
+## What this proposes
+
+1. **[A catalog](catalog.md):** every shared name becomes an entry with a
+   stable id, a kind, tags, metadata and, where it applies, a value domain,
+   aliases, a status and relations to other entries. Sets are queries over
+   kinds and tags. Each consumer reads the catalog, or code generated from it,
+   instead of keeping its own copy. Official entries and a package's own
+   declarations (`com.acme.f@1`) have the same shape.
+2. **[Granular `@unverified`](granular-unverified.md):** the marker may name
+   the guarantees it covers, each with its own reason, and may apply at the
+   scope a guarantee naturally has (a protocol, a function, an argument).
+   Core keeps working out what is given up, and checks it against what the
+   author wrote. This revisits part of the
+   [guarantee-marker decision](../guarantee-marker/index.md); that page's
+   last open question asks for exactly this fixed vocabulary of guarantees.
+
+## Rules that hold whatever the details
+
+- **A published wire name never changes.** `packed@1` and `comline@2` are hashed
+  into the handshake, so their spelling is protocol. A rename is a new entry,
+  with the old one deprecated.
+- **Third parties are first-class.** Anything the catalog can say about an
+  official encoding, a package can say about its own, and the same rules
+  judge both (as for the encoding-pair facts).
+- **Nothing new at run time.** The catalog feeds compilers, generators,
+  tooling and CI. Runtimes keep compile-time constants, with no lookup on the
+  call path.
+- **One change, every consumer.** Adding a name, a value or a set member is an
+  edit to the catalog plus regeneration. Hand-kept copies are a bug.
+
+## Rollout
+
+In stages, each useful on its own, in the order the encoding-facts work used:
+
+1. **The spec repository** ([catalog → where it lives](catalog.md#where-it-lives)):
+   the catalog in CUE, seeded from `profile.cue`, core's `Guarantee` and the
+   official encodings, with the conformance specs and vectors moved in from
+   `runtime/conformance`.
+2. **Core reads it:** guarantees, facts, value domains, aliases and official
+   encodings come from the catalog. Unknown annotation names, settings keys
+   and diagnostic codes are refused (core#171, core#178).
+3. **The runtime and conformance read it:** fact names, conformance
+   features, and the fuzz and bench target sets. The CI matrices and the
+   Observatory's expected reports are generated from it.
+4. **Granular `@unverified`** in core: grammar, scopes, per-package
+   acknowledgement pinned to each cause's chain, and freezing. It needs
+   keyed annotation values (core#124). It lands with its safety tests: a
+   property test against an oracle, a fuzz target, compiler conformance cases
+   in the spec repository, and an audit of every path that judges guarantees.
+5. **Tooling reads it:** language server completion and hover, generated
+   `@unverified` docs (generation#93), and the docs tables.
+
+## Leanings so far
+
+- **Home:** a spec repository, `specification`, holding the catalog, the conformance specs and
+  vectors, and compiler conformance cases, versioned as the spec.
+- **Format:** CUE as the source, with generated Rust, TypeScript and JSON.
+- **Relations:** plain references only (establishes, keeps, gives up, applies
+  to, scopes); logic that compares values stays in code.
+- **`@unverified`:** plain or keyed, at any scope a guarantee allows. Outer
+  covers inner, with a strict opt-in. Acknowledged once per package along a
+  chain, pinned to the chain, accepted per protocol, failing closed.
+
+- **Package defaults:** acknowledged in `config.idp` next to the setting that
+  causes the loss, covering only that cause.
+- **Spec upgrades:** a loss found by a newer spec asks the author and consumers
+  again, and `diff` recomputes both versions under it, so it is never a false
+  major change.
+- **Versions:** the spec version and the IR format version are independent,
+  with each frozen version recording its spec version, and the spec
+  append-only for anything frozen.
+- **The word:** `@unverified` for both forms.
+
+## Open questions
+
+None blocking. The next step is the `specification` repository (core#220).
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
index f97f52d..18fe4b0 100755
--- a/docs/mkdocs.yml
+++ b/docs/mkdocs.yml
@@ -225,6 +225,10 @@ nav:
       - 'Proposal B': 'proposals/guarantee-marker/assumes.md'
       - 'Proposal C': 'proposals/guarantee-marker/unverified.md'
       - 'Proposal D': 'proposals/guarantee-marker/unchecked.md'
+    - 'A shared vocabulary':
+      - 'proposals/shared-vocabulary/index.md'
+      - 'The catalog': 'proposals/shared-vocabulary/catalog.md'
+      - 'Granular @unverified': 'proposals/shared-vocabulary/granular-unverified.md'
 
 extra_css:
   - stylesheets/nav.css?v=23   # bump on every nav.css change — it is not cache-busted otherwise