diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -100,6 +100,117 @@
 68-65-6C-6C-6F
 ```
 
+### Atoms
+
+Which λ functions exist is a property of the object model being dataized, not
+of the calculus, so `phino` implements none of them. They come from a JSON
+registry given with `--atoms`, keyed by λ name:
+
+```json
+{
+  "L_number_plus": {
+    "rt": "node",
+    "script": "const fs = require('fs'); ..."
+  }
+}
+```
+
+The `rt` field names the executable the `script` is run under. Only `node` is
+supported for now; a registry naming any other runtime is refused when the file
+is read, before dataization starts.
+
+When 𝔼 reaches a λ function the registry carries, `phino` writes its `script`
+to a temporary file and runs it as a POSIX process under that interpreter, with
+the λ name as the first command-line argument:
+
+```text
+node /tmp/phino-atom-4f2a.js L_number_plus
+```
+
+The name matters: one script may be registered under several λ names and branch
+on it, which is where `node` puts it — `process.argv[2]`. The script is then
+fed one JSON object on `stdin`:
+
+```json
+{
+  "b": "⟦ x ↦ Φ.number( as-bytes ↦ … ), ρ ↦ ⟦ … ⟧ ⟧",
+  "s": "⟦ bytes ↦ ⟦ … ⟧, number ↦ ⟦ … ⟧, φ ↦ … ⟧"
+}
+```
+
+Here `b` is the formation being evaluated, with its λ binding removed so that
+the script may dispatch on it, and `s` is the universe Φ. Both are canonical
+𝜑-calculus on a single line — no syntax sugar, whatever `--sweet` says about
+the output of the run — so a script never has to know about `phino`'s sugar in
+order to find a datum: every byte array is spelled out as a Δ binding.
+
+The script writes one JSON object to `stdout`:
+
+```json
+{ "n": "11" }
+```
+
+The `n` field is the 𝜑-expression the atom answers with, in any syntax
+`phino`'s parser reads — syntax sugar included, so the `11` above and the
+`Φ.number( … )` it stands for are the same answer. `phino` parses it back
+and hands it to 𝔼 as the atom's raw result, normalizing it exactly as it
+normalizes anything else, so `--evaluations`, `--partial` and `--max-steps`
+keep working unchanged. A non-zero exit, output that is not JSON, a missing
+`n` or an `n` that does not parse fails the run, with the script's own
+`stderr` in the message.
+
+A λ name the registry does not carry has no λ function at all, so 𝔼 gets stuck
+on it. Without `--atoms` the registry is empty and every atom gets stuck.
+
+### Reducing the operands of an atom
+
+A script gets at the parts of `b` by calling `phino` again, so no API has to be
+exposed for it. The `--inside` option is how it asks: the expression it names
+is bound to a fresh synthetic attribute of the input expression, which the run
+takes as the universe, normalized there, and then dataized. This is the same
+trick `phino` plays internally whenever it has to reduce a sub-expression the
+program does not contain:
+
+```bash
+$ phino dataize --atoms=atoms.json --inside='5.plus( 6 )' universe.phi
+40-26-00-00-00-00-00-00
+```
+
+Here `universe.phi` is the 𝜑-program the atom is being fired inside — the very
+text the script was handed as `s`, which it feeds back on `stdin`.
+
+So a `L_number_plus` that reduces its own operands reads like this:
+
+```js
+const fs = require('fs');
+const { execFileSync } = require('child_process');
+const atom = process.argv[2];
+if (atom !== 'L_number_plus') {
+  throw new Error(`unsupported atom ${atom}`);
+}
+const { b, s } = JSON.parse(fs.readFileSync(0, 'utf8'));
+const dataized = (expr) => execFileSync(
+  'phino',
+  ['dataize', '--atoms=atoms.json', `--inside=${expr}`],
+  { input: s, encoding: 'utf8' }
+).trim();
+const number = (expr) => Buffer.from(dataized(expr).replace(/-/g, ''), 'hex').readDoubleBE(0);
+const sum = Buffer.alloc(8);
+sum.writeDoubleBE(number(`${b}.ρ`) + number(`${b}.x`));
+const hex = [...sum]
+  .map((octet) => octet.toString(16).toUpperCase().padStart(2, '0'))
+  .join('-');
+process.stdout.write(JSON.stringify({
+  n: `Φ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ ${hex} ⟧ ) )`
+}));
+```
+
+The `--inside` option cannot be combined with `--locator`, since it aims the
+run at the binding it mints itself. Both `dataize` and `morph` take `--atoms`
+and `--inside`.
+
+### Recording what fired
+
 Every atom fired on the way to the bytes may be recorded in a machine-readable
 protocol, with the `--evaluations` option. One firing is one line of three
 tab-separated fields: the name of the λ function, the formation it was applied
@@ -112,7 +223,8 @@
   number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
   φ ↦ 5.plus( 6 )
 ⟧
-$ phino dataize --evaluations=atoms.tsv --quiet --sweet --hide-rho sum.phi
+$ phino dataize --atoms=atoms.json --evaluations=atoms.tsv --quiet \
+    --sweet --hide-rho sum.phi
 $ cat -T atoms.tsv
 L_number_plus^I⟦ x ↦ 6 ⟧^I11
 ```
@@ -122,14 +234,16 @@
 beginning of every run, and `--output=phi` is the only output format it
 works with, since one record must fit into one line.
 
-An atom that cannot fire fails the run: its λ function is unknown to phino,
-or one of its inputs reaches such an atom. This is what happens when a
-data input is replaced on purpose by a placeholder formation, such as
-`⟦ λ ⤍ Sym_arg_0 ⟧`. With `--partial`, dataization becomes partial
-evaluation instead: what the known inputs decide is computed, the rest
-survives as the residual program, which is printed in place of the bytes,
-and the run ends successfully:
+### Partial evaluation
 
+An atom that cannot fire fails the run: its λ function is not in the registry
+given with `--atoms`. This is what happens when an operation is deliberately
+left unimplemented — a data input replaced by a placeholder formation such as
+`⟦ λ ⤍ Sym_arg_0 ⟧`, or an operation whose answer is not known yet. With
+`--partial`, dataization becomes partial evaluation instead: what the known
+inputs decide is computed, the rest survives as the residual program, which is
+printed in place of the bytes, and the run ends successfully:
+
 ```bash
 $ cat partial.phi
 ⟦
@@ -137,29 +251,29 @@
   number(as-bytes) ↦ ⟦
     φ ↦ as-bytes,
     plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
-    times(x) ↦ ⟦ λ ⤍ L_number_times ⟧
+    times(x) ↦ ⟦ λ ⤍ L_number_times ⟧,
+    as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧
   ⟧,
-  φ ↦ 2.times(3).plus(⟦ λ ⤍ Sym_arg_0 ⟧)
+  φ ↦ 2.times( 3 ).plus( 4 ).as-bool
 ⟧
-$ phino dataize --partial --sweet --hide-rho partial.phi
-⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧, λ ⤍ L_number_plus ⟧
+$ phino dataize --atoms=atoms.json --partial --sweet --hide-rho partial.phi
+⟦ λ ⤍ L_number_as_bool ⟧
 ```
 
-Here `2.times(3)` was decided by literals, so it was computed (its result,
-`6`, sits in the hidden `ρ` of the residual program), while `plus` waits
-for an `x` no atom can produce, so it stays in place as a normal-form
-subterm. Each such stuck site also lands in the `--evaluations` file, as a
-record with the first two fields only, since there is no result to report;
-the inner stuck atom comes first, then the known atom whose input reached
-it:
+Here `2.times( 3 ).plus( 4 )` was decided by the atoms the registry carries, so
+it was computed (its result, `10`, sits in the hidden `ρ` of the residual
+program), while `as-bool` names a λ function no script answers for, so it stays
+in place as a normal-form subterm. Each such stuck site also lands in the
+`--evaluations` file, as a record with the first two fields only, since there is
+no result to report:
 
 ```bash
-$ phino dataize --partial --evaluations=atoms.tsv --quiet \
+$ phino dataize --atoms=atoms.json --partial --evaluations=atoms.tsv --quiet \
     --sweet --hide-rho partial.phi
 $ cat -T atoms.tsv
 L_number_times^I⟦ x ↦ 3 ⟧^I6
-Sym_arg_0^I⟦⟧
-L_number_plus^I⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧ ⟧
+L_number_plus^I⟦ x ↦ 4 ⟧^I10
+L_number_as_bool^I⟦⟧
 ```
 
 Evaluation stays demand-driven, as the calculus prescribes: an argument
@@ -193,9 +307,9 @@
   number(as-bytes) ↦ ⟦ φ ↦ as-bytes, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
   φ ↦ 5.plus( 6 ).plus( 7 )
 ⟧
-$ phino dataize --sweet --hide-rho two.phi
+$ phino dataize --atoms=atoms.json --sweet --hide-rho two.phi
 40-32-00-00-00-00-00-00
-$ phino morph --locator=Q.φ --sweet --hide-rho two.phi
+$ phino morph --atoms=atoms.json --locator=Q.φ --sweet --hide-rho two.phi
 ⟦ x ↦ 7, λ ⤍ L_number_plus ⟧
 ```
 
@@ -214,9 +328,9 @@
 ⊥
 ```
 
-The whole `dataize` option surface applies unchanged — `--sequence`,
-`--headers`, `--steps-dir`, `--evaluations`, `--partial`, `--max-steps`,
-`--shuffle`/`--seed`, `--output`, `--focus` and the rest.
+The whole `dataize` option surface applies unchanged — `--atoms`, `--inside`,
+`--sequence`, `--headers`, `--steps-dir`, `--evaluations`, `--partial`,
+`--max-steps`, `--shuffle`/`--seed`, `--output`, `--focus` and the rest.
 
 ## Rewrite
 
@@ -550,7 +664,29 @@
 * `!d` || `δ` - bytes in meta delta binding
 * `!F` || `𝑓` - function name in meta lambda binding
 
-Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`.
+A meta variable carries a suffix, like `!B1` or `𝜏0`, to name what it
+captured, so that the `result`, `when`, `where` and `having` of a rule can
+read it back.
+
+Written bare, with no suffix at all, a meta variable is anonymous: it matches
+whatever term stands in its place, every occurrence on its own, and binds no
+name. Two anonymous metas of one kind are therefore two different captures,
+which is what lets a pattern ask for any two attributes without inventing
+names for them:
+
+```yaml
+name: two-attributes
+pattern: '⟦ 𝜏 ↦ 𝑒, 𝜏 ↦ 𝑒 ⟧'
+result: '⟦ x ↦ ⟦ Δ ⤍ 2A- ⟧ ⟧'
+```
+
+Spelled with suffixes, that pattern would read `⟦ 𝜏1 ↦ 𝑒1, 𝜏2 ↦ 𝑒2 ⟧` and
+name four captures the result never mentions, while `⟦ 𝜏1 ↦ 𝑒1, 𝜏1 ↦ 𝑒1 ⟧`
+would be rejected as a duplicated attribute.
+
+Nothing can refer to an anonymous meta, since it has no name to be referred to
+by. Writing one outside a `pattern` (or the `match`, `e-match` and `c-match` of
+an inference rule) is a mistake in the rule and is reported as the rule loads.
 
 A positional (α) application argument is written as `α0`, `~0` (ASCII), or
 `α𝑖`/`~!i` when its index is captured by an `!i`/`𝑖` meta variable.
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.116
+version: 0.0.117
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -35,6 +35,7 @@
   import: warnings
   exposed-modules:
     AST
+    Atoms
     Builder
     Bytes
     Canonizer
@@ -69,6 +70,7 @@
     Replacer
     Rewriter
     Rule
+    Slots
     Sugar
     Tau
     XMIR
@@ -94,6 +96,7 @@
     gitrev >=1.3.1 && <1.4,
     megaparsec >=9.5 && <9.9,
     optparse-applicative >=0.18 && <0.20,
+    process >=1.6.17 && <1.7,
     random >=1.2 && <1.4,
     regex-pcre-builtin >=0.95.2 && <0.96,
     scientific >=0.3.7 && <0.4,
@@ -125,6 +128,7 @@
   hs-source-dirs: test
   other-modules:
     ASTSpec
+    AtomsSpec
     BuilderSpec
     BytesSpec
     CanonizerSpec
@@ -138,6 +142,7 @@
     EncodingSpec
     FilesSpec
     FilterSpec
+    Fixtures
     FunctionsSpec
     LaTeXSpec
     LiningSpec
diff --git a/resources/contextualization.yaml b/resources/contextualization.yaml
--- a/resources/contextualization.yaml
+++ b/resources/contextualization.yaml
@@ -17,63 +17,65 @@
 # 'c-result' (a premise meta or a literal), provided the ordered 'premises'
 # reduce as stated. A premise binds its 'n-result' to one 𝒞 ('contextualize')
 # judgment. 'c-match' is the context-argument matcher of 𝒞(n, c); it is always
-# the c meta. Derived terms are named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is
-# skipped only when 'match' already binds it.
+# the 𝑘0 meta. Derived terms are named 𝑛1, 𝑛2, … in premise order; the term 𝒞 is
+# handed is 𝑛0, leaving that numbering to the premises alone. A meta the rule
+# never reads back is written bare: it matches whatever stands in its place,
+# binds nothing and cannot be referenced.
 
 - name: cg
   match: Φ
-  c-match: 𝑘
+  c-match: 𝑘0
   c-result: Φ
 
 - name: cxi
   match: ξ
-  c-match: 𝑘
-  c-result: 𝑘
+  c-match: 𝑘0
+  c-result: 𝑘0
 
 - name: ct
   match: ⊥
-  c-match: 𝑘
+  c-match: 𝑘0
   c-result: ⊥
 
 - name: cf
-  match: ⟦𝐵⟧
-  c-match: 𝑘
-  c-result: ⟦𝐵⟧
+  match: ⟦𝐵0⟧
+  c-match: 𝑘0
+  c-result: ⟦𝐵0⟧
 
 - name: cd
-  match: '𝑛.𝜏'
-  c-match: 𝑘
-  c-result: '𝑛1.𝜏'
+  match: '𝑛0.𝜏0'
+  c-match: 𝑘0
+  c-result: '𝑛1.𝜏0'
   premises:
     - n-result: 𝑛1
       contextualize:
-        - 𝑛
-        - 𝑘
+        - 𝑛0
+        - 𝑘0
 
 - name: ca
-  match: '𝑛(𝜏 ↦ 𝑒1)'
-  c-match: 𝑘
-  c-result: '𝑛1(𝜏 ↦ 𝑛2)'
+  match: '𝑛0(𝜏0 ↦ 𝑒1)'
+  c-match: 𝑘0
+  c-result: '𝑛1(𝜏0 ↦ 𝑛2)'
   premises:
     - n-result: 𝑛1
       contextualize:
-        - 𝑛
-        - 𝑘
+        - 𝑛0
+        - 𝑘0
     - n-result: 𝑛2
       contextualize:
         - 𝑒1
-        - 𝑘
+        - 𝑘0
 
 - name: caa
-  match: '𝑛(α𝑖 ↦ 𝑒1)'
-  c-match: 𝑘
-  c-result: '𝑛1(α𝑖 ↦ 𝑛2)'
+  match: '𝑛0(α𝑖0 ↦ 𝑒1)'
+  c-match: 𝑘0
+  c-result: '𝑛1(α𝑖0 ↦ 𝑛2)'
   premises:
     - n-result: 𝑛1
       contextualize:
-        - 𝑛
-        - 𝑘
+        - 𝑛0
+        - 𝑘0
     - n-result: 𝑛2
       contextualize:
         - 𝑒1
-        - 𝑘
+        - 𝑘0
diff --git a/resources/dataization.yaml b/resources/dataization.yaml
--- a/resources/dataization.yaml
+++ b/resources/dataization.yaml
@@ -14,19 +14,21 @@
 # ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result'
 # to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate')
 # or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of
-# 𝔻(n, e); it is always the e meta. The single bytes result is named δ. A
+# 𝔻(n, e); it is always the 𝑒0 meta. The single bytes result is named δ0. A
 # normal-form-valued result (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate') is named
-# 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match' already binds
-# it; an expression-valued result (𝒞 'contextualize') is not a normal form —
-# that is why a 'normalize' premise follows it — so it takes an 𝑒-family name
-# (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe)
-# rather than an 𝑛 name reserved for normal forms.
+# 𝑛1, 𝑛2, … in premise order; the term 𝔻 is handed is 𝑛0, leaving that
+# numbering to the premises alone. An expression-valued result (𝒞
+# 'contextualize') is not a normal form — that is why a 'normalize' premise
+# follows it — so it takes an 𝑒-family name (𝑒1, 𝑒2, …, the next index free of
+# 'match', 𝑒0 itself being the universe) rather than an 𝑛 name reserved for
+# normal forms. A meta the rule never reads back is written bare: it matches
+# whatever stands in its place, binds nothing and cannot be referenced.
 #
 # The clauses are disjoint, so their relative order does not change behavior.
-# 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is
-# guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',
+# 'norm' matches the lone meta 𝑛0, which unifies with any expression, so it is
+# guarded to fire only when 𝑛0 is neither a formation ('not (formation 𝑛0)',
 # carving out 'delta', 'box', 'fire' and 'none') nor the termination ⊥
-# ('not (𝑛 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and
+# ('not (𝑛0 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and
 # lies outside its domain, so it deliberately matches no clause and dataization
 # stops there — there is no 'end' rule mapping ⊥ to empty bytes (see #955).
 # Without the guard 'norm' would behave correctly only by being declared last;
@@ -34,14 +36,14 @@
 
 - name: delta
   label: \Delta
-  match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧
-  e-match: 𝑒
-  d-result: δ
+  match: ⟦𝐵1, Δ ⤍ δ0, 𝐵2⟧
+  e-match: 𝑒0
+  d-result: δ0
 
 - name: box
   match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
-  e-match: 𝑒
-  d-result: δ
+  e-match: 𝑒0
+  d-result: δ0
   when:
     disjoint:
       - [Δ, λ]
@@ -53,47 +55,47 @@
         - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧
     - n-result: 𝑛1
       normalize: 𝑒2
-    - d-result: δ
+    - d-result: δ0
       dataize: 𝑛1
 
 - name: fire
-  match: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
-  e-match: 𝑒
-  d-result: δ
+  match: ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧
+  e-match: 𝑒0
+  d-result: δ0
   premises:
     - n-result: 𝑛1
       evaluate:
-        - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧
-        - 𝑒
-    - d-result: δ
+        - ⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧
+        - 𝑒0
+    - d-result: δ0
       dataize: 𝑛1
 
 - name: none
-  match: ⟦𝐵⟧
-  e-match: 𝑒
-  d-result: δ
+  match: ⟦𝐵0⟧
+  e-match: 𝑒0
+  d-result: δ0
   when:
     disjoint:
       - [Δ, λ, φ]
-      - [𝐵]
+      - [𝐵0]
   premises:
-    - d-result: δ
+    - d-result: δ0
       dataize: ⊥
 
 - name: norm
-  match: 𝑛
-  e-match: 𝑒
-  d-result: δ
+  match: 𝑛0
+  e-match: 𝑒0
+  d-result: δ0
   when:
     and:
       - not:
-          formation: 𝑛
+          formation: 𝑛0
       - not:
           eq:
-            - 𝑛
+            - 𝑛0
             - ⊥
   premises:
     - n-result: 𝑛1
-      morph: 𝑛
-    - d-result: δ
+      morph: 𝑛0
+    - d-result: δ0
       dataize: 𝑛1
diff --git a/resources/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -18,24 +18,26 @@
 # 'n-result' (a premise meta or a literal), provided 'when' holds and the
 # ordered 'premises' reduce as stated. A premise binds 'n-result' to the result
 # of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is
-# the universe-argument matcher of 𝕄(n, e); usually the e meta, but a rule may
+# the universe-argument matcher of 𝕄(n, e); usually the 𝑒0 meta, but a rule may
 # pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). Every judgment here is
 # normal-form-valued (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate' — 𝔼 normalizes its
-# atom's result internally), so results are named 𝑛, 𝑛1, … in premise order, the
-# bare 𝑛 skipped only when 'match' already binds it; the 𝑒-family stays reserved
-# for the universe 𝑒 itself.
+# atom's result internally), so premise results are named 𝑛1, 𝑛2, … in premise
+# order. The term a rule morphs is 𝑛0 and its universe 𝑒0, leaving that
+# numbering to the premises alone; the 𝑒-family stays reserved for the universe.
+# A meta the rule never reads back is written bare (see 'mad'): it matches
+# whatever stands in its place, binds nothing and cannot be referenced.
 #
 # 'ml' and 'md' are kept mutually exclusive: 'md' fires only
-# when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation
+# when its head 𝑛0 is not a formation ('not (formation 𝑛0)'), so every formation
 # head — λ-bearing or not — is left to 'ml' (and 'mf'). The two clauses
 # are disjoint and their relative order does not change behavior.
 #
 # 'ma'/'maa' and 'mad'/'maad' partition application-headed normal forms on
 # the argument's absoluteness (#959). Both pairs pin the argument to a
 # normal-form meta, so the split is total over the normal forms 𝕄 actually
-# sees: 'ma'/'maa' take a '𝑘' argument — absolute (xi-free) and in normal
+# sees: 'ma'/'maa' take a '𝑘1' argument — absolute (xi-free) and in normal
 # form — and recurse by re-normalizing the application; 'mad'/'maad' take an
-# '𝑛' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥
+# '𝑛1' argument (a normal form) that is 'not (absolute 𝑛1)' and yield ⊥
 # through a single 'morph: ⊥' premise, which terminates at once via the
 # 'dead' axiom (𝕄(⊥, e, s) → (⊥, s)) — no recursion. A non-absolute argument
 # can never fill a slot, so ⊥ is the correct outcome and morphing stays
@@ -46,91 +48,91 @@
 # re-morphed the identical stuck term forever.
 
 - name: mf
-  match: ⟦𝐵⟧
-  e-match: 𝑒
-  n-result: ⟦𝐵⟧
+  match: ⟦𝐵0⟧
+  e-match: 𝑒0
+  n-result: ⟦𝐵0⟧
 
 - name: ml
   label: \lambda
-  match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏'
-  e-match: 𝑒
+  match: '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧.𝜏0'
+  e-match: 𝑒0
   n-result: 𝑛3
   premises:
     - n-result: 𝑛1
       evaluate:
-        - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'
-        - 𝑒
+        - '⟦𝐵1, λ ⤍ 𝑓0, 𝐵2⟧'
+        - 𝑒0
     - n-result: 𝑛2
-      normalize: '𝑛1.𝜏'
+      normalize: '𝑛1.𝜏0'
     - n-result: 𝑛3
       morph: 𝑛2
 
 - name: mphi
   label: \varphi
-  match: ⟦𝐵⟧.𝜏
-  e-match: 𝑒
-  n-result: 𝑛1
+  match: ⟦𝐵0⟧.𝜏0
+  e-match: 𝑒0
+  n-result: 𝑛2
   when:
     and:
       - in:
           - φ
-          - 𝐵
+          - 𝐵0
       - not:
           in:
-            - 𝜏
-            - 𝐵
+            - 𝜏0
+            - 𝐵0
       - not:
           in:
             - λ
-            - 𝐵
+            - 𝐵0
   premises:
-    - n-result: 𝑛
-      normalize: ⟦𝐵⟧.φ.𝜏
     - n-result: 𝑛1
-      morph: 𝑛
+      normalize: ⟦𝐵0⟧.φ.𝜏0
+    - n-result: 𝑛2
+      morph: 𝑛1
 
 - name: md
-  match: '𝑛.𝜏'
-  e-match: 𝑒
+  match: '𝑛0.𝜏0'
+  e-match: 𝑒0
   n-result: 𝑛3
   when:
     not:
-      formation: 𝑛
+      formation: 𝑛0
   premises:
     - n-result: 𝑛1
-      morph: 𝑛
+      morph: 𝑛0
     - n-result: 𝑛2
-      normalize: '𝑛1.𝜏'
+      normalize: '𝑛1.𝜏0'
     - n-result: 𝑛3
       morph: 𝑛2
 
 - name: ma
-  match: '𝑛(𝜏 ↦ 𝑘1)'
-  e-match: 𝑒
+  match: '𝑛0(𝜏0 ↦ 𝑘1)'
+  e-match: 𝑒0
   n-result: 𝑛3
   premises:
     - n-result: 𝑛1
-      morph: 𝑛
+      morph: 𝑛0
     - n-result: 𝑛2
-      normalize: '𝑛1(𝜏 ↦ 𝑘1)'
+      normalize: '𝑛1(𝜏0 ↦ 𝑘1)'
     - n-result: 𝑛3
       morph: 𝑛2
 
 - name: maa
-  match: '𝑛(α𝑖 ↦ 𝑘1)'
-  e-match: 𝑒
+  match: '𝑛0(α𝑖0 ↦ 𝑘1)'
+  e-match: 𝑒0
   n-result: 𝑛3
   premises:
     - n-result: 𝑛1
-      morph: 𝑛
+      morph: 𝑛0
     - n-result: 𝑛2
-      normalize: '𝑛1(α𝑖 ↦ 𝑘1)'
+      normalize: '𝑛1(α𝑖0 ↦ 𝑘1)'
     - n-result: 𝑛3
       morph: 𝑛2
 
 - name: mad
   match: '𝑛(𝜏 ↦ 𝑛1)'
-  e-match: 𝑒
+  e-match: 𝑒0
   n-result: 𝑛2
   when:
     not:
@@ -141,7 +143,7 @@
 
 - name: maad
   match: '𝑛(α𝑖 ↦ 𝑛1)'
-  e-match: 𝑒
+  e-match: 𝑒0
   n-result: 𝑛2
   when:
     not:
@@ -153,36 +155,36 @@
 - name: universe
   label: \Phi
   match: Φ
-  e-match: 𝑒
-  n-result: 𝑛1
+  e-match: 𝑒0
+  n-result: 𝑛2
   when:
     not:
       eq:
-        - 𝑒
+        - 𝑒0
         - Φ
   premises:
-    - n-result: 𝑛
-      normalize: 𝑒
     - n-result: 𝑛1
-      morph: 𝑛
+      normalize: 𝑒0
+    - n-result: 𝑛2
+      morph: 𝑛1
 
 - name: dead
   match: ⊥
-  e-match: 𝑒
+  e-match: 𝑒0
   n-result: ⊥
 
 - name: xi
   match: ξ
-  e-match: 𝑒
-  n-result: 𝑛
+  e-match: 𝑒0
+  n-result: 𝑛1
   premises:
-    - n-result: 𝑛
+    - n-result: 𝑛1
       morph: ⊥
 
 - name: mg
   match: Φ
   e-match: Φ
-  n-result: 𝑛
+  n-result: 𝑛1
   premises:
-    - n-result: 𝑛
+    - n-result: 𝑛1
       morph: ⊥
diff --git a/resources/normalize/alpha.yaml b/resources/normalize/alpha.yaml
--- a/resources/normalize/alpha.yaml
+++ b/resources/normalize/alpha.yaml
@@ -2,9 +2,9 @@
 # SPDX-License-Identifier: MIT
 ---
 name: alpha
-pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧(α𝑖 ↦ 𝑒)
-result: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧(𝜏 ↦ 𝑒)
+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(α𝑖1 ↦ 𝑒1)
+result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒1)
 when:
   eq:
-    - 𝑖
+    - 𝑖1
     - domain: 𝐵1
diff --git a/resources/normalize/amiss.yaml b/resources/normalize/amiss.yaml
--- a/resources/normalize/amiss.yaml
+++ b/resources/normalize/amiss.yaml
@@ -2,10 +2,10 @@
 # SPDX-License-Identifier: MIT
 ---
 name: amiss
-pattern: ⟦𝐵⟧(α𝑖 ↦ 𝑒)
+pattern: ⟦𝐵1⟧(α𝑖1 ↦ 𝑒)
 result: ⊥
 when:
   not:
     gt:
-      - domain: 𝐵
-      - 𝑖
+      - domain: 𝐵1
+      - 𝑖1
diff --git a/resources/normalize/copy.yaml b/resources/normalize/copy.yaml
--- a/resources/normalize/copy.yaml
+++ b/resources/normalize/copy.yaml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: MIT
 ---
 name: copy
-pattern: ⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑘)
-result: ⟦ 𝐵1, 𝜏 ↦ 𝑘, 𝐵2 ⟧
+pattern: ⟦ 𝐵1, 𝜏1 ↦ ∅, 𝐵2 ⟧(𝜏1 ↦ 𝑘1)
+result: ⟦ 𝐵1, 𝜏1 ↦ 𝑘1, 𝐵2 ⟧
diff --git a/resources/normalize/dot.yaml b/resources/normalize/dot.yaml
--- a/resources/normalize/dot.yaml
+++ b/resources/normalize/dot.yaml
@@ -1,21 +1,21 @@
 # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 # SPDX-License-Identifier: MIT
 ---
-# Dispatch 𝜏 on a formation: contextualize the dispatched body 𝑛 and decorate
+# Dispatch 𝜏1 on a formation: contextualize the dispatched body 𝑛1 and decorate
 # it with the whole formation as ρ. The contextualization context is the
-# formation WITHOUT the dispatched binding — ⟦𝐵1, 𝐵2⟧, not ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧ —
-# so a self-referential ξ inside 𝑛 (as in ⟦ a ↦ ξ ⟧.a or ⟦ a ↦ ξ.a ⟧.a) no
-# longer sees 𝜏. Such a self-reference then dispatches on a formation that
-# lacks 𝜏 and collapses to ⊥ via stop/null/dd instead of rebuilding the same
-# ⟦…, 𝜏 ↦ 𝑛, …⟧.𝜏 term and looping forever. ρ on line 'result' still binds the
-# full formation, so sibling and φ-decoration references stay intact — only the
-# self-ξ path narrows, keeping normalization (near-)total.
+# formation WITHOUT the dispatched binding — ⟦𝐵1, 𝐵2⟧, not ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧ —
+# so a self-referential ξ inside 𝑛1 (as in ⟦ a ↦ ξ ⟧.a or ⟦ a ↦ ξ.a ⟧.a) no
+# longer sees 𝜏1. Such a self-reference then dispatches on a formation that
+# lacks 𝜏1 and collapses to ⊥ via stop/null/dd instead of rebuilding the same
+# ⟦…, 𝜏1 ↦ 𝑛1, …⟧.𝜏1 term and looping forever. ρ on line 'result' still binds
+# the full formation, so sibling and φ-decoration references stay intact — only
+# the self-ξ path narrows, keeping normalization (near-)total.
 name: dot
-pattern: ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧.𝜏
-result: 𝑒(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑛, 𝐵2⟧)
+pattern: ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧.𝜏1
+result: 𝑒1(ρ ↦ ⟦𝐵1, 𝜏1 ↦ 𝑛1, 𝐵2⟧)
 where:
-  - meta: 𝑒
+  - meta: 𝑒1
     function: contextualize
     args:
-      - 𝑛
+      - 𝑛1
       - ⟦𝐵1, 𝐵2⟧
diff --git a/resources/normalize/miss.yaml b/resources/normalize/miss.yaml
--- a/resources/normalize/miss.yaml
+++ b/resources/normalize/miss.yaml
@@ -2,10 +2,10 @@
 # SPDX-License-Identifier: MIT
 ---
 name: miss
-pattern: ⟦𝐵⟧(𝜏 ↦ 𝑒)
+pattern: ⟦𝐵1⟧(𝜏1 ↦ 𝑒)
 result: ⊥
 when:
   not:
     in:
-      - 𝜏
-      - 𝐵
+      - 𝜏1
+      - 𝐵1
diff --git a/resources/normalize/null.yaml b/resources/normalize/null.yaml
--- a/resources/normalize/null.yaml
+++ b/resources/normalize/null.yaml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: MIT
 ---
 name: 'null'
-pattern: ⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏
+pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧.𝜏1
 result: ⊥
diff --git a/resources/normalize/over.yaml b/resources/normalize/over.yaml
--- a/resources/normalize/over.yaml
+++ b/resources/normalize/over.yaml
@@ -2,10 +2,10 @@
 # SPDX-License-Identifier: MIT
 ---
 name: over
-pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)
+pattern: ⟦𝐵1, 𝜏1 ↦ 𝑒1, 𝐵2⟧(𝜏1 ↦ 𝑒2)
 result: ⊥
 when:
   not:
     eq:
-      - 𝜏
+      - 𝜏1
       - ρ
diff --git a/resources/normalize/overa.yaml b/resources/normalize/overa.yaml
--- a/resources/normalize/overa.yaml
+++ b/resources/normalize/overa.yaml
@@ -2,14 +2,14 @@
 # SPDX-License-Identifier: MIT
 ---
 name: overa
-pattern: ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(α𝑖 ↦ 𝑒2)
+pattern: ⟦𝐵1, 𝜏1 ↦ 𝑒1, 𝐵2⟧(α𝑖1 ↦ 𝑒2)
 result: ⊥
 when:
   and:
     - eq:
-        - 𝑖
+        - 𝑖1
         - domain: 𝐵1
     - not:
         eq:
-          - 𝜏
+          - 𝜏1
           - ρ
diff --git a/resources/normalize/stop.yaml b/resources/normalize/stop.yaml
--- a/resources/normalize/stop.yaml
+++ b/resources/normalize/stop.yaml
@@ -2,19 +2,19 @@
 # SPDX-License-Identifier: MIT
 ---
 name: stop
-pattern: ⟦𝐵⟧.𝜏
+pattern: ⟦𝐵1⟧.𝜏1
 result: ⊥
 when:
   and:
     - not:
         in:
-          - 𝜏
-          - 𝐵
+          - 𝜏1
+          - 𝐵1
     - not:
         in:
           - φ
-          - 𝐵
+          - 𝐵1
     - not:
         in:
           - λ
-          - 𝐵
+          - 𝐵1
diff --git a/src/AST.hs b/src/AST.hs
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -16,6 +16,14 @@
 import qualified Data.Text as T
 import GHC.Generics (Generic)
 
+-- An anonymous meta-variable, written bare — 𝜏, 𝐵, 𝑒, 𝑛, 𝑘, δ, 𝑓 or 𝑖 with
+-- no index after it. It matches whatever term stands in its place and no rule
+-- can name it afterwards, so it is known only by the kind it was written as
+-- ('t', 'B', 'e', 'n', 'k', 'd', 'F', 'i') and by the offset it was written
+-- at, which tells it apart from every other anonymous meta of the same term.
+data Slot = Slot Text Int
+  deriving (Eq, Ord, Show)
+
 data Expression
   = ExFormation [Binding]
   | ExXi
@@ -24,6 +32,7 @@
   | ExApplication Expression Argument
   | ExDispatch Expression Attribute
   | ExMeta Text
+  | ExAny Slot
   | ExPhiMeet (Maybe String) Int Expression
   | ExPhiAgain (Maybe String) Int Expression
   | {- | Bare data 𝛿 — the raw bytes extracted by the 'delta' dataization rule.
@@ -43,6 +52,7 @@
 data Alpha
   = Alpha Int
   | AlMeta Text
+  | AlAny Slot
   deriving (Eq, Ord, Generic)
 
 data Binding
@@ -51,6 +61,7 @@
   | BiDelta Bytes
   | BiLambda Function
   | BiMeta Text
+  | BiAny Slot
   deriving (Eq, Ord, Show, Generic)
 
 data Bytes
@@ -58,6 +69,7 @@
   | BtOne String
   | BtMany [String]
   | BtMeta Text
+  | BtAny Slot
   deriving (Eq, Ord, Show, Generic)
 
 data Attribute
@@ -67,11 +79,13 @@
   | AtLambda
   | AtDelta
   | AtMeta Text
+  | AtAny Slot
   deriving (Eq, Generic, Ord)
 
 data Function
   = Function Text
   | FnMeta Text
+  | FnAny Slot
   deriving (Eq, Generic, Show, Ord)
 
 instance Show Attribute where
@@ -81,10 +95,12 @@
   show AtDelta = "Δ"
   show AtLambda = "λ"
   show (AtMeta meta) = '!' : T.unpack meta
+  show (AtAny (Slot kind _)) = '!' : T.unpack kind
 
 instance Show Alpha where
   show (Alpha idx) = 'α' : show idx
   show (AlMeta meta) = 'α' : '!' : T.unpack meta
+  show (AlAny (Slot kind _)) = 'α' : '!' : T.unpack kind
 
 -- A cheap, fixed-size digest of an expression, used for fast (dirty) equality
 -- checks during loop detection. Equal expressions always produce the same
@@ -103,6 +119,8 @@
     hashText = T.foldl' (\h c -> step h (fromEnum c))
     hashString :: Int -> String -> Int
     hashString = foldl' (\h c -> step h (fromEnum c))
+    goSlot :: Int -> Slot -> Int
+    goSlot h (Slot kind idx) = step (hashText h kind) idx
     hashMaybeString :: Int -> Maybe String -> Int
     hashMaybeString h Nothing = step h 0
     hashMaybeString h (Just s) = hashString (step h 1) s
@@ -115,6 +133,7 @@
       ExApplication ex arg -> goArgument (goExpr (step h 5) ex) arg
       ExDispatch ex at -> goAttribute (goExpr (step h 6) ex) at
       ExMeta t -> hashText (step h 7) t
+      ExAny slot -> goSlot (step h 32) slot
       ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex
       ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex
       ExBytes bts -> goBytes (step h 8) bts
@@ -125,12 +144,14 @@
       BiVoid at -> goAttribute (step h 13) at
       BiLambda fn -> goFunction (step h 14) fn
       BiMeta t -> hashText (step h 15) t
+      BiAny slot -> goSlot (step h 33) slot
     goBytes :: Int -> Bytes -> Int
     goBytes h = \case
       BtEmpty -> step h 17
       BtOne s -> hashString (step h 18) s
       BtMany ss -> foldl' hashString (step h 19) ss
       BtMeta t -> hashText (step h 20) t
+      BtAny slot -> goSlot (step h 34) slot
     goAttribute :: Int -> Attribute -> Int
     goAttribute h = \case
       AtLabel t -> hashText (step h 21) t
@@ -139,6 +160,7 @@
       AtLambda -> step h 25
       AtDelta -> step h 26
       AtMeta t -> hashText (step h 27) t
+      AtAny slot -> goSlot (step h 35) slot
     goArgument :: Int -> Argument -> Int
     goArgument h = \case
       ArTau at ex -> goExpr (goAttribute (step h 22) at) ex
@@ -147,10 +169,12 @@
     goAlpha h = \case
       Alpha idx -> step (step h 31) idx
       AlMeta t -> hashText (step h 28) t
+      AlAny slot -> goSlot (step h 36) slot
     goFunction :: Int -> Function -> Int
     goFunction h = \case
       Function t -> hashText (step h 16) t
       FnMeta t -> hashText (step h 29) t
+      FnAny slot -> goSlot (step h 37) slot
 
 countNodes :: Expression -> Int
 countNodes (ExFormation bds) = 1 + sum (map nodesInBinding bds) + length bds
@@ -158,6 +182,7 @@
     nodesInBinding :: Binding -> Int
     nodesInBinding (BiTau _ expr) = countNodes expr + 2
     nodesInBinding (BiMeta _) = 1
+    nodesInBinding (BiAny _) = 1
     nodesInBinding _ = 3
 countNodes (ExApplication expr (ArTau _ expr')) = 4 + countNodes expr + countNodes expr'
 countNodes (ExApplication expr (ArAlpha _ expr')) = 4 + countNodes expr + countNodes expr'
diff --git a/src/Atoms.hs b/src/Atoms.hs
new file mode 100644
--- /dev/null
+++ b/src/Atoms.hs
@@ -0,0 +1,261 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+-- Which λ functions exist is a property of the object model being dataized,
+-- not of the calculus. phino therefore implements none of them: it reads a
+-- registry of them from a JSON file given with '--atoms' and fires each one as
+-- a POSIX process. The registry maps a λ name to the runtime that runs it and
+-- the script it runs:
+--
+-- > {
+-- >   "L_bytes_eq": {
+-- >     "rt": "node",
+-- >     "script": "const fs = require('fs'); ..."
+-- >   }
+-- > }
+--
+-- A name absent from the registry has no λ function at all: 𝔼 gets stuck on
+-- it, exactly as it does for a name no one ever declared (see 'Stuck' in
+-- 'Dataize').
+module Atoms
+  ( Atom (..)
+  , AtomException (..)
+  , Registry
+  , Runtime (..)
+  , emptyRegistry
+  , fireAtom
+  , readRegistry
+  , registeredAtom
+  , runtimeNames
+  )
+where
+
+import AST
+import Control.Exception (Exception, bracket, catch, throwIO)
+import Control.Monad (unless)
+import Data.Aeson (FromJSON (parseJSON), eitherDecodeStrict', object, withObject, withText, (.:), (.=))
+import qualified Data.Aeson as A
+import qualified Data.ByteString as BS
+import qualified Data.ByteString.Lazy as BSL
+import Data.List (find, intercalate)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import qualified Data.Text as T
+import Data.Text.Encoding (decodeUtf8Lenient, encodeUtf8)
+import Encoding (Encoding (UNICODE))
+import Lining (LineFormat (SINGLELINE))
+import Logger (logDebug)
+import Margin (defaultMargin)
+import Parser (parseExpression)
+import Printer (printExpression')
+import Sugar (SugarType (SALTY))
+import System.Directory (getTemporaryDirectory, removePathForcibly)
+import System.Exit (ExitCode (ExitFailure, ExitSuccess))
+import System.IO (Handle, IOMode (WriteMode), hClose, hSetBinaryMode, openBinaryTempFile, withBinaryFile)
+import System.Process (CreateProcess (std_err, std_in, std_out), ProcessHandle, StdStream (CreatePipe, UseHandle), createProcess, proc, waitForProcess)
+import Text.Printf (printf)
+
+-- The interpreter a script is run under, named after the executable itself:
+-- only 'node' for now. A registry naming any other runtime is rejected when it
+-- is read, before dataization starts, so a run never gets half-way through a
+-- program to discover that one of its atoms cannot be run at all.
+data Runtime = RtNode
+  deriving stock (Eq, Show)
+
+-- One entry of the registry: the runtime and the source of the script.
+data Atom = Atom
+  { _runtime :: Runtime
+  , _script :: T.Text
+  }
+  deriving stock (Eq, Show)
+
+-- Every λ function phino may fire, keyed by name.
+type Registry = Map T.Text Atom
+
+data AtomException
+  = -- The '--atoms' file is not a JSON registry of λ functions.
+    BrokenRegistry FilePath String
+  | -- The interpreter of a runtime is not installed, so no script of it can run.
+    NoRuntime T.Text String String
+  | -- The script exited with a non-zero status; the message carries its stderr.
+    AtomBroke T.Text Int String
+  | -- The script exited successfully but said nothing phino can use: its stdout
+    -- is not a JSON object, carries no 'n' field, or the 𝜑-expression under it
+    -- does not parse.
+    AtomMute T.Text String String
+  deriving anyclass (Exception)
+
+instance Show AtomException where
+  show (BrokenRegistry file failure) = printf "The registry of atoms '%s' cannot be read: %s" file failure
+  show (NoRuntime func runner failure) =
+    printf "Atom '%s' cannot be fired, '%s' is not runnable: %s" (T.unpack func) runner failure
+  show (AtomBroke func status complaint) =
+    printf "Atom '%s' failed with exit code %d: %s" (T.unpack func) status complaint
+  show (AtomMute func answer failure) =
+    printf "Atom '%s' returned '%s', which phino cannot use: %s" (T.unpack func) answer failure
+
+-- The name a registry spells a runtime with.
+runtimeName :: Runtime -> String
+runtimeName RtNode = "node"
+
+-- The POSIX executable the scripts of a runtime are run under.
+interpreter :: Runtime -> String
+interpreter RtNode = "node"
+
+-- The extension the script of a runtime is written to disk with, so the
+-- interpreter recognizes the file for what it is. This is the language, not the
+-- runtime: 'node' loads a file only if it is named '.js'.
+extension :: Runtime -> String
+extension RtNode = "js"
+
+-- Every runtime phino can run, in the order the '--atoms' help lists them.
+runtimes :: [Runtime]
+runtimes = [RtNode]
+
+runtimeNames :: [String]
+runtimeNames = map runtimeName runtimes
+
+instance FromJSON Runtime where
+  parseJSON = withText "runtime" $ \name -> case find ((== T.unpack name) . runtimeName) runtimes of
+    Just runtime -> pure runtime
+    Nothing -> fail (printf "unknown runtime '%s', expected one of: %s" (T.unpack name) (intercalate ", " runtimeNames))
+
+instance FromJSON Atom where
+  parseJSON = withObject "atom" $ \entry -> Atom <$> entry .: "rt" <*> entry .: "script"
+
+-- What the script writes to stdout: one JSON object whose 'n' field is the
+-- 𝜑-expression the atom answers with.
+newtype Answer = Answer T.Text
+
+instance FromJSON Answer where
+  parseJSON = withObject "answer" $ \answer -> Answer <$> answer .: "n"
+
+-- No λ function at all: every atom gets stuck. This is what a run without
+-- '--atoms' fires against.
+emptyRegistry :: Registry
+emptyRegistry = Map.empty
+
+-- The λ function registered under this name, if any.
+registeredAtom :: Registry -> T.Text -> Maybe Atom
+registeredAtom registry func = Map.lookup func registry
+
+-- Read the registry of λ functions from a JSON file. An unknown runtime, a
+-- missing 'script' or malformed JSON fails here, before any dataization
+-- starts.
+readRegistry :: FilePath -> IO Registry
+readRegistry path = do
+  content <- BS.readFile path `catch` unreadable
+  case eitherDecodeStrict' content of
+    Left failure -> throwIO (BrokenRegistry path failure)
+    Right registry -> do
+      logDebug (printf "Loaded %d atom(s) from '%s'" (Map.size registry) path)
+      pure registry
+  where
+    unreadable :: IOError -> IO BS.ByteString
+    unreadable failure = throwIO (BrokenRegistry path (show failure))
+
+-- Fire the λ function 'func' by running its script as a POSIX process under
+-- the interpreter of its runtime, with the λ name as the first command-line
+-- argument — one script may be registered under several names and branch on
+-- it. The script is fed a JSON object on stdin (see 'payload') and answers
+-- with one on stdout; the 𝜑-expression under 'n' becomes the atom's raw
+-- result, which 𝔼 normalizes exactly as it normalized the answer of a built-in
+-- one. A non-zero exit, unparsable output or a missing 'n' fails the run.
+fireAtom :: T.Text -> Atom -> Expression -> Expression -> IO Expression
+fireAtom func Atom{..} form univ =
+  withTemp (printf "phino-atom-.%s" (extension _runtime)) (encodeUtf8 _script) $ \script ->
+    withTemp "phino-atom-.err" "" $ \errors -> do
+      logDebug (printf "Firing atom '%s' as '%s %s %s'" (T.unpack func) (interpreter _runtime) script (T.unpack func))
+      (status, answer) <- executed script errors
+      complaint <- readErrors errors
+      unless (null complaint) (logDebug (printf "Atom '%s' wrote to stderr: %s" (T.unpack func) complaint))
+      case status of
+        ExitFailure code -> throwIO (AtomBroke func code complaint)
+        ExitSuccess -> answered answer
+  where
+    -- Run the interpreter with its input and its output on pipes and its
+    -- complaints in a file. The input is written and closed before the output is
+    -- read, so the parent never has two streams to drain at once — which would
+    -- need threads to be safe — and the script's own stderr, which may be
+    -- anything at all, cannot fill a pipe nobody is reading. Every stream is
+    -- bytes: a 𝜑 expression carries characters no single-byte locale can spell,
+    -- so nothing is left to the locale.
+    executed :: FilePath -> FilePath -> IO (ExitCode, BS.ByteString)
+    executed script errors =
+      withBinaryFile errors WriteMode $ \stderr' -> do
+        (stdin', stdout', process) <- spawned script stderr'
+        hSetBinaryMode stdin' True
+        hSetBinaryMode stdout' True
+        -- A script that dies before reading its input leaves this write with
+        -- nobody to drain it. The failure worth reporting is the one the script
+        -- made, so a broken pipe is swallowed here and the exit status decides.
+        BS.hPut stdin' (payload form univ) `catch` unheard
+        hClose stdin' `catch` unheard
+        answer <- BS.hGetContents stdout'
+        status <- waitForProcess process
+        pure (status, answer)
+    spawned :: FilePath -> Handle -> IO (Handle, Handle, ProcessHandle)
+    spawned script stderr' = do
+      spawn <- createProcess started `catch` missing
+      case spawn of
+        (Just stdin', Just stdout', _, process) -> pure (stdin', stdout', process)
+        _ -> throwIO (AtomMute func "" "the interpreter gave phino no streams to talk over")
+      where
+        started :: CreateProcess
+        started =
+          (proc (interpreter _runtime) [script, T.unpack func])
+            { std_in = CreatePipe
+            , std_out = CreatePipe
+            , std_err = UseHandle stderr'
+            }
+    missing :: IOError -> IO a
+    missing failure = throwIO (NoRuntime func (interpreter _runtime) (show failure))
+    unheard :: IOError -> IO ()
+    unheard _ = pure ()
+    -- Whatever the script complained about, decoded leniently: the stream is
+    -- the script's, so it may hold anything at all.
+    readErrors :: FilePath -> IO String
+    readErrors errors = T.unpack . T.strip . decodeUtf8Lenient <$> BS.readFile errors
+    -- Parse what the script said: a JSON object with the raw 𝜑-expression
+    -- under 'n'.
+    answered :: BS.ByteString -> IO Expression
+    answered answer = case eitherDecodeStrict' answer of
+      Left failure -> throwIO (AtomMute func spoken failure)
+      Right (Answer raw) -> case parseExpression (T.unpack raw) of
+        Left failure -> throwIO (AtomMute func (T.unpack raw) failure)
+        Right expr -> pure expr
+      where
+        spoken :: String
+        spoken = T.unpack (T.strip (decodeUtf8Lenient answer))
+
+-- The JSON phino feeds a script on stdin: the formation being evaluated under
+-- 'b', with its λ binding removed so the script may dispatch on it, and the
+-- universe Φ under 's'. Both are rendered as canonical 𝜑-calculus on a single
+-- line — no syntax sugar, whatever '--sweet' says about the output of the run —
+-- so a script never has to know phino's sugar to find a datum: every byte array
+-- it may need is spelled out as a Δ binding. The text is what phino's own parser
+-- reads back, so a script may hand any part of it to another phino run (see the
+-- '--inside' option).
+payload :: Expression -> Expression -> BS.ByteString
+payload form univ = BSL.toStrict (A.encode (object ["b" .= rendered form, "s" .= rendered univ]))
+  where
+    rendered :: Expression -> T.Text
+    rendered expr = T.pack (printExpression' expr (SALTY, UNICODE, SINGLELINE, defaultMargin))
+
+-- Write the content to a fresh temporary file, hand its path to the action and
+-- delete the file afterwards, whatever the action does.
+withTemp :: String -> BS.ByteString -> (FilePath -> IO a) -> IO a
+withTemp template content action = do
+  dir <- getTemporaryDirectory
+  bracket (openBinaryTempFile dir template) discarded $ \(path, handle) -> do
+    BS.hPut handle content
+    hClose handle
+    action path
+  where
+    discarded :: (FilePath, Handle) -> IO ()
+    discarded (path, handle) = hClose handle >> removePathForcibly path
diff --git a/src/Builder.hs b/src/Builder.hs
--- a/src/Builder.hs
+++ b/src/Builder.hs
@@ -42,6 +42,11 @@
 metaMsg :: Text -> String
 metaMsg = printf "meta '%s' is either does not exist or refers to an inappropriate term" . T.unpack
 
+-- An anonymous meta is bound only within the very pattern that matched it, so
+-- a lookup that misses means the term being built is not that pattern
+slotMsg :: Slot -> String
+slotMsg (Slot kind _) = printf "anonymous meta '!%s' cannot be referenced" (T.unpack kind)
+
 type Built a = Either String a
 
 instance Show BuildException where
@@ -64,21 +69,30 @@
 contextualize ex _ = ex
 
 buildAttribute :: Attribute -> Subst -> Built Attribute
-buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup meta mp of
+buildAttribute (AtMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of
   Just (MvAttribute attr) -> Right attr
   _ -> Left (metaMsg meta)
+buildAttribute (AtAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of
+  Just (MvAttribute attr) -> Right attr
+  _ -> Left (slotMsg slot)
 buildAttribute attr _ = Right attr
 
 buildAlpha :: Alpha -> Subst -> Built Alpha
-buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup meta mp of
+buildAlpha (AlMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of
   Just (MvIndex idx) -> Right (Alpha idx)
   _ -> Left (metaMsg meta)
+buildAlpha (AlAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of
+  Just (MvIndex idx) -> Right (Alpha idx)
+  _ -> Left (slotMsg slot)
 buildAlpha a _ = Right a
 
 buildBytes :: Bytes -> Subst -> Built Bytes
-buildBytes (BtMeta meta) (Subst mp) = case Map.lookup meta mp of
+buildBytes (BtMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of
   Just (MvBytes bytes) -> Right bytes
   _ -> Left (metaMsg meta)
+buildBytes (BtAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of
+  Just (MvBytes bytes) -> Right bytes
+  _ -> Left (slotMsg slot)
 buildBytes bts _ = Right bts
 
 -- Build binding
@@ -92,15 +106,21 @@
 buildBinding (BiVoid attr) subst = do
   attribute <- buildAttribute attr subst
   Right [BiVoid attribute]
-buildBinding (BiMeta meta) (Subst mp) = case Map.lookup meta mp of
+buildBinding (BiMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of
   Just (MvBindings bds) -> uniqueBindings bds
   _ -> Left (metaMsg meta)
+buildBinding (BiAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of
+  Just (MvBindings bds) -> uniqueBindings bds
+  _ -> Left (slotMsg slot)
 buildBinding (BiDelta bytes) subst = do
   bts <- buildBytes bytes subst
   Right [BiDelta bts]
-buildBinding (BiLambda (FnMeta meta)) (Subst mp) = case Map.lookup meta mp of
+buildBinding (BiLambda (FnMeta meta)) (Subst mp) = case Map.lookup (Named meta) mp of
   Just (MvFunction func) -> Right [BiLambda (Function func)]
   _ -> Left (metaMsg meta)
+buildBinding (BiLambda (FnAny slot)) (Subst mp) = case Map.lookup (Anon slot) mp of
+  Just (MvFunction func) -> Right [BiLambda (Function func)]
+  _ -> Left (slotMsg slot)
 buildBinding binding _ = Right [binding]
 
 buildArgument :: Argument -> Subst -> Built Argument
@@ -121,6 +141,12 @@
   bds <- buildBindings rest subst
   Right (first ++ bds)
 
+-- The bindings of a formation a meta was bound to are checked once more here,
+-- since a substitution may bring two of them together under one attribute.
+unique :: Expression -> Built Expression
+unique (ExFormation bds) = uniqueBindings bds >> Right (ExFormation bds)
+unique expr = Right expr
+
 -- Build meta expression with given substitution
 buildExpression :: Expression -> Subst -> Built Expression
 buildExpression (ExDispatch ex at) subst = do
@@ -134,12 +160,12 @@
 buildExpression (ExFormation bds) subst = do
   bds' <- buildBindings bds subst >>= uniqueBindings
   Right (ExFormation bds')
-buildExpression (ExMeta meta) (Subst mp) = case Map.lookup meta mp of
-  Just (MvExpression expr) ->
-    case expr of
-      ExFormation bds -> uniqueBindings bds >> Right expr
-      _ -> Right expr
+buildExpression (ExMeta meta) (Subst mp) = case Map.lookup (Named meta) mp of
+  Just (MvExpression expr) -> unique expr
   _ -> Left (metaMsg meta)
+buildExpression (ExAny slot) (Subst mp) = case Map.lookup (Anon slot) mp of
+  Just (MvExpression expr) -> unique expr
+  _ -> Left (slotMsg slot)
 buildExpression expr _ = Right expr
 
 buildBytesThrows :: Bytes -> Subst -> IO Bytes
diff --git a/src/Bytes.hs b/src/Bytes.hs
--- a/src/Bytes.hs
+++ b/src/Bytes.hs
@@ -60,6 +60,7 @@
 btsToWord8 (BtOne bt) = [hexByte bt]
 btsToWord8 (BtMany bts) = map hexByte bts
 btsToWord8 (BtMeta mt) = error $ "Cannot convert meta bytes to Word8; " ++ T.unpack mt
+btsToWord8 (BtAny _) = error "Cannot convert anonymous meta bytes to Word8"
 
 hexByte :: String -> Word8
 hexByte [hi, lo] = (nibble hi `shiftL` 4) .|. nibble lo
@@ -185,6 +186,7 @@
 -- Nothing
 btsToNonFinite :: Bytes -> Maybe NonFinite
 btsToNonFinite (BtMeta _) = Nothing
+btsToNonFinite (BtAny _) = Nothing
 btsToNonFinite bts = find (btsEqual bts . nonFiniteBts) nonFinites
 
 -- The non-finite double the given name stands for, if it names one at all
diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs
--- a/src/CLI/Helpers.hs
+++ b/src/CLI/Helpers.hs
@@ -7,6 +7,7 @@
 module CLI.Helpers where
 
 import AST
+import Atoms (Registry, emptyRegistry, readRegistry)
 import CLI.Types
 import CLI.Validators (invalidCLIArguments)
 import Canonizer (canonize)
@@ -16,6 +17,7 @@
 import Data.IORef
 import Data.List (intercalate, nub)
 import Data.Maybe
+import Dataize (DataizeContext, insideUniverse)
 import Deps (SaveEvalFunc, SaveStepFunc, dontSaveEval, saveEval, saveStep)
 import Encoding
 import Files (ensuredFile)
@@ -83,6 +85,34 @@
       protocol <- openFile file WriteMode
       hSetEncoding protocol utf8
       pure protocol
+
+-- The λ functions this run may fire. phino implements none of them, so without
+-- '--atoms' the registry is empty and every atom a program names gets stuck —
+-- which is exactly what '--partial' parks on. The file is read here, before
+-- anything is parsed or dataized, so an unknown runtime or a malformed registry
+-- fails the run up front rather than half-way through a derivation.
+registryOf :: Maybe FilePath -> IO Registry
+registryOf Nothing = do
+  logDebug "The option '--atoms' is not specified, no λ function can be fired"
+  pure emptyRegistry
+registryOf (Just file) = do
+  logDebug (printf "The option '--atoms' is specified, reading the λ functions from '%s'" file)
+  ensuredFile file >>= readRegistry
+
+-- Aim the run at the '--inside' expression instead of at '--locator': the
+-- expression is bound to a synthetic attribute prepended to the input
+-- expression, which the run takes as the universe, and the locator becomes that
+-- attribute (see 'insideUniverse'). Without the option nothing moves and the
+-- context is handed back as it came.
+aimed :: Maybe String -> Expression -> DataizeContext -> IO (Expression, DataizeContext)
+aimed Nothing expr ctx = pure (expr, ctx)
+aimed (Just src) expr@(ExFormation _) ctx = do
+  target <- parseExpressionThrows src
+  logDebug (printf "The option '--inside' is specified, reducing '%s' inside the given universe" (P.printExpression target))
+  insideUniverse target expr ctx
+aimed (Just _) expr _ =
+  invalidCLIArguments
+    (printf "The option --inside requires the input expression to be a formation, but given: %s" (P.printExpression expr))
 
 -- Read input from file or stdin
 readInput :: Maybe FilePath -> IO String
diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs
--- a/src/CLI/Parsers.hs
+++ b/src/CLI/Parsers.hs
@@ -3,6 +3,7 @@
 
 module CLI.Parsers where
 
+import Atoms (runtimeNames)
 import CLI.Types
 import Data.Char (toLower, toUpper)
 import Data.List (intercalate)
@@ -203,8 +204,42 @@
 optStepsDir = optional (strOption (long "steps-dir" <> metavar "FILE" <> help "Directory to save intermediate steps during rewriting/dataizing"))
 
 optPartial :: Parser Bool
-optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on an atom that cannot fire (its λ function is unknown, or an input of it reaches such an atom), leave it in place and print the residual 𝜑-program")
+optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on an atom that cannot fire (its λ function is not in the --atoms registry), leave it in place and print the residual 𝜑-program")
 
+-- Which λ functions this run may fire. phino implements none of them itself
+-- (see 'Atoms'), so without this option every atom a program names gets stuck.
+optAtoms :: Parser (Maybe FilePath)
+optAtoms =
+  optional
+    ( strOption
+        ( long "atoms"
+            <> metavar "FILE"
+            <> help
+              ( printf
+                  "Path to the JSON registry of λ functions this run may fire, mapping each name to the runtime that runs it (%s) and the script it runs"
+                  (intercalate ", " runtimeNames)
+              )
+        )
+    )
+
+-- The external face of the trick phino plays internally to reduce a
+-- sub-expression against a universe: prepend a synthetic binding holding it to
+-- that universe and aim the locator at the binding. An atom script needs it to
+-- reduce the parts of the formation it was given, so it does not have to splice
+-- them into the text of the universe by hand.
+optInside :: Parser (Maybe String)
+optInside =
+  optional
+    ( strOption
+        ( long "inside"
+            <> metavar "EXPRESSION"
+            <> help
+              "The 𝜑-expression to dataize or morph inside the input expression, which is taken as the universe \
+              \Φ: a synthetic binding holding it is prepended to the universe and the locator is aimed at that \
+              \binding. Cannot be used together with --locator"
+        )
+    )
+
 optEvaluations :: Parser (Maybe FilePath)
 optEvaluations = optional (strOption (long "evaluations" <> metavar "FILE" <> help "File to record every atom fired during dataizing, as one tab-separated line per firing: the λ function name, its argument formation and its result (requires --output=phi)"))
 
@@ -312,8 +347,10 @@
             <*> optExpression
             <*> optLabel
             <*> optMeetPrefix
+            <*> optInside
             <*> optStepsDir
             <*> optEvaluations
+            <*> optAtoms
             <*> argInputFile
         )
 
@@ -353,8 +390,10 @@
             <*> optExpression
             <*> optLabel
             <*> optMeetPrefix
+            <*> optInside
             <*> optStepsDir
             <*> optEvaluations
+            <*> optAtoms
             <*> argInputFile
         )
 
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -14,9 +14,11 @@
 import Condition (parseConditionThrows)
 import Control.Exception
 import Control.Monad (unless, when)
+import Data.Foldable (traverse_)
 import Data.List (intercalate)
 import qualified Data.List.NonEmpty as NE
 import Data.Maybe (fromJust, isJust, isNothing)
+import qualified Data.Text as T
 import Dataize
 import Encoding
 import qualified Filter as F
@@ -30,6 +32,7 @@
 import qualified Random as R
 import Rewriter
 import Rule (RuleContext (..), matchExpressionWithRule)
+import Slots (anonymous)
 import System.Directory (doesFileExist, getModificationTime)
 import System.Exit (exitSuccess)
 import System.Random (mkStdGen, setStdGen)
@@ -142,6 +145,7 @@
 runDataize :: OptsDataize -> IO ()
 runDataize OptsDataize{..} = do
   validateOpts
+  atoms <- registryOf _atoms
   excluded <- validatedDispatches "hide" _hide
   included <- validatedDispatches "show" _show
   [loc] <- validatedDispatches "locator" [_locator]
@@ -156,8 +160,10 @@
       include = (`F.include` included)
   save <- saveStepFunc _stepsDir printCtx
   (outcome, chain) <-
-    withEvalFunc _evaluations printCtx $
-      dataize expr . DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial buildTerm save
+    withEvalFunc _evaluations printCtx $ \record -> do
+      let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record
+      (universe, aiming) <- aimed _inside expr ctx
+      dataize universe aiming
   when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)
   unless _quiet (printOutcome printCtx outcome >>= putStrLn)
   where
@@ -181,6 +187,9 @@
       when
         (isJust _evaluations && _outputFormat /= PHI)
         (invalidCLIArguments "The --evaluations option can stay together with --output=phi only, since one record must fit into one line")
+      when
+        (isJust _inside && _locator /= "Q")
+        (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")
     toPrintCtx :: Expression -> PrintContext
     toPrintCtx focus =
       PrintCtx
@@ -211,6 +220,7 @@
 runMorph :: OptsMorph -> IO ()
 runMorph OptsMorph{..} = do
   validateOpts
+  atoms <- registryOf _atoms
   excluded <- validatedDispatches "hide" _hide
   included <- validatedDispatches "show" _show
   [loc] <- validatedDispatches "locator" [_locator]
@@ -225,8 +235,10 @@
       include = (`F.include` included)
   save <- saveStepFunc _stepsDir printCtx
   (morphed, chain) <-
-    withEvalFunc _evaluations printCtx $
-      morph expr . DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial buildTerm save
+    withEvalFunc _evaluations printCtx $ \record -> do
+      let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record
+      (universe, aiming) <- aimed _inside expr ctx
+      morph universe aiming
   when _sequence (printRewrittens printCtx (exclude $ include chain, False) >>= putStrLn)
   unless _quiet (printFocused printCtx morphed >>= putStrLn)
   where
@@ -242,6 +254,9 @@
       when
         (isJust _evaluations && _outputFormat /= PHI)
         (invalidCLIArguments "The --evaluations option can stay together with --output=phi only, since one record must fit into one line")
+      when
+        (isJust _inside && _locator /= "Q")
+        (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")
     toPrintCtx :: Expression -> PrintContext
     toPrintCtx focus =
       PrintCtx
@@ -333,6 +348,7 @@
     else do
       ptn <- parseExpressionThrows (fromJust _pattern)
       condition <- traverse parseConditionThrows _when
+      traverse_ (throwIO . AnonymousMetaInCondition . T.unpack) (anonymous condition)
       substs <- matchExpressionWithRule expr (rule ptn condition) (RuleContext buildTerm)
       if null substs
         then throwIO EmptySubstsOnMatch
diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs
--- a/src/CLI/Types.hs
+++ b/src/CLI/Types.hs
@@ -41,6 +41,7 @@
   | CouldNotDataize
   | CouldNotPrintExpressionInXMIR
   | EmptySubstsOnMatch
+  | AnonymousMetaInCondition String
   | VersionMismatch String String
   deriving (Exception)
 
@@ -50,6 +51,8 @@
   show CouldNotDataize = "Could not dataize given expression"
   show CouldNotPrintExpressionInXMIR = "Could not print expression with --output=xmir, only expression printing is allowed"
   show EmptySubstsOnMatch = "Provided pattern was not matched, no substitutions are built"
+  show (AnonymousMetaInCondition kind) =
+    printf "Anonymous meta '!%s' cannot be referenced in --when, only a named one can" kind
   show (VersionMismatch expected actual) =
     printf "Version mismatch: --pin requires '%s', but this is phino %s" expected actual
 
@@ -107,8 +110,10 @@
   , _expression :: Maybe String
   , _label :: Maybe String
   , _meetPrefix :: Maybe String
+  , _inside :: Maybe String
   , _stepsDir :: Maybe FilePath
   , _evaluations :: Maybe FilePath
+  , _atoms :: Maybe FilePath
   , _inputFile :: Maybe FilePath
   }
 
@@ -149,8 +154,10 @@
   , _expression :: Maybe String
   , _label :: Maybe String
   , _meetPrefix :: Maybe String
+  , _inside :: Maybe String
   , _stepsDir :: Maybe FilePath
   , _evaluations :: Maybe FilePath
+  , _atoms :: Maybe FilePath
   , _inputFile :: Maybe FilePath
   }
 
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -303,6 +303,11 @@
 metaTail :: T.Text -> T.Text
 metaTail = T.drop 1
 
+-- An anonymous meta renders as the bare sigil it was written with: it carries
+-- no suffix, and needs none, since nothing on the page refers back to it.
+anyMeta :: META_HEAD -> META
+anyMeta hd' = META NO_EXCL hd' T.empty
+
 -- The first character of an expression meta name encodes its kind:
 -- 'n'-prefixed names are normal-form-constrained '𝑛' metas, 'k'-prefixed
 -- names are absolute-constrained '𝑘' metas, everything else is an ordinary
@@ -323,6 +328,7 @@
   toCST ExRoot _ = EX_GLOBAL Φ
   toCST ExXi _ = EX_XI XI
   toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))
+  toCST (ExAny (Slot kind _)) _ = EX_META (anyMeta (exMetaHead kind))
   toCST ExTermination _ = EX_TERMINATION DEAD
   toCST (ExBytes bts) ctx = EX_BYTES (toCST bts ctx)
   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)
@@ -467,11 +473,13 @@
 instance ToCST [Binding] BINDING where
   toCST [] (tabs, _) = BI_EMPTY (TAB tabs)
   toCST (BiMeta mt : bds) ctx@(tabs, _) = BI_META (META NO_EXCL B (metaTail mt)) (toCST bds ctx) (TAB tabs)
+  toCST (BiAny _ : bds) ctx@(tabs, _) = BI_META (anyMeta B) (toCST bds ctx) (TAB tabs)
   toCST (bd : bds) ctx@(tabs, _) = BI_PAIR (toCST bd ctx) (toCST bds ctx) (TAB tabs)
 
 instance ToCST [Binding] BINDINGS where
   toCST [] (tabs, _) = BDS_EMPTY (TAB tabs)
   toCST (BiMeta mt : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (META NO_EXCL B (metaTail mt)) (toCST bds ctx)
+  toCST (BiAny _ : bds) ctx@(tabs, eol) = BDS_META eol (TAB tabs) (anyMeta B) (toCST bds ctx)
   toCST (bd : bds) ctx@(tabs, eol) = BDS_PAIR eol (TAB tabs) (toCST bd ctx) (toCST bds ctx)
 
 instance ToCST Binding PAIR where
@@ -498,7 +506,9 @@
   toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)
   toCST (BiLambda (Function name)) _ = PA_LAMBDA name
   toCST (BiLambda (FnMeta mt)) _ = PA_META_LAMBDA (META NO_EXCL F (metaTail mt))
+  toCST (BiLambda (FnAny _)) _ = PA_META_LAMBDA (anyMeta F)
   toCST (BiMeta mt) _ = error $ "BiMeta binding " ++ T.unpack mt ++ " cannot be converted to PAIR"
+  toCST (BiAny _) _ = error "An anonymous meta binding cannot be converted to PAIR"
 
 instance ToCST Argument PAIR where
   toCST (ArTau attr exp) ctx = toCST (BiTau attr exp) ctx
@@ -521,6 +531,7 @@
   toCST (BtOne byte) _ = BT_ONE byte
   toCST (BtMany bts) _ = BT_MANY bts
   toCST (BtMeta mt) _ = BT_META (META NO_EXCL D (metaTail mt))
+  toCST (BtAny _) _ = BT_META (anyMeta D)
 
 instance ToCST Attribute ATTRIBUTE where
   toCST (AtLabel label) _ = AT_LABEL label
@@ -529,10 +540,12 @@
   toCST AtDelta _ = AT_DELTA DELTA
   toCST AtLambda _ = AT_LAMBDA LAMBDA
   toCST (AtMeta mt) _ = AT_META (META NO_EXCL TAU (metaTail mt))
+  toCST (AtAny _) _ = AT_META (anyMeta TAU)
 
 instance ToCST Alpha ALPHA where
   toCST (Alpha idx) _ = AL_IDX ALPHA idx
   toCST (AlMeta mt) _ = AL_META ALPHA (META NO_EXCL I (metaTail mt))
+  toCST (AlAny _) _ = AL_META ALPHA (anyMeta I)
 
 instance ToCST Y.Condition CONDITION where
   toCST (Y.Not (Y.In attr binding)) _ = CO_BELONGS (attributeToCST attr) NOT_IN (ST_BINDING (bindingsToCST [binding]))
@@ -563,6 +576,7 @@
 
 instance ToCST Y.Number NUMBER where
   toCST (Y.MetaIndex mt) _ = IDX_META (META NO_EXCL I (metaTail mt))
+  toCST (Y.AnyIndex _) _ = IDX_META (anyMeta I)
   toCST (Y.Length binding) _ = LENGTH (bindingsToCST [binding])
   toCST (Y.Domain binding) _ = DOMAIN (bindingsToCST [binding])
   toCST (Y.Literal num) _ = LITERAL num
diff --git a/src/Condition.hs b/src/Condition.hs
--- a/src/Condition.hs
+++ b/src/Condition.hs
@@ -58,7 +58,7 @@
         bd <- _binding phiParser
         _ <- rparen
         return (Y.Domain bd)
-    , Y.MetaIndex <$> _index phiParser
+    , either Y.AnyIndex Y.MetaIndex <$> _index phiParser
     , do
         sign <- optional (choice [char '-', char '+'])
         unsigned <- lexeme L.decimal
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -10,14 +10,13 @@
 -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
 -- SPDX-License-Identifier: MIT
 
-module Dataize (morph, morph', dataize, dataize', DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where
+module Dataize (morph, morph', dataize, dataize', insideUniverse, DataizeContext (..), DataizeException (..), Outcome (..), Steps (..), State, emptyState, execBuildTerm) where
 
 import AST
+import Atoms (Registry, fireAtom, registeredAtom)
 import Builder (buildBytesThrows, buildExpressionThrows)
-import Bytes (btsAnd, btsConcat, btsEqual, btsNot, btsOr, btsShift, btsSize, btsSlice, btsToNum, numToBts, strToBts)
 import Control.Exception (Exception, catch, throwIO, try)
 import Control.Monad (foldM, when)
-import Data.Int (Int32)
 import Data.List (find, partition)
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NE
@@ -25,7 +24,6 @@
 import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..))
 import Locator (locatedExpression, withLocatedExpression)
 import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle)
-import Misc
 import Must (Must (..))
 import Random (shuffle)
 import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)
@@ -76,6 +74,7 @@
   , _depthSensitive :: Bool
   , _shuffle :: Bool
   , _partial :: Bool
+  , _atoms :: Registry
   , _buildTerm :: BuildTermFunc
   , _saveStep :: SaveStepFunc
   , _saveEval :: SaveEvalFunc
@@ -83,9 +82,10 @@
 
 data DataizeException
   = OutOfSteps Int
-  | -- An atom could not fire: 'atom' does not know its λ function, or the
-    -- dataization of one of its inputs met an atom it does not know. The name
-    -- is that of the innermost unknown atom, the one 𝔼 actually failed on.
+  | -- An atom could not fire: the '--atoms' registry carries no λ function of
+    -- that name, so there is nothing to run. The name is that of the atom 𝔼
+    -- actually failed on, which for a chain of dispatches is the innermost one,
+    -- since 'ml' reduces a head before the atom above it fires.
     Stuck T.Text
   | -- A 'Stuck' caught by a frame of the 𝕄/𝔻 spine, together with the
     -- derivation that frame had reached (see 'parking'). The head of the chain
@@ -461,130 +461,43 @@
     rewriteContext DataizeContext{..} =
       RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep
 
--- Synthetic dataize function for internal usage inside atoms. Here we modify the
--- universe by adding a new binding which refers to the expression we want to
--- dataize, building a local working expression to reduce within. As a caller of 𝔻,
--- it first reduces the expression to a normal form, since 𝔻 only accepts normal
--- forms. The universe 'univ' itself is forwarded unchanged, so morphing Φ under
--- this context still resolves to the true universe rather than to this
--- synthetic, binding-prepended formation. The chain is the synthetic one, so a
--- stuck atom met on the way leaves without it (see 'unparked').
-_dataize :: Expression -> Expression -> State -> DataizeContext -> IO (Bytes, State)
-_dataize expr univ state ctx@DataizeContext{_buildTerm = buildTerm} = case univ of
-  ExFormation bds -> unparked $ do
+-- Bind 'expr' to a synthetic attribute of the universe and reduce it to a
+-- normal form there, handing back the extended universe together with the
+-- locator that aims at the binding. This is the trick phino has always played
+-- to reduce a sub-expression that is not part of the program — an atom's
+-- operand, while the atoms still lived in the binary — and it is now the
+-- contract of the '--inside' option, so an atom script asking phino to reduce
+-- a part of the formation it was given does not have to splice it into the text
+-- of the universe by hand. 𝔻 and 𝕄 accept normal forms only and an expression
+-- handed in from outside is not necessarily one (a dispatch off a formation,
+-- '⟦ x ↦ 6, ρ ↦ 5 ⟧.x', is not), so it is normalized against the extended
+-- universe before either judgment sees it. The context comes back aimed at that
+-- binding, so the caller hands the extended universe and the context it got
+-- straight to 'dataize' or 'morph'.
+insideUniverse :: Expression -> Expression -> DataizeContext -> IO (Expression, DataizeContext)
+insideUniverse expr univ ctx@DataizeContext{_buildTerm = buildTerm} = case univ of
+  ExFormation bds -> do
     (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty
-    let synthetic = ExFormation (BiTau attr expr : bds)
-    (normal, seq) <- normalized expr ((synthetic, Nothing) :| []) ctx
-    ((bts, _), state') <- dataize' (normal, seq) univ state ctx
-    pure (bts, state')
-  _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe")
-
--- A number atom only operates on numeric data. Empty bytes — a genuine
--- zero-length byte array ⟦Δ ⤍ --⟧ — carry no number, so the operand is rejected
--- and the atom yields ⊥. So does any byte array whose length is not 8: 'btsToNum'
--- throws on such arrays, so the size is checked up front, exactly like 'asInt'.
-asNumber :: Bytes -> Maybe Double
-asNumber bts
-  | btsSize bts /= 8 = Nothing
-  | otherwise = Just (either toDouble id (btsToNum bts))
-
--- An operand that EO reads as a Java 'int' — a shift distance or a slice bound.
--- 'Expect.at(…).that(Integer)' turns down anything but a whole number inside the
--- 32-bit range, and so does this, leaving the atom with ⊥
-asInt :: Bytes -> Maybe Int
-asInt bts
-  | btsSize bts /= 8 = Nothing
-  | otherwise = case btsToNum bts of
-      Left num | num >= fromIntegral (minBound :: Int32) && num <= fromIntegral (maxBound :: Int32) -> Just num
-      _ -> Nothing
-
--- An atom whose EO signature ends in '/Q.bool' hands back one of the two bool
--- objects of the universe, exactly what 'Data.ToPhi(boolean)' does in the runtime
-boolean :: Bool -> Expression
-boolean True = BaseObject "true"
-boolean False = BaseObject "false"
-
--- Both bitwise atoms take ρ and 'b' and reject operands of different lengths
-bitwise :: (Bytes -> Bytes -> Maybe Bytes) -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)
-bitwise op self univ state ctx = do
-  (b, bstate) <- _dataize (ExDispatch self (AtLabel "b")) univ state ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx
-  pure (maybe ExTermination dataBytes (op rho b), rstate)
+    let aiming = ctx{_locator = ExDispatch ExRoot attr}
+        synthetic = ExFormation (BiTau attr expr : bds)
+    (normal, _) <- normalized expr ((synthetic, Nothing) :| []) aiming
+    pure (ExFormation (BiTau attr normal : bds), aiming)
+  _ -> throwIO (userError "Can't reduce an expression inside a universe which is not a formation")
 
--- The 12 primitive λ-atoms every EO data operation reduces to. phino mirrors
--- EO's set exactly: bytes {and, concat, eq, not, or, right, size, slice} and
--- number {div, gt, plus, times}. There is deliberately no 'L_number_eq': EO's
--- 'number.eq' (eo-runtime/src/main/eo/number/eq.eo) is pure EO — a formation
--- composing 'is-nan', 'or', 'and' and 'L_bytes_eq', with no λ of its own — so
--- nothing is left for a phino atom to implement. Names like 'L_bool_if' or
--- 'L_string_slice' must stay unimplemented too: the EO lowering declares them
--- precisely so that '--partial' parks on them and renders the call to Java.
+-- phino implements no λ function of its own. Which atoms exist is a property of
+-- the object model being dataized, not of the calculus, so they come from the
+-- '--atoms' registry and run as external scripts (see 'Atoms'). A name the
+-- registry does not carry has no λ function to fire at all, and 𝔼 gets stuck on
+-- it — the one behaviour left here. The script is handed the formation 'self'
+-- (its λ binding already removed, so it may dispatch on it) and the universe
+-- 'univ'; the state 𝑠 is not part of that contract yet, so it is threaded
+-- through untouched.
 atom :: T.Text -> Expression -> Expression -> State -> DataizeContext -> IO (Expression, State)
-atom "L_number_plus" self univ state ctx = do
-  (left, lstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx
-  (right, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx
-  case (asNumber left, asNumber right) of
-    (Just first, Just second) -> pure (DataNumber (numToBts (first + second)), rstate)
-    _ -> pure (ExTermination, rstate)
-atom "L_number_times" self univ state ctx = do
-  (left, lstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx
-  (right, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx
-  case (asNumber left, asNumber right) of
-    (Just first, Just second) -> pure (DataNumber (numToBts (first * second)), rstate)
-    _ -> pure (ExTermination, rstate)
-atom "L_number_div" self univ state ctx = do
-  (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx
-  case (asNumber x, asNumber rho) of
-    (Just divisor, Just dividend) -> pure (DataNumber (numToBts (dividend / divisor)), rstate)
-    _ -> pure (ExTermination, rstate)
-atom "L_number_gt" self univ state ctx = do
-  (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx
-  case (asNumber x, asNumber rho) of
-    (Just threshold, Just value) -> pure (boolean (value > threshold), rstate)
-    _ -> pure (ExTermination, rstate)
-atom "L_bytes_and" self univ state ctx = bitwise btsAnd self univ state ctx
-atom "L_bytes_or" self univ state ctx = bitwise btsOr self univ state ctx
-atom "L_bytes_not" self univ state ctx = do
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ state ctx
-  pure (dataBytes (btsNot rho), rstate)
-atom "L_bytes_concat" self univ state ctx = do
-  (b, bstate) <- _dataize (ExDispatch self (AtLabel "b")) univ state ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx
-  pure (dataBytes (btsConcat rho b), rstate)
-atom "L_bytes_eq" self univ state ctx = do
-  (b, bstate) <- _dataize (ExDispatch self (AtLabel "b")) univ state ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ bstate ctx
-  pure (boolean (btsEqual rho b), rstate)
-atom "L_bytes_size" self univ state ctx = do
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ state ctx
-  pure (DataNumber (numToBts (fromIntegral (btsSize rho))), rstate)
-atom "L_bytes_right" self univ state ctx = do
-  (x, xstate) <- _dataize (ExDispatch self (AtLabel "x")) univ state ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ xstate ctx
-  case asInt x of
-    Just bits -> pure (dataBytes (btsShift bits rho), rstate)
-    Nothing -> pure (ExTermination, rstate)
-atom "L_bytes_slice" self univ state ctx = do
-  (start, sstate) <- _dataize (ExDispatch self (AtLabel "start")) univ state ctx
-  (len, lstate) <- _dataize (ExDispatch self (AtLabel "len")) univ sstate ctx
-  (rho, rstate) <- _dataize (ExDispatch self AtRho) univ lstate ctx
-  case (asInt start, asInt len) of
-    (Just from, Just count)
-      | from >= 0 && count >= 0 ->
-          pure (maybe (cantSlice from count (btsSize rho)) dataBytes (btsSlice from count rho), rstate)
-    _ -> pure (ExTermination, rstate)
-  where
-    -- A window past the end of the array does not stop EO: it copies the
-    -- 'cant-slice' fallback, applies the complaint to it and lets the caller
-    -- decide. A caller that left 'cant-slice' unbound gets ⊥ out of the dispatch
-    cantSlice :: Int -> Int -> Int -> Expression
-    cantSlice from count size =
-      ExApplication
-        (ExDispatch self (AtLabel "cant-slice"))
-        (ArAlpha (Alpha 0) (DataString (strToBts (printf "cannot slice '%d' bytes from offset '%d' of bytes of size %d" count from size))))
-atom func _ _ _ _ = throwIO (Stuck func)
+atom func self univ state ctx = case registeredAtom ctx._atoms func of
+  Nothing -> throwIO (Stuck func)
+  Just registered -> do
+    raw <- fireAtom func registered self univ
+    pure (raw, state)
 
 -- Augment the injected, context-free term builder with the dataization and
 -- morphing operations that need the universe: 'evaluate' applies an atom and
@@ -609,14 +522,12 @@
 -- Every firing is reported to '_saveEval', which the '--evaluations' option
 -- turns into one record per line. The reported result is the normal form 𝔼
 -- returns, never the atom's raw answer, so the protocol and the caller see the
--- same term. A nested firing — an atom that dataizes its own arguments —
--- completes first, so it is reported before the firing that triggered it. A
+-- same term. Firings are reported in the order they complete, so the atom of a
+-- head reduced by 'ml' is reported before the one dispatched on its result. A
 -- firing that gets stuck is reported too, with no result, when the run is a
 -- partial evaluation rather than a failure ('_partial'): the site is what the
--- caller wants to learn then, and the nested order holds, since the unknown
--- atom is reported before the known one whose input reached it. The report is
--- made before the signal goes on to the spine, where 'parking' attaches the
--- derivation to it.
+-- caller wants to learn then. The report is made before the signal goes on to
+-- the spine, where 'parking' attaches the derivation to it.
 _evaluate :: DataizeContext -> State -> BuildTermMethodS
 _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do
   form <- buildExpressionThrows expr subst
diff --git a/src/Matcher.hs b/src/Matcher.hs
--- a/src/Matcher.hs
+++ b/src/Matcher.hs
@@ -22,9 +22,17 @@
   | MvExpression Expression -- !e
   deriving (Eq, Show)
 
+-- The left-hand side of a substitution: a meta-variable the rule author named
+-- and may reference from a result, or an anonymous slot that only the pattern
+-- it was written in can address
+data Meta
+  = Named Text
+  | Anon Slot
+  deriving (Eq, Ord, Show)
+
 -- Substitution
--- Shows the match of meta name to meta value
-newtype Subst = Subst (Map Text MetaValue)
+-- Shows the match of meta variable to meta value
+newtype Subst = Subst (Map Meta MetaValue)
   deriving (Eq, Show)
 
 -- A way to match a pattern expression against a target expression, yielding
@@ -37,14 +45,18 @@
 
 -- Singleton substitution with one (key -> value) pair
 substSingle :: Text -> MetaValue -> Subst
-substSingle key value = Subst (Map.singleton key value)
+substSingle key value = Subst (Map.singleton (Named key) value)
 
+-- Singleton substitution binding one anonymous slot
+substSlot :: Slot -> MetaValue -> Subst
+substSlot slot value = Subst (Map.singleton (Anon slot) value)
+
 -- Combine two substitutions into a single one
 -- Fails if values by the same keys are not equal
 combine :: Subst -> Subst -> Maybe Subst
 combine (Subst a) (Subst b) = go (Map.toList b) a
   where
-    go :: [(Text, MetaValue)] -> Map Text MetaValue -> Maybe Subst
+    go :: [(Meta, MetaValue)] -> Map Meta MetaValue -> Maybe Subst
     go [] acc = Just (Subst acc)
     go ((key, value) : rest) acc = case Map.lookup key acc of
       Just found
@@ -57,18 +69,21 @@
 
 matchAttribute :: Attribute -> Attribute -> [Subst]
 matchAttribute (AtMeta meta) tgt = [substSingle meta (MvAttribute tgt)]
+matchAttribute (AtAny slot) tgt = [substSlot slot (MvAttribute tgt)]
 matchAttribute ptn tgt
   | ptn == tgt = [substEmpty]
   | otherwise = []
 
 matchAlpha :: Alpha -> Alpha -> [Subst]
 matchAlpha (AlMeta meta) (Alpha idx) = [substSingle meta (MvIndex idx)]
+matchAlpha (AlAny slot) (Alpha idx) = [substSlot slot (MvIndex idx)]
 matchAlpha ptn tgt
   | ptn == tgt = [substEmpty]
   | otherwise = []
 
 matchFunction :: Function -> Function -> [Subst]
 matchFunction (FnMeta meta) (Function name) = [substSingle meta (MvFunction name)]
+matchFunction (FnAny slot) (Function name) = [substSlot slot (MvFunction name)]
 matchFunction ptn tgt
   | ptn == tgt = [substEmpty]
   | otherwise = []
@@ -76,6 +91,7 @@
 matchBinding :: Binding -> Binding -> [Subst]
 matchBinding (BiVoid pattr) (BiVoid tattr) = matchAttribute pattr tattr
 matchBinding (BiDelta (BtMeta meta)) (BiDelta tdata) = [substSingle meta (MvBytes tdata)]
+matchBinding (BiDelta (BtAny slot)) (BiDelta tdata) = [substSlot slot (MvBytes tdata)]
 matchBinding (BiDelta pdata) (BiDelta tdata)
   | pdata == tdata = [substEmpty]
   | otherwise = []
@@ -92,18 +108,24 @@
 matchBindings :: [Binding] -> [Binding] -> [Subst]
 matchBindings [] [] = [substEmpty]
 matchBindings [] _ = []
-matchBindings ((BiMeta name) : pbs) tbs =
-  let splits = [splitAt idx tbs | idx <- [0 .. length tbs]]
-   in catMaybes
-        [ combine (substSingle name (MvBindings before)) subst
-        | (before, after) <- splits
-        , subst <- matchBindings pbs after
-        ]
+matchBindings ((BiMeta name) : pbs) tbs = matchBindingsMeta (substSingle name) pbs tbs
+matchBindings ((BiAny slot) : pbs) tbs = matchBindingsMeta (substSlot slot) pbs tbs
 matchBindings (pb : pbs) (tb : tbs) = combineMany (matchBinding pb tb) (matchBindings pbs tbs)
 matchBindings _ _ = []
 
+-- A meta binding stands for any leading run of the target bindings, so every
+-- way of splitting the target into that run and the rest is tried.
+matchBindingsMeta :: (MetaValue -> Subst) -> [Binding] -> [Binding] -> [Subst]
+matchBindingsMeta bind pbs tbs =
+  catMaybes
+    [ combine (bind (MvBindings before)) subst
+    | (before, after) <- [splitAt idx tbs | idx <- [0 .. length tbs]]
+    , subst <- matchBindings pbs after
+    ]
+
 matchExpression' :: MatchExpressionFunc
 matchExpression' (ExMeta meta) tgt = [substSingle meta (MvExpression tgt)]
+matchExpression' (ExAny slot) tgt = [substSlot slot (MvExpression tgt)]
 matchExpression' ExXi ExXi = [substEmpty]
 matchExpression' ExRoot ExRoot = [substEmpty]
 matchExpression' ExTermination ExTermination = [substEmpty]
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -36,6 +36,7 @@
 attributeFromBinding (BiDelta _) = Just AtDelta
 attributeFromBinding (BiLambda _) = Just AtLambda
 attributeFromBinding (BiMeta _) = Nothing
+attributeFromBinding (BiAny _) = Nothing
 
 -- Extract attributes from bindings
 attributesFromBindings :: [Binding] -> [Attribute]
@@ -79,8 +80,11 @@
     go (bd : rest) hasRho =
       case bd of
         BiMeta _ -> bd : rest
+        BiAny _ -> bd : rest
         BiVoid (AtMeta _) -> bd : rest
+        BiVoid (AtAny _) -> bd : rest
         BiTau (AtMeta _) _ -> bd : rest
+        BiTau (AtAny _) _ -> bd : rest
         BiVoid AtRho -> bd : go rest True
         BiTau AtRho _ -> bd : go rest True
         _ -> bd : go rest hasRho
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -48,14 +48,14 @@
 data PhiParser = PhiParser
   { _attribute :: Parser Attribute
   , _alpha :: Parser Alpha
-  , _index :: Parser T.Text
+  , _index :: Parser (Either Slot T.Text)
   , _binding :: Parser Binding
   , _expression :: Parser Expression
   , _string :: Parser String
   }
 
 phiParser :: PhiParser
-phiParser = PhiParser attribute alpha index' binding expression quotedStr
+phiParser = PhiParser attribute alpha indexVar binding expression quotedStr
 
 instance Show ParserException where
   show CouldNotParseExpression{..} = printf "Couldn't parse given phi expression, cause: %s" message
@@ -122,23 +122,24 @@
 metaSuffix :: Parser String
 metaSuffix = lexeme (many (oneOf ('_' : '-' : ['0' .. '9'] ++ ['a' .. 'z'] ++ ['A' .. 'Z']) <?> "meta suffix"))
 
--- Meta variable names are packed to Text once here; all AST meta fields are Text
-meta :: Char -> Parser T.Text
-meta ch = do
-  _ <- char '!'
-  c <- char ch
-  suf <- metaSuffix
-  return (T.pack (c : suf))
-
-meta' :: Char -> String -> Parser T.Text
-meta' ch uni =
-  choice
-    [ meta ch
-    , do
-        _ <- string uni
-        suf <- metaSuffix
-        return (T.pack (ch : suf))
-    ]
+-- A meta-variable, written either in ASCII ('!t') or in Unicode ('𝜏'). The
+-- suffix tells the two kinds apart: with one the variable is named and a rule
+-- may reference it from its result, without one it is an anonymous slot
+-- pinned to the offset it starts at, unique within the parsed term. Named
+-- variables are packed to Text once here; all AST meta fields are Text.
+metaVar :: Char -> String -> Parser (Either Slot T.Text)
+metaVar ch uni = do
+  offset <- getOffset
+  suf <-
+    choice
+      [ char '!' >> char ch >> metaSuffix
+      , string uni >> metaSuffix
+      ]
+  return
+    ( if null suf
+        then Left (Slot (T.singleton ch) offset)
+        else Right (T.pack (ch : suf))
+    )
 
 byte :: Parser String
 byte = do
@@ -160,7 +161,7 @@
 bytes =
   lexeme
     ( choice
-        [ BtMeta <$> meta' 'd' "δ"
+        [ either BtAny BtMeta <$> metaVar 'd' "δ"
         , symbol "--" >> return BtEmpty
         , try $ do
             first <- byte
@@ -290,7 +291,7 @@
     rb = symbol ")"
 
 metaBinding :: Parser Binding
-metaBinding = BiMeta <$> meta' 'B' "𝐵"
+metaBinding = either BiAny BiMeta <$> metaVar 'B' "𝐵"
 
 -- binding
 -- 1. delta
@@ -313,7 +314,7 @@
     , try metaBinding
     , do
         _ <- try lambda
-        BiLambda <$> choice [Function . T.pack <$> function, FnMeta <$> meta' 'F' "𝑓"]
+        BiLambda <$> choice [Function . T.pack <$> function, either FnAny FnMeta <$> metaVar 'F' "𝑓"]
     , do
         attr <- attribute
         choice
@@ -351,13 +352,13 @@
 attribute =
   choice
     [ void'
-    , AtMeta <$> meta' 't' "𝜏"
+    , either AtAny AtMeta <$> metaVar 't' "𝜏"
     ]
     <?> "attribute"
 
 -- index meta: !i, 𝑖
-index' :: Parser T.Text
-index' = meta' 'i' "𝑖"
+indexVar :: Parser (Either Slot T.Text)
+indexVar = metaVar 'i' "𝑖"
 
 -- alpha
 -- 1. index: ~0, α0
@@ -367,7 +368,7 @@
   _ <- choice [symbol "~", symbol "α"]
   choice
     [ Alpha <$> lexeme L.decimal
-    , AlMeta <$> index'
+    , either AlAny AlMeta <$> indexVar
     ]
     <?> "alpha"
 
@@ -423,9 +424,9 @@
         return ExTermination
     , number
     , lexeme (DataString . strToBts <$> quotedStr)
-    , try (ExMeta <$> meta' 'e' "𝑒")
-    , try (ExMeta <$> meta' 'n' "𝑛")
-    , try (ExMeta <$> meta' 'k' "𝑘")
+    , try (either ExAny ExMeta <$> metaVar 'e' "𝑒")
+    , try (either ExAny ExMeta <$> metaVar 'n' "𝑛")
+    , try (either ExAny ExMeta <$> metaVar 'k' "𝑘")
     , ExDispatch ExXi <$> attribute
     ]
     <?> "expression head"
@@ -508,8 +509,8 @@
 parseAlpha :: String -> Either String Alpha
 parseAlpha = parse' "alpha" alpha
 
-parseIndex :: String -> Either String T.Text
-parseIndex = parse' "index meta" index'
+parseIndex :: String -> Either String (Either Slot T.Text)
+parseIndex = parse' "index meta" indexVar
 
 parseAttributeThrows :: String -> IO Attribute
 parseAttributeThrows attr = orThrow CouldNotParseAttribute (parseAttribute attr)
diff --git a/src/Printer.hs b/src/Printer.hs
--- a/src/Printer.hs
+++ b/src/Printer.hs
@@ -101,11 +101,19 @@
 printMetaValue (MvBindings bds) config = printExpression' (ExFormation bds) config
 printMetaValue (MvFunction fun) _ = T.unpack fun
 
+-- An anonymous slot is reported under the bare sigil it was written with,
+-- just as a named meta is reported under its name. Two slots of one kind
+-- therefore share a line label while keeping their own values, which is all
+-- the report can say about a variable no rule may refer back to.
+printMeta :: Meta -> String
+printMeta (Named name) = T.unpack name
+printMeta (Anon (Slot kind _)) = T.unpack kind
+
 printSubst :: Subst -> PrintConfig -> String
 printSubst (Subst mp) config =
   intercalate
     "\n"
-    (map (\(key, value) -> T.unpack key <> " >> " <> printMetaValue value config) (Map.toList mp))
+    (map (\(key, value) -> printMeta key <> " >> " <> printMetaValue value config) (Map.toList mp))
 
 printSubsts' :: [Subst] -> PrintConfig -> String
 printSubsts' [] _ = "------"
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -163,6 +163,7 @@
     isMetaBinding :: Binding -> Bool
     isMetaBinding = \case
       BiMeta _ -> True
+      BiAny _ -> True
       _ -> False
     hasMetaBindings = foldl (\acc bd -> acc || isMetaBinding bd) False
 tryBuildAndReplaceFast state _ = buildAndReplace' state replaceExpression
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -113,13 +113,13 @@
 -- Convert a 'Number' to an 'Int' under the given substitution, resolving
 -- index metas, binding lengths and formation domains.
 numToInt :: Y.Number -> Subst -> Maybe Int
-numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup meta mp of
+numToInt (Y.MetaIndex meta) (Subst mp) = case M.lookup (Named meta) mp of
   Just (MvIndex idx) -> Just idx
   _ -> Nothing
-numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup meta mp of
+numToInt (Y.Length (BiMeta meta)) (Subst mp) = case M.lookup (Named meta) mp of
   Just (MvBindings bds) -> Just (length bds)
   _ -> Nothing
-numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup meta mp of
+numToInt (Y.Domain (BiMeta meta)) (Subst mp) = case M.lookup (Named meta) mp of
   Just (MvBindings bds) -> Just (length (filter notAsset bds))
   _ -> Nothing
   where
@@ -136,26 +136,26 @@
 _eq (Y.CmpAttr left) (Y.CmpAttr right) subst _ = pure [subst | compareAttrs left right subst]
   where
     compareAttrs :: Attribute -> Attribute -> Subst -> Bool
-    compareAttrs (AtMeta left) (AtMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of
+    compareAttrs (AtMeta left) (AtMeta right) (Subst mp) = case (M.lookup (Named left) mp, M.lookup (Named right) mp) of
       (Just (MvAttribute left'), Just (MvAttribute right')) -> compareAttrs left' right' (Subst mp)
       _ -> False
-    compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup meta mp of
+    compareAttrs attr (AtMeta meta) (Subst mp) = case M.lookup (Named meta) mp of
       Just (MvAttribute found) -> attr == found
       _ -> False
-    compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup meta mp of
+    compareAttrs (AtMeta meta) attr (Subst mp) = case M.lookup (Named meta) mp of
       Just (MvAttribute found) -> attr == found
       _ -> False
     compareAttrs left right _ = right == left
 _eq (Y.CmpExpr left) (Y.CmpExpr right) subst _ = pure [subst | compareExprs left right subst]
   where
     compareExprs :: Expression -> Expression -> Subst -> Bool
-    compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup left mp, M.lookup right mp) of
+    compareExprs (ExMeta left) (ExMeta right) (Subst mp) = case (M.lookup (Named left) mp, M.lookup (Named right) mp) of
       (Just (MvExpression left'), Just (MvExpression right')) -> compareExprs left' right' (Subst mp)
       _ -> False
-    compareExprs expr (ExMeta meta) (Subst mp) = case M.lookup meta mp of
+    compareExprs expr (ExMeta meta) (Subst mp) = case M.lookup (Named meta) mp of
       Just (MvExpression found) -> expr == found
       _ -> False
-    compareExprs (ExMeta meta) expr (Subst mp) = case M.lookup meta mp of
+    compareExprs (ExMeta meta) expr (Subst mp) = case M.lookup (Named meta) mp of
       Just (MvExpression found) -> expr == found
       _ -> False
     compareExprs left right _ = left == right
@@ -170,9 +170,12 @@
 _gt _ _ _ _ = pure []
 
 _nf :: Expression -> Subst -> RuleContext -> IO [Subst]
-_nf (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of
+_nf (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of
   Just (MvExpression expr) -> _nf expr (Subst mp) ctx
   _ -> pure []
+_nf (ExAny slot) (Subst mp) ctx = case M.lookup (Anon slot) mp of
+  Just (MvExpression expr) -> _nf expr (Subst mp) ctx
+  _ -> pure []
 _nf expr subst ctx = pure [subst | isNF expr ctx]
 
 -- An expression is xi-free when it contains no ξ outside of a formation: it is
@@ -184,9 +187,12 @@
 -- structural, rules out the ξ-recursion the normal-form check could loop on)
 -- and the normal-form check second.
 _absolute :: Expression -> Subst -> RuleContext -> IO [Subst]
-_absolute (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of
+_absolute (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of
   Just (MvExpression expr) -> _absolute expr (Subst mp) ctx
   _ -> pure []
+_absolute (ExAny slot) (Subst mp) ctx = case M.lookup (Anon slot) mp of
+  Just (MvExpression expr) -> _absolute expr (Subst mp) ctx
+  _ -> pure []
 _absolute expr subst _ = pure [subst | xiFree expr]
   where
     xiFree :: Expression -> Bool
@@ -201,7 +207,7 @@
 -- Hold when the given expression is a formation (an abstraction ⟦…⟧). A meta
 -- is resolved first, so 'binding 𝑛' inspects whatever 𝑛 is bound to.
 _isFormation :: Expression -> Subst -> RuleContext -> IO [Subst]
-_isFormation (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of
+_isFormation (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of
   Just (MvExpression expr) -> _isFormation expr (Subst mp) ctx
   _ -> pure []
 _isFormation expr subst _ = pure [subst | isFormation expr]
@@ -211,7 +217,7 @@
     isFormation _ = False
 
 _matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst]
-_matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of
+_matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of
   Just (MvExpression expr) -> _matches pat expr (Subst mp) ctx
   _ -> pure []
 _matches pat expr subst ctx = do
@@ -328,27 +334,32 @@
     logDebug "Extra substitutions have been built"
     pure (catMaybes res)
 
--- Collect the names of constrained expression meta-variables with the given
+-- Collect the constrained expression meta-variables with the given
 -- one-character prefix used in a pattern. Each kind ('𝑛'/'!n' normal-form,
 -- '𝑘'/'!k' absolute) lives in its own 'n'-/'k'-prefixed key-space, so a
--- pattern may freely mix them with plain '𝑒' captures.
-metaNamesWithPrefix :: T.Text -> Expression -> [T.Text]
-metaNamesWithPrefix prefix = nub . go
+-- pattern may freely mix them with plain '𝑒' captures. An anonymous meta
+-- carries the same prefix as the sigil it was written with, so a bare '𝑛' is
+-- held to the normal form just as '𝑛1' is.
+metasWithPrefix :: T.Text -> Expression -> [Expression]
+metasWithPrefix prefix = nub . go
   where
-    go :: Expression -> [T.Text]
-    go (ExMeta mt)
-      | T.isPrefixOf prefix mt = [mt]
+    go :: Expression -> [Expression]
+    go expr@(ExMeta mt)
+      | T.isPrefixOf prefix mt = [expr]
       | otherwise = []
+    go expr@(ExAny (Slot kind _))
+      | T.isPrefixOf prefix kind = [expr]
+      | otherwise = []
     go (ExFormation bds) = concatMap goBinding bds
     go (ExApplication e arg) = go e ++ goArgument arg
     go (ExDispatch e _) = go e
     go (ExPhiMeet _ _ e) = go e
     go (ExPhiAgain _ _ e) = go e
     go _ = []
-    goBinding :: Binding -> [T.Text]
+    goBinding :: Binding -> [Expression]
     goBinding (BiTau _ e) = go e
     goBinding _ = []
-    goArgument :: Argument -> [T.Text]
+    goArgument :: Argument -> [Expression]
     goArgument (ArTau _ expr) = go expr
     goArgument (ArAlpha _ expr) = go expr
 
@@ -381,8 +392,8 @@
           -- A '𝑘' meta-variable is absolute (𝒦 ⊆ 𝒩): check it is xi-free first
           -- (cheap, structural), then fold its name into the same normal-form
           -- check used for '𝑛' metas, so 'isNF' is applied in a single place.
-          inXiFree <- foldlM (\substs nm -> meetCondition (Y.Absolute (ExMeta nm)) substs ctx) matched (kMetaNames ptn)
-          inNf <- foldlM (\substs nm -> meetCondition (Y.NF (ExMeta nm)) substs ctx) inXiFree (nfMetaNames ptn ++ kMetaNames ptn)
+          inXiFree <- foldlM (\substs mt -> meetCondition (Y.Absolute mt) substs ctx) matched (kMetas ptn)
+          inNf <- foldlM (\substs mt -> meetCondition (Y.NF mt) substs ctx) inXiFree (nfMetas ptn ++ kMetas ptn)
           if null inNf
             then do
               logDebug "A '𝑛'/'𝑘' meta-variable is not in normal form, or a '𝑘' meta-variable is not xi-free"
@@ -405,8 +416,8 @@
                       when (null met) (logDebug "The 'having' condition wasn't met")
                       pure met
   where
-    nfMetaNames :: Expression -> [T.Text]
-    nfMetaNames = metaNamesWithPrefix "n"
+    nfMetas :: Expression -> [Expression]
+    nfMetas = metasWithPrefix "n"
 
-    kMetaNames :: Expression -> [T.Text]
-    kMetaNames = metaNamesWithPrefix "k"
+    kMetas :: Expression -> [Expression]
+    kMetas = metasWithPrefix "k"
diff --git a/src/Slots.hs b/src/Slots.hs
new file mode 100644
--- /dev/null
+++ b/src/Slots.hs
@@ -0,0 +1,65 @@
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+-- The goal of the module is to collect the anonymous meta-variable slots a
+-- term was written with. A rule binds them where it matches and nowhere else,
+-- so every other part of a rule is asked for its slots and rejected when it
+-- has any.
+module Slots (Slots (..), anonymous) where
+
+import AST
+import Data.Text (Text)
+
+class Slots a where
+  slots :: a -> [Slot]
+
+-- The kind sigil of the first anonymous meta a term was written with, if any,
+-- so a caller can word its own complaint about a term that must have none
+anonymous :: (Slots a) => a -> Maybe Text
+anonymous term = case slots term of
+  [] -> Nothing
+  Slot kind _ : _ -> Just kind
+
+instance (Slots a) => Slots [a] where
+  slots = concatMap slots
+
+instance (Slots a) => Slots (Maybe a) where
+  slots = maybe [] slots
+
+instance Slots Expression where
+  slots (ExAny slot) = [slot]
+  slots (ExFormation bds) = slots bds
+  slots (ExApplication expr arg) = slots expr ++ slots arg
+  slots (ExDispatch expr attr) = slots expr ++ slots attr
+  slots (ExPhiMeet _ _ expr) = slots expr
+  slots (ExPhiAgain _ _ expr) = slots expr
+  slots (ExBytes bts) = slots bts
+  slots _ = []
+
+instance Slots Argument where
+  slots (ArTau attr expr) = slots attr ++ slots expr
+  slots (ArAlpha alpha expr) = slots alpha ++ slots expr
+
+instance Slots Binding where
+  slots (BiAny slot) = [slot]
+  slots (BiTau attr expr) = slots attr ++ slots expr
+  slots (BiVoid attr) = slots attr
+  slots (BiDelta bts) = slots bts
+  slots (BiLambda func) = slots func
+  slots (BiMeta _) = []
+
+instance Slots Attribute where
+  slots (AtAny slot) = [slot]
+  slots _ = []
+
+instance Slots Alpha where
+  slots (AlAny slot) = [slot]
+  slots _ = []
+
+instance Slots Bytes where
+  slots (BtAny slot) = [slot]
+  slots _ = []
+
+instance Slots Function where
+  slots (FnAny slot) = [slot]
+  slots _ = []
diff --git a/src/Yaml.hs b/src/Yaml.hs
--- a/src/Yaml.hs
+++ b/src/Yaml.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
@@ -22,6 +23,7 @@
 import qualified Data.Yaml as Yaml
 import GHC.Generics (Generic)
 import Parser
+import Slots
 import Text.Printf (printf)
 
 -- Fail unless the object names exactly one of the expected keys
@@ -81,7 +83,8 @@
       | toRational (round num :: Integer) == toRational num -> pure (Literal (round num))
       | otherwise -> fail (printf "Expected an integer, got a fractional number %s" (show num))
     String txt -> case parseIndex (unpack txt) of
-      Right mt -> pure (MetaIndex mt)
+      Right (Right mt) -> pure (MetaIndex mt)
+      Right (Left slot) -> pure (AnyIndex slot)
       Left err -> fail err
     _ ->
       fail "Expected a numerable expression (object, number or index meta)"
@@ -172,16 +175,24 @@
       )
 
 instance FromJSON Rule where
-  parseJSON =
-    genericParseJSON
-      defaultOptions
-        { fieldLabelModifier = \case
-            "where_" -> "where"
-            other -> other
-        }
+  parseJSON value = do
+    rule <-
+      genericParseJSON
+        defaultOptions
+          { fieldLabelModifier = \case
+              "where_" -> "where"
+              other -> other
+          }
+        value
+    referenceless rule.name "result" rule.result
+    referenceless rule.name "when" rule.when
+    referenceless rule.name "where" rule.where_
+    referenceless rule.name "having" rule.having
+    pure rule
 
 data Number
   = MetaIndex Text
+  | AnyIndex Slot
   | Length Binding
   | Domain Binding
   | Literal Int
@@ -234,6 +245,68 @@
   }
   deriving (Generic, Show)
 
+instance Slots Condition where
+  slots (And conds) = slots conds
+  slots (Or conds) = slots conds
+  slots (Not cond) = slots cond
+  slots (In attr bd) = slots attr ++ slots bd
+  slots (Eq left right) = slots left ++ slots right
+  slots (Gt left right) = slots left ++ slots right
+  slots (NF expr) = slots expr
+  slots (Absolute expr) = slots expr
+  slots (Matches _ expr) = slots expr
+  slots (PartOf expr bd) = slots expr ++ slots bd
+  slots (Disjoint attrs bds) = slots attrs ++ slots bds
+  slots (IsFormation expr) = slots expr
+
+instance Slots Comparable where
+  slots (CmpAttr attr) = slots attr
+  slots (CmpNum num) = slots num
+  slots (CmpExpr expr) = slots expr
+
+instance Slots Number where
+  slots (AnyIndex slot) = [slot]
+  slots (Length bd) = slots bd
+  slots (Domain bd) = slots bd
+  slots (MetaIndex _) = []
+  slots (Literal _) = []
+
+instance Slots ExtraArgument where
+  slots (ArgAttribute attr) = slots attr
+  slots (ArgExpression expr) = slots expr
+  slots (ArgBinding bd) = slots bd
+  slots (ArgBytes bts) = slots bts
+
+instance Slots Extra where
+  slots extra = slots extra.meta ++ slots extra.args
+
+instance Slots Premise where
+  slots premise = slots premise.operation
+
+instance Slots Operation where
+  slots (OpMorph expr) = slots expr
+  slots (OpNormalize expr) = slots expr
+  slots (OpEvaluate expr universe) = slots expr ++ slots universe
+  slots (OpContextualize expr context) = slots expr ++ slots context
+  slots (OpDataize expr) = slots expr
+
+-- An anonymous meta-variable is bound by the pattern it stands in and is
+-- forgotten as soon as that pattern matches, so it has no name for any other
+-- part of a rule to read it back by. Writing one outside the pattern is
+-- therefore a mistake in the rule, not a term to be resolved later, and the
+-- rule is rejected as it loads.
+referenceless :: (MonadFail m, Slots a) => String -> String -> a -> m ()
+referenceless rule field term = case anonymous term of
+  Nothing -> pure ()
+  Just kind ->
+    fail
+      ( printf
+          "anonymous meta '!%s' cannot be referenced in '%s' of rule '%s'"
+          (unpack kind)
+          field
+          rule
+      )
+
 normalizationRules :: [Rule]
 {-# NOINLINE normalizationRules #-}
 normalizationRules = map decodeRule $(embedDir "resources/normalize")
@@ -323,11 +396,13 @@
   expr <- o .:? "n-result"
   case expr of
     Just (ExMeta metaName) -> pure metaName
+    Just (ExAny _) -> fail "an anonymous 'n-result' meta cannot be referenced"
     Just _ -> fail "'n-result' must be an expression meta"
     Nothing -> do
       bytes <- o .:? "d-result"
       case bytes of
         Just (BtMeta metaName) -> pure metaName
+        Just (BtAny _) -> fail "an anonymous 'd-result' meta cannot be referenced"
         Just _ -> fail "'d-result' must be a bytes meta"
         Nothing -> fail "a premise needs an 'n-result' or 'd-result' meta"
 
@@ -367,13 +442,18 @@
       "MorphRule"
       ( \o -> do
           ruleName <- o .: "name"
-          MorphRule ruleName
-            <$> parseLabel ruleName o
-            <*> o .: "match"
-            <*> o .: "e-match"
-            <*> o .: "n-result"
-            <*> o .:? "when"
-            <*> o .:? "premises" .!= []
+          rule <-
+            MorphRule ruleName
+              <$> parseLabel ruleName o
+              <*> o .: "match"
+              <*> o .: "e-match"
+              <*> o .: "n-result"
+              <*> o .:? "when"
+              <*> o .:? "premises" .!= []
+          referenceless ruleName "n-result" rule.nresult
+          referenceless ruleName "when" rule.when
+          referenceless ruleName "premises" rule.premises
+          pure rule
       )
 
 instance FromJSON DataizeRule where
@@ -382,13 +462,18 @@
       "DataizeRule"
       ( \o -> do
           ruleName <- o .: "name"
-          DataizeRule ruleName
-            <$> parseLabel ruleName o
-            <*> o .: "match"
-            <*> o .: "e-match"
-            <*> o .: "d-result"
-            <*> o .:? "when"
-            <*> o .:? "premises" .!= []
+          rule <-
+            DataizeRule ruleName
+              <$> parseLabel ruleName o
+              <*> o .: "match"
+              <*> o .: "e-match"
+              <*> o .: "d-result"
+              <*> o .:? "when"
+              <*> o .:? "premises" .!= []
+          referenceless ruleName "d-result" rule.dresult
+          referenceless ruleName "when" rule.when
+          referenceless ruleName "premises" rule.premises
+          pure rule
       )
 
 instance FromJSON ContextualizeRule where
@@ -397,12 +482,16 @@
       "ContextualizeRule"
       ( \o -> do
           ruleName <- o .: "name"
-          ContextualizeRule ruleName
-            <$> parseLabel ruleName o
-            <*> o .: "match"
-            <*> o .: "c-match"
-            <*> o .: "c-result"
-            <*> o .:? "premises" .!= []
+          rule <-
+            ContextualizeRule ruleName
+              <$> parseLabel ruleName o
+              <*> o .: "match"
+              <*> o .: "c-match"
+              <*> o .: "c-result"
+              <*> o .:? "premises" .!= []
+          referenceless ruleName "c-result" rule.cresult
+          referenceless ruleName "premises" rule.premises
+          pure rule
       )
 
 decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a]
diff --git a/test/AtomsSpec.hs b/test/AtomsSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/AtomsSpec.hs
@@ -0,0 +1,154 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module AtomsSpec (spec) where
+
+import AST
+import Atoms (Atom (..), Runtime (RtNode), emptyRegistry, fireAtom, readRegistry, registeredAtom)
+import Control.Exception (SomeException, bracket)
+import Control.Monad (forM_)
+import Data.ByteString qualified as BS
+import Data.List (isInfixOf)
+import Data.Text qualified as T
+import Data.Text.Encoding (encodeUtf8)
+import Fixtures (withNode)
+import Parser (parseExpressionThrows)
+import System.Directory (getTemporaryDirectory, removePathForcibly)
+import System.IO (Handle, hClose, openBinaryTempFile)
+import Test.Hspec
+
+-- A registry file holding the given content, removed afterwards
+withRegistry :: T.Text -> (FilePath -> IO a) -> IO a
+withRegistry content action = do
+  dir <- getTemporaryDirectory
+  bracket (openBinaryTempFile dir "phino-registry-.json") discarded $ \(path, handle) -> do
+    BS.hPut handle (encodeUtf8 content)
+    hClose handle
+    action path
+  where
+    discarded :: (FilePath, Handle) -> IO ()
+    discarded (path, handle) = hClose handle >> removePathForcibly path
+
+-- Fire the λ function 'L_answer' out of the given script, against a formation
+-- binding 'x' inside a universe binding 'y'
+fired :: T.Text -> IO Expression
+fired script = do
+  form <- parseExpressionThrows "⟦ x ↦ ⟦ Δ ⤍ 01- ⟧ ⟧"
+  univ <- parseExpressionThrows "⟦ y ↦ ⟦ Δ ⤍ 02- ⟧ ⟧"
+  fireAtom "L_answer" (Atom RtNode script) form univ
+
+-- What the script wrote under 'n' has to come back parsed, so a case asserting
+-- on it says which expression it expects in 𝜑 rather than in constructors
+answers :: T.Text -> String -> Expectation
+answers script expected = withNode $ do
+  answer <- fired script
+  wanted <- parseExpressionThrows expected
+  answer `shouldBe` wanted
+
+-- A firing that has to fail, with the reason naming the given fragments
+fails :: T.Text -> [String] -> Expectation
+fails script fragments =
+  withNode $
+    fired script
+      `shouldThrow` (\failure -> all (`isInfixOf` show (failure :: SomeException)) fragments)
+
+spec :: Spec
+spec = do
+  -- phino implements no λ function, so an empty registry is what a run without
+  -- '--atoms' fires against: every name is unknown there
+  describe "emptyRegistry" $
+    it "registers no λ function at all" $
+      registeredAtom emptyRegistry "L_bytes_eq" `shouldBe` Nothing
+
+  describe "readRegistry" $ do
+    it "reads a λ function together with its runtime and script" $
+      withRegistry "{\"L_answer\": {\"rt\": \"node\", \"script\": \"say(1)\"}}" $ \path -> do
+        registry <- readRegistry path
+        registeredAtom registry "L_answer" `shouldBe` Just (Atom RtNode "say(1)")
+
+    it "leaves a name the file does not carry unregistered" $
+      withRegistry "{\"L_answer\": {\"rt\": \"node\", \"script\": \"say(1)\"}}" $ \path -> do
+        registry <- readRegistry path
+        registeredAtom registry "L_bytes_eq" `shouldBe` Nothing
+
+    -- An unknown runtime is refused where the file is read, which is before any
+    -- dataization starts, rather than at the moment an atom of it would fire
+    forM_
+      [
+        ( "the runtime is not one phino can run"
+        , "{\"L_answer\": {\"rt\": \"ruby\", \"script\": \"say(1)\"}}"
+        , ["unknown runtime 'ruby'", "node"]
+        )
+      ,
+        ( "an entry carries no script"
+        , "{\"L_answer\": {\"rt\": \"node\"}}"
+        , ["script"]
+        )
+      ,
+        ( "an entry carries no runtime"
+        , "{\"L_answer\": {\"script\": \"say(1)\"}}"
+        , ["rt"]
+        )
+      ,
+        ( "the file is not JSON at all"
+        , "L_answer: js"
+        , ["cannot be read"]
+        )
+      ]
+      ( \(desc, content, fragments) ->
+          it ("fails when " ++ desc) $
+            withRegistry content $ \path ->
+              readRegistry path
+                `shouldThrow` (\failure -> all (`isInfixOf` show (failure :: SomeException)) fragments)
+      )
+
+    it "fails when the file is not there" $
+      readRegistry "no-such-registry.json"
+        `shouldThrow` (\failure -> "cannot be read" `isInfixOf` show (failure :: SomeException))
+
+  describe "fireAtom" $ do
+    it "hands back the 𝜑-expression the script wrote under 'n'" $
+      answers "process.stdout.write(JSON.stringify({n: '⟦ Δ ⤍ 2A- ⟧'}))" "⟦ Δ ⤍ 2A- ⟧"
+
+    -- One script may stand for several λ functions, so the name of the one
+    -- being fired is its first command-line argument — where node puts it
+    it "names the λ function being fired as the first command-line argument" $
+      answers
+        "process.stdout.write(JSON.stringify({n: process.argv[2] === 'L_answer' ? '⟦ Δ ⤍ FF- ⟧' : '⟦ Δ ⤍ 00- ⟧'}))"
+        "⟦ Δ ⤍ FF- ⟧"
+
+    -- The formation being evaluated arrives under 'b' and the universe Φ under
+    -- 's', both as 𝜑 text on stdin
+    it "feeds the formation and the universe to the script on stdin" $
+      answers
+        "const {b, s} = JSON.parse(require('fs').readFileSync(0, 'utf8'));\
+        \process.stdout.write(JSON.stringify({n: b.includes('x ↦') && s.includes('y ↦') ? '⟦ Δ ⤍ FF- ⟧' : '⟦ Δ ⤍ 00- ⟧'}))"
+        "⟦ Δ ⤍ FF- ⟧"
+
+    -- Neither payload carries syntax sugar, whatever '--sweet' says about the
+    -- output of the run, so a script finds every datum spelled as a Δ binding
+    it "spells the payloads as canonical 𝜑-calculus" $
+      answers
+        "const {b} = JSON.parse(require('fs').readFileSync(0, 'utf8'));\
+        \process.stdout.write(JSON.stringify({n: b.includes('Δ ⤍ 01-') ? '⟦ Δ ⤍ FF- ⟧' : '⟦ Δ ⤍ 00- ⟧'}))"
+        "⟦ Δ ⤍ FF- ⟧"
+
+    it "reads a script that says nothing to stdin without waiting for it" $
+      answers "process.stdout.write(JSON.stringify({n: '⟦ Δ ⤍ 01- ⟧'}))" "⟦ Δ ⤍ 01- ⟧"
+
+    it "fails with the script's own complaint when it exits non-zero" $
+      fails
+        "process.stderr.write('no idea what to do');process.exit(4)"
+        ["L_answer", "exit code 4", "no idea what to do"]
+
+    it "fails when the script writes something other than JSON" $
+      fails "process.stdout.write('almost')" ["L_answer", "almost"]
+
+    it "fails when the script writes JSON with no 'n' in it" $
+      fails "process.stdout.write(JSON.stringify({m: '⟦ ⟧'}))" ["L_answer", "n"]
+
+    it "fails when what the script put under 'n' is not a 𝜑-expression" $
+      fails "process.stdout.write(JSON.stringify({n: '⟦ ⟧⟧'}))" ["L_answer"]
diff --git a/test/BuilderSpec.hs b/test/BuilderSpec.hs
--- a/test/BuilderSpec.hs
+++ b/test/BuilderSpec.hs
@@ -19,7 +19,7 @@
 test :: (Show a, Eq a) => (a -> Subst -> Either String a) -> [(String, a, [(T.Text, MetaValue)], Either String a)] -> SpecWith (Arg Expectation)
 test function useCases =
   forM_ useCases $ \(desc, expr, mp, res) ->
-    it desc $ function expr (Subst (Map.fromList mp)) `shouldBe` res
+    it desc $ function expr (Subst (Map.mapKeys Named (Map.fromList mp))) `shouldBe` res
 
 spec :: Spec
 spec = do
@@ -208,6 +208,38 @@
         )
       ]
       (\(desc, action, message) -> it desc (action `shouldThrow` (\exc -> message `isInfixOf` show (exc :: SomeException))))
+
+  describe "builds an anonymous meta only from the pattern that bound it" $ do
+    -- An anonymous slot is a key of the very substitution its own pattern
+    -- produced, which is how a fired pattern is rebuilt for replacement. Asked
+    -- for it under any other substitution, the builder says plainly that the
+    -- meta has no name to be referenced by, rather than inventing a term.
+    forM_
+      [
+        ( "buildExpression rebuilds an anonymous expression from its own slot"
+        , buildExpression (ExAny (Slot "e" 7)) (substSlot (Slot "e" 7) (MvExpression ExRoot))
+        , Right ExRoot
+        )
+      ,
+        ( "buildExpression refuses an anonymous expression bound by another pattern"
+        , buildExpression (ExAny (Slot "e" 7)) (substSlot (Slot "e" 9) (MvExpression ExRoot))
+        , Left "anonymous meta '!e' cannot be referenced"
+        )
+      ]
+      (\(desc, built, expected) -> it desc (built `shouldBe` expected))
+    forM_
+      [
+        ( "buildAttribute rebuilds an anonymous attribute from its own slot"
+        , buildAttribute (AtAny (Slot "t" 2)) (substSlot (Slot "t" 2) (MvAttribute AtPhi))
+        , Right AtPhi
+        )
+      ,
+        ( "buildAttribute refuses an anonymous attribute bound by another pattern"
+        , buildAttribute (AtAny (Slot "t" 2)) substEmpty
+        , Left "anonymous meta '!t' cannot be referenced"
+        )
+      ]
+      (\(desc, built, expected) -> it desc (built `shouldBe` expected))
 
   describe "build with duplicate attributes in bindings" $ do
     it "build binding with duplicates" $
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -15,6 +15,7 @@
 import Data.Time.Clock (addUTCTime, getCurrentTime)
 import Data.Time.Clock.POSIX (getPOSIXTime)
 import Data.Version (showVersion)
+import Fixtures (withFixtureRegistry, withNode)
 import GHC.IO.Handle
 import Paths_phino (version)
 import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, getTemporaryDirectory, listDirectory, removeDirectoryRecursive, removeFile, removePathForcibly, setModificationTime)
@@ -119,6 +120,13 @@
 testCLISucceeded :: [String] -> [String] -> Expectation
 testCLISucceeded args outputs = testCLI' args outputs (Right ())
 
+-- phino implements no λ function of its own, so a case that needs an atom to
+-- fire brings the fixture registry in and hands its path to the command as
+-- '--atoms' (see 'Fixtures'). Every such atom runs under 'node', so the case is
+-- pending where 'node' is not installed.
+withAtoms :: (String -> Expectation) -> Expectation
+withAtoms action = withNode (withFixtureRegistry (action . ("--atoms=" ++)))
+
 testCLIFailed :: [String] -> [String] -> Expectation
 testCLIFailed args outputs = testCLI' args outputs (Left (ExitFailure 1))
 
@@ -392,20 +400,21 @@
           doesFileExist (dir ++ "/00003.phi") `shouldReturn` True
 
     it "saves dataize steps to dir with --steps-dir" $
-      withTempDirectory "phino-steps-dataize" $ \dir ->
-        withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ do
-          testCLISucceeded
-            ["dataize", "--steps-dir=" ++ dir, "--sweet"]
-            ["40-26"]
-          doesDirectoryExist dir `shouldReturn` True
-          files <- listDirectory dir
-          let steps = sort files
-          -- The fix is about numbering, not about a specific rule set: the file
-          -- names must be distinct and contiguous from 00001, and there must be
-          -- more of them than a single normalization pass produces (this input
-          -- runs several normalizations, so a global counter yields more steps).
-          steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]
-          length steps `shouldSatisfy` (> 18)
+      withAtoms $ \atoms ->
+        withTempDirectory "phino-steps-dataize" $ \dir ->
+          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do
+            testCLISucceeded
+              ["dataize", atoms, "--steps-dir=" ++ dir, "--sweet"]
+              ["40-32"]
+            doesDirectoryExist dir `shouldReturn` True
+            files <- listDirectory dir
+            let steps = sort files
+            -- The fix is about numbering, not about a specific rule set: the file
+            -- names must be distinct and contiguous from 00001, and there must be
+            -- more of them than a single normalization pass produces (this input
+            -- runs several normalizations, so a global counter yields more steps).
+            steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]
+            length steps `shouldSatisfy` (> 18)
 
     it "saves steps with a .tex extension when --output=latex is used with --steps-dir" $
       withTempDirectory "phino-steps-latex" $ \dir ->
@@ -1070,10 +1079,11 @@
     -- The 𝕄/𝔻 recursion used to be unbounded, so this division kept morphing
     -- forever and no option could stop it (#1052)
     it "fails on --max-steps instead of morphing forever" $
-      withStdin "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" $
-        testCLIFailed
-          ["dataize", "--max-steps=40"]
-          ["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]
+      withAtoms $ \atoms ->
+        withStdin "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" $
+          testCLIFailed
+            ["dataize", atoms, "--max-steps=40"]
+            ["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]
 
     it "dataizes with --sequence" $
       withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $
@@ -1112,16 +1122,18 @@
           ["⟦ Δ ⤍ 01- ⟧\n01-"]
 
     it "focuses a compressed sequence whose meet replaces a step root" $
-      withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $
-        testCLISucceeded
-          ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]
-          ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]
+      withAtoms $ \atoms ->
+        withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $
+          testCLISucceeded
+            ["dataize", atoms, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]
+            ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\leadsto_{\\nameref{r:contextualize}}"]
 
     it "compresses a canonized whole-expression sequence into a meet" $
-      withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $
-        testCLISucceeded
-          ["dataize", "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"]
-          ["\\phinoMeet{dataization:1}"]
+      withAtoms $ \atoms ->
+        withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $
+          testCLISucceeded
+            ["dataize", atoms, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"]
+            ["\\phinoMeet{dataization:1}"]
 
     it "dataizes with --locator" $
       withStdin "[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]" $
@@ -1133,38 +1145,42 @@
 
     describe "--evaluations" $ do
       it "writes one tab-separated record per fired atom" $
-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
-          hClose stream
-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
-            testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
-          records <- readUtf8 path
-          records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"
+        withAtoms $ \atoms ->
+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
+            hClose stream
+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
+              testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
+            records <- readUtf8 path
+            records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"
 
       it "writes a record for every firing" $
-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
-          hClose stream
-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $
-            testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
-          records <- readUtf8 path
-          lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11", "L_number_plus\t⟦ x ↦ 7 ⟧\t18"]
+        withAtoms $ \atoms ->
+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
+            hClose stream
+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $
+              testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
+            records <- readUtf8 path
+            lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11", "L_number_plus\t⟦ x ↦ 7 ⟧\t18"]
 
       it "writes records in canonical syntax without --sweet" $
-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
-          hClose stream
-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
-            testCLISucceeded ["dataize", "--evaluations=" ++ path, "--quiet", "--hide-rho"] []
-          records <- readUtf8 path
-          records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n"
+        withAtoms $ \atoms ->
+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
+            hClose stream
+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
+              testCLISucceeded ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--hide-rho"] []
+            records <- readUtf8 path
+            records `shouldEndWith` "\tΦ.number( as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-26-00-00-00-00-00-00 ⟧ ) )\n"
 
       it "keeps the records of a run that fails" $
-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
-          hClose stream
-          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $
-            testCLIFailed
-              ["dataize", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"]
-              ["Atom 'L_number_nope' does not exist"]
-          records <- readUtf8 path
-          records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"
+        withAtoms $ \atoms ->
+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
+            hClose stream
+            withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], nope -> [[ L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $
+              testCLIFailed
+                ["dataize", atoms, "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"]
+                ["Atom 'L_number_nope' does not exist"]
+            records <- readUtf8 path
+            records `shouldBe` "L_number_plus\t⟦ x ↦ 6 ⟧\t11\n"
 
       it "truncates the records left over from the previous run" $
         withTempFileContent "evaluationsXXXXXX.txt" "L_number_gt\t[[ ]]\t01-\n" $ \path -> do
@@ -1185,53 +1201,117 @@
             ["dataize", "--evaluations=evaluations.txt", "--output=latex"]
             ["The --evaluations option can stay together with --output=phi only"]
 
-    -- A placeholder formation ⟦ λ ⤍ Sym_arg_0 ⟧ standing in for a data input
-    -- names an atom phino cannot fire; the run used to die on it, discarding
-    -- what it had already evaluated (#1060)
+    -- A λ function the '--atoms' registry does not carry cannot fire — a
+    -- placeholder such as ⟦ λ ⤍ Sym_arg_0 ⟧ standing in for a data input, or
+    -- an operation the caller left out of its registry on purpose. The run used
+    -- to die on it, discarding what it had already evaluated (#1060)
     describe "--partial" $ do
-      let stuck = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]], times(x) -> [[ L> L_number_times ]] ]], @ -> 2.times(3).plus([[ L> Sym_arg_0 ]]) ]]"
+      let stuck = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]], nope -> [[ L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]"
       it "fails on an atom that cannot fire without the flag" $
-        withStdin stuck $
-          testCLIFailed ["dataize", "--sweet", "--hide-rho"] ["Atom 'Sym_arg_0' does not exist"]
+        withAtoms $ \atoms ->
+          withStdin stuck $
+            testCLIFailed ["dataize", atoms, "--sweet", "--hide-rho"] ["Atom 'L_number_nope' does not exist"]
 
       it "prints the residue with the stuck application intact and exits successfully" $
-        withStdin stuck $
-          testCLISucceeded
-            ["dataize", "--partial", "--sweet", "--hide-rho"]
-            ["⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧, λ ⤍ L_number_plus ⟧"]
+        withAtoms $ \atoms ->
+          withStdin stuck $
+            testCLISucceeded
+              ["dataize", atoms, "--partial", "--sweet", "--hide-rho"]
+              ["⟦ λ ⤍ L_number_nope ⟧"]
 
       it "keeps what was evaluated before the stuck site in the residue" $
-        withStdin stuck $
-          testCLISucceeded
-            ["dataize", "--partial", "--sweet"]
-            ["as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"]
+        withAtoms $ \atoms ->
+          withStdin stuck $
+            testCLISucceeded
+              ["dataize", atoms, "--partial", "--sweet"]
+              ["as-bytes ↦ Φ.bytes( data ↦ ⟦ Δ ⤍ 40-18-00-00-00-00-00-00 ⟧ )"]
 
       it "records every stuck site in --evaluations with no result" $
-        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
-          hClose stream
-          withStdin stuck $
-            testCLISucceeded ["dataize", "--partial", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
-          records <- readUtf8 path
-          lines records
-            `shouldBe` [ "L_number_times\t⟦ x ↦ 3 ⟧\t6"
-                       , "Sym_arg_0\t⟦⟧"
-                       , "L_number_plus\t⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧ ⟧"
-                       ]
+        withAtoms $ \atoms ->
+          withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
+            hClose stream
+            withStdin stuck $
+              testCLISucceeded ["dataize", atoms, "--partial", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
+            records <- readUtf8 path
+            lines records
+              `shouldBe` [ "L_number_times\t⟦ x ↦ 3 ⟧\t6"
+                         , "L_number_nope\t⟦⟧"
+                         ]
 
       it "still prints bytes when nothing gets stuck" $
-        withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
-          testCLISucceeded ["dataize", "--partial"] ["40-26-00-00-00-00-00-00"]
+        withAtoms $ \atoms ->
+          withStdin "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
+            testCLISucceeded ["dataize", atoms, "--partial"] ["40-26-00-00-00-00-00-00"]
 
       it "prints the chain of steps ending in the residue with --sequence" $
-        withStdin stuck $
-          testCLISucceeded
-            ["dataize", "--partial", "--sequence", "--sweet", "--hide-rho", "--flat"]
-            ["2.times( 3 ).plus( ⟦ λ ⤍ Sym_arg_0 ⟧ )", "⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧, λ ⤍ L_number_plus ⟧"]
+        withAtoms $ \atoms ->
+          withStdin stuck $
+            testCLISucceeded
+              ["dataize", atoms, "--partial", "--sequence", "--sweet", "--hide-rho", "--flat"]
+              ["2.times( 3 ).nope", "⟦ λ ⤍ L_number_nope ⟧"]
 
       it "still stops on the terminator ⊥, since a wrong operand is not a stuck atom" $
         withStdin "[[ ]]" $
           testCLIFailed ["dataize", "--partial"] ["terminator ⊥"]
 
+    -- Which λ functions exist is not phino's business any more: the registry
+    -- given with '--atoms' decides, and phino carries none of its own
+    describe "--atoms" $ do
+      let sum' = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
+      it "fires the λ function the registry carries" $
+        withAtoms $ \atoms ->
+          withStdin sum' $
+            testCLISucceeded ["dataize", atoms] ["40-26-00-00-00-00-00-00"]
+
+      it "gets stuck on every atom when it is not given" $
+        withStdin sum' $
+          testCLIFailed ["dataize"] ["Atom 'L_number_plus' does not exist"]
+
+      it "fails when the registry file is not there" $
+        withStdin sum' $
+          testCLIFailed ["dataize", "--atoms=no-such-registry.json"] ["no-such-registry.json"]
+
+      -- An unknown runtime is refused where the registry is read, which is
+      -- before the input is even parsed, rather than when an atom of it fires
+      it "fails on a runtime phino cannot run, before dataizing anything" $
+        withTempFileContent "atomsXXXXXX.json" "{\"L_number_plus\": {\"rt\": \"ruby\", \"script\": \"puts 1\"}}" $ \path ->
+          withStdin sum' $
+            testCLIFailed ["dataize", "--atoms=" ++ path] ["unknown runtime 'ruby'"]
+
+      it "fails on a registry that is not JSON" $
+        withTempFileContent "atomsXXXXXX.json" "L_number_plus: js" $ \path ->
+          withStdin sum' $
+            testCLIFailed ["dataize", "--atoms=" ++ path] ["cannot be read"]
+
+    -- An atom script cannot reduce the operands it was handed by itself, so it
+    -- asks phino for them: '--inside' binds an expression to a synthetic
+    -- attribute of the universe and aims the run at it
+    describe "--inside" $ do
+      let universe = "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]"
+      it "dataizes an expression the input does not contain" $
+        withAtoms $ \atoms ->
+          withStdin universe $
+            testCLISucceeded ["dataize", atoms, "--inside=5.plus( 6 )"] ["40-26-00-00-00-00-00-00"]
+
+      -- The expression is normalized first, so a dispatch off a formation — the
+      -- very shape a script asks about, '⟦ x ↦ 6, ρ ↦ 5 ⟧.x' — reduces too
+      it "normalizes what it is handed before dataizing it" $
+        withStdin universe $
+          testCLISucceeded ["dataize", "--inside=[[ x -> [[ D> 2A- ]] ]].x"] ["2A-"]
+
+      it "morphs inside the universe just as it dataizes inside it" $
+        withAtoms $ \atoms ->
+          withStdin universe $
+            testCLISucceeded ["morph", atoms, "--inside=5.plus( 6 )", "--sweet", "--hide-rho", "--flat"] ["⟦ x ↦ 6, λ ⤍ L_number_plus ⟧"]
+
+      it "cannot be used together with --locator" $
+        withStdin universe $
+          testCLIFailed ["dataize", "--inside=Q.@", "--locator=Q.@"] ["--inside and --locator cannot be used together"]
+
+      it "fails when the input expression is not a formation" $
+        withStdin "Q.x" $
+          testCLIFailed ["dataize", "--inside=Q.x"] ["--inside requires the input expression to be a formation"]
+
     describe "fails" $ do
       it "with --output != latex and --nonumber" $
         withStdin "" $
@@ -1307,15 +1387,17 @@
         testCLISucceeded ["morph", "--flat", "--hide-rho"] ["⟦ Δ ⤍ 01- ⟧"]
 
     it "stops at the bare saturated λ-formation" $
-      withStdin chained $
-        testCLISucceeded
-          ["morph", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]
-          ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]
+      withAtoms $ \atoms ->
+        withStdin chained $
+          testCLISucceeded
+            ["morph", atoms, "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]
+            ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]
 
     -- The same term under 𝔻, which insists on bytes and fires what 𝕄 left bare
     it "leaves to dataize the firing that takes the same term to bytes" $
-      withStdin chained $
-        testCLISucceeded ["dataize"] ["40-32-00-00-00-00-00-00"]
+      withAtoms $ \atoms ->
+        withStdin chained $
+          testCLISucceeded ["dataize", atoms] ["40-32-00-00-00-00-00-00"]
 
     -- 'mf' hands a formation back as it is, so '--locator' is how one aims 𝕄 at
     -- a subterm worth navigating: here it resolves Φ against the universe and
@@ -1340,37 +1422,40 @@
     -- design — it happens in a side premise, which reduces on a chain of its
     -- own and discards it
     it "prints the chain of morphing steps with --sequence" $
-      withStdin chained $
-        testCLISucceeded
-          ["morph", "--locator=Q.@", "--sequence", "--headers", "--sweet", "--hide-rho", "--flat"]
-          [ "Rule 'maa'"
-          , "Rule 'alpha'"
-          , "Rule 'copy'"
-          , "Rule 'mf'"
-          , "⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"
-          ]
+      withAtoms $ \atoms ->
+        withStdin chained $
+          testCLISucceeded
+            ["morph", atoms, "--locator=Q.@", "--sequence", "--headers", "--sweet", "--hide-rho", "--flat"]
+            [ "Rule 'maa'"
+            , "Rule 'alpha'"
+            , "Rule 'copy'"
+            , "Rule 'mf'"
+            , "⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"
+            ]
 
     it "does not print the result with --quiet" $
       withStdin "[[ D> 01- ]]" $
         testCLISucceeded ["morph", "--quiet"] []
 
     it "records the atoms it fires with --evaluations" $
-      withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
-        hClose stream
-        withStdin chained $
-          testCLISucceeded ["morph", "--locator=Q.@", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
-        records <- readUtf8 path
-        lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11"]
+      withAtoms $ \atoms ->
+        withTempFile "evaluationsXXXXXX.txt" $ \(path, stream) -> do
+          hClose stream
+          withStdin chained $
+            testCLISucceeded ["morph", atoms, "--locator=Q.@", "--evaluations=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
+          records <- readUtf8 path
+          lines records `shouldBe` ["L_number_plus\t⟦ x ↦ 6 ⟧\t11"]
 
     it "saves morphing steps to dir with --steps-dir" $
-      withTempDirectory "phino-steps-morph" $ \dir ->
-        withStdin chained $ do
-          testCLISucceeded
-            ["morph", "--locator=Q.@", "--steps-dir=" ++ dir, "--sweet", "--hide-rho", "--flat"]
-            ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]
-          steps <- sort <$> listDirectory dir
-          steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]
-          length steps `shouldSatisfy` (> 0)
+      withAtoms $ \atoms ->
+        withTempDirectory "phino-steps-morph" $ \dir ->
+          withStdin chained $ do
+            testCLISucceeded
+              ["morph", atoms, "--locator=Q.@", "--steps-dir=" ++ dir, "--sweet", "--hide-rho", "--flat"]
+              ["⟦ x ↦ 7, λ ⤍ L_number_plus ⟧"]
+            steps <- sort <$> listDirectory dir
+            steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]
+            length steps `shouldSatisfy` (> 0)
 
     it "accepts --seed, --shuffle and --depth-sensitive" $
       withStdin "[[ D> 01- ]]" $
@@ -1442,8 +1527,8 @@
         ["explain", "--rule=resources/normalize/copy.yaml"]
         [ unlines
             [ "\\phinoNormalizationRule{copy}"
-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
-            , "  { [[ B_1, \\tau -> k, B_2 ]] }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> k_1 ) }"
+            , "  { [[ B_1, \\tau_1 -> k_1, B_2 ]] }"
             , "  { }"
             , "  { }"
             ]
@@ -1454,8 +1539,8 @@
         ["explain", "--rule=test-resources/cli/labeled.yaml"]
         [ unlines
             [ "\\phinoNormalizationRule[\\lambda]{copy}"
-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
-            , "  { [[ B_1, \\tau -> k, B_2 ]] }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> k_1 ) }"
+            , "  { [[ B_1, \\tau_1 -> k_1, B_2 ]] }"
             , "  { }"
             , "  { }"
             ]
@@ -1488,18 +1573,18 @@
         ["explain", "--normalize"]
         [ unlines
             [ "\\phinoNormalizationRule{alpha}"
-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"
-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"
-            , "  { i = \\vert \\overline{ B_1 } \\vert }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i1}} -> e_1 ) }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e_1 ) }"
+            , "  { i_1 = \\vert \\overline{ B_1 } \\vert }"
             , "  { }"
             , "\\phinoNormalizationRule{amiss}"
-            , "  { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"
+            , "  { [[ B_1 ]] ( \\phiTerminal{\\alpha_{i1}} -> e ) }"
             , "  { T }"
-            , "  { \\vert \\overline{ B } \\vert \\leq i }"
+            , "  { \\vert \\overline{ B_1 } \\vert \\leq i_1 }"
             , "  { }"
             , "\\phinoNormalizationRule{copy}"
-            , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
-            , "  { [[ B_1, \\tau -> k, B_2 ]] }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> k_1 ) }"
+            , "  { [[ B_1, \\tau_1 -> k_1, B_2 ]] }"
             , "  { }"
             , "  { }"
             , "\\phinoNormalizationRule{dc}"
@@ -1523,29 +1608,29 @@
             , "  { D \\in B_1 \\;\\text{or}\\; D \\in B_2 }"
             , "  { }"
             , "\\phinoNormalizationRule{dot}"
-            , "  { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"
-            , "  { e ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }"
+            , "  { [[ B_1, \\tau_1 -> n_1, B_2 ]] . \\tau_1 }"
+            , "  { e_1 ( \\phiTerminal{\\rho} -> [[ B_1, \\tau_1 -> n_1, B_2 ]] ) }"
             , "  { }"
-            , "  { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e } }"
+            , "  { \\phinoContextualize{ n_1 }{ [[ B_1, B_2 ]] }{ e_1 } }"
             , "\\phinoNormalizationRule{miss}"
-            , "  { [[ B ]] ( \\tau -> e ) }"
+            , "  { [[ B_1 ]] ( \\tau_1 -> e ) }"
             , "  { T }"
-            , "  { \\tau \\notin B }"
+            , "  { \\tau_1 \\notin B_1 }"
             , "  { }"
             , "\\phinoNormalizationRule{null}"
-            , "  { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"
+            , "  { [[ B_1, \\tau_1 -> ?, B_2 ]] . \\tau_1 }"
             , "  { T }"
             , "  { }"
             , "  { }"
             , "\\phinoNormalizationRule{over}"
-            , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"
+            , "  { [[ B_1, \\tau_1 -> e_1, B_2 ]] ( \\tau_1 -> e_2 ) }"
             , "  { T }"
-            , "  { \\tau \\not= \\phiTerminal{\\rho} }"
+            , "  { \\tau_1 \\not= \\phiTerminal{\\rho} }"
             , "  { }"
             , "\\phinoNormalizationRule{overa}"
-            , "  { [[ B_1, \\tau -> e_1, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e_2 ) }"
+            , "  { [[ B_1, \\tau_1 -> e_1, B_2 ]] ( \\phiTerminal{\\alpha_{i1}} -> e_2 ) }"
             , "  { T }"
-            , "  { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }"
+            , "  { i_1 = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau_1 \\not= \\phiTerminal{\\rho} }"
             , "  { }"
             , "\\phinoNormalizationRule{stay}"
             , "  { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }"
@@ -1553,9 +1638,9 @@
             , "  { }"
             , "  { }"
             , "\\phinoNormalizationRule{stop}"
-            , "  { [[ B ]] . \\tau }"
+            , "  { [[ B_1 ]] . \\tau_1 }"
             , "  { T }"
-            , "  { \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B }"
+            , "  { \\tau_1 \\notin B_1 \\;\\text{and}\\; @ \\notin B_1 \\;\\text{and}\\; L \\notin B_1 }"
             , "  { }"
             ]
         ]
@@ -1566,79 +1651,79 @@
         [ unlines
             [ "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mf}"
-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s }{ [[ B ]] }{ s } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] }{ e_0 }{ s }{ [[ B_0 ]] }{ s } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{ml}"
             , "  \\phinoLabel{\\lambda}"
-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"
+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F_0, B_2 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mphi}"
             , "  \\phinoLabel{\\varphi}"
-            , "  \\phinoCondition{ @ \\in B \\;\\text{and}\\; \\tau \\notin B \\;\\text{and}\\; L \\notin B }"
-            , "  \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] . \\tau }{ e }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoCondition{ @ \\in B_0 \\;\\text{and}\\; \\tau_0 \\notin B_0 \\;\\text{and}\\; L \\notin B_0 }"
+            , "  \\phinoPremise{ \\phinoNormalize{ [[ B_0 ]] . @ . \\tau_0 }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_0 ]] . \\tau_0 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{md}"
-            , "  \\phinoCondition{ \\phinoNotFormation{ n } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"
+            , "  \\phinoCondition{ \\phinoNotFormation{ n_0 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau_0 }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n_0 . \\tau_0 }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{ma}"
-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> k_1 ) }{ n_2 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> k_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau_0 -> k_1 ) }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n_0 ( \\tau_0 -> k_1 ) }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{maa}"
-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> k_1 ) }{ n_2 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> k_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> k_1 ) }{ n_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e_0 }{ s_2 }{ n_3 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> k_1 ) }{ e_0 }{ s_1 }{ n_3 }{ s_3 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mad}"
             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{maad}"
             , "  \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"
-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{universe}"
             , "  \\phinoLabel{\\Phi}"
-            , "  \\phinoCondition{ e \\not= Q }"
-            , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"
-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoCondition{ e_0 \\not= Q }"
+            , "  \\phinoPremise{ \\phinoNormalize{ e_0 }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e_0 }{ s_1 }{ n_2 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{dead}"
-            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s }{ T }{ s } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e_0 }{ s }{ T }{ s } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{xi}"
-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ n }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
             , "  \\phinoName{mg}"
-            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n_1 }{ s_2 } }"
             , "\\end{phinoMorphingInference}"
             ]
         ]
@@ -1650,34 +1735,34 @@
             [ "\\begin{phinoDataizationInference}"
             , "  \\phinoName{delta}"
             , "  \\phinoLabel{\\Delta}"
-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s }{ \\delta }{ s } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta_0, B_2 ]] }{ e_0 }{ s }{ \\delta_0 }{ s } }"
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{box}"
             , "  \\phinoCondition{ [ D \\char44{} L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }"
             , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ e_2 } }"
             , "  \\phinoPremise{ \\phinoNormalize{ e_2 }{ n_1 } }"
-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\delta }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{fire}"
-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }"
+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_2 }{ \\delta_0 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F_0, B_2 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_3 } }"
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{none}"
-            , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"
-            , "  \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"
-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"
+            , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B_0 = \\emptyset }"
+            , "  \\phinoPremise{ \\phinoDataize{ T }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_0 ]] }{ e_0 }{ s_1 }{ \\delta_0 }{ s_2 } }"
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{norm}"
-            , "  \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }"
-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"
-            , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ s_1 }{ \\delta }{ s_3 } }"
+            , "  \\phinoCondition{ \\phinoNotFormation{ n_0 } \\;\\text{and}\\; n_0 \\not= T }"
+            , "  \\phinoPremise{ \\phinoMorph{ n_0 }{ e_0 }{ s_1 }{ n_1 }{ s_2 } }"
+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e_0 }{ s_2 }{ \\delta_0 }{ s_3 } }"
+            , "  \\phinoConclusion{ \\phinoDataize{ n_0 }{ e_0 }{ s_1 }{ \\delta_0 }{ s_3 } }"
             , "\\end{phinoDataizationInference}"
             ]
         ]
@@ -1688,36 +1773,36 @@
         [ unlines
             [ "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{cg}"
-            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k }{ Q } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k_0 }{ Q } }"
             , "\\end{phinoContextualizationInference}"
             , "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{cxi}"
-            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k }{ k } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k_0 }{ k_0 } }"
             , "\\end{phinoContextualizationInference}"
             , "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{ct}"
-            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k }{ T } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k_0 }{ T } }"
             , "\\end{phinoContextualizationInference}"
             , "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{cf}"
-            , "  \\phinoConclusion{ \\phinoContextualize{ [[ B ]] }{ k }{ [[ B ]] } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ [[ B_0 ]] }{ k_0 }{ [[ B_0 ]] } }"
             , "\\end{phinoContextualizationInference}"
             , "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{cd}"
-            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"
-            , "  \\phinoConclusion{ \\phinoContextualize{ n . \\tau }{ k }{ n_1 . \\tau } }"
+            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 . \\tau_0 }{ k_0 }{ n_1 . \\tau_0 } }"
             , "\\end{phinoContextualizationInference}"
             , "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{ca}"
-            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"
-            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k }{ n_2 } }"
-            , "  \\phinoConclusion{ \\phinoContextualize{ n ( \\tau -> e_1 ) }{ k }{ n_1 ( \\tau -> n_2 ) } }"
+            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\tau_0 -> e_1 ) }{ k_0 }{ n_1 ( \\tau_0 -> n_2 ) } }"
             , "\\end{phinoContextualizationInference}"
             , "\\begin{phinoContextualizationInference}"
             , "  \\phinoName{caa}"
-            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"
-            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k }{ n_2 } }"
-            , "  \\phinoConclusion{ \\phinoContextualize{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ k }{ n_1 ( \\phiTerminal{\\alpha_{i}} -> n_2 ) } }"
+            , "  \\phinoPremise{ \\phinoContextualize{ n_0 }{ k_0 }{ n_1 } }"
+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k_0 }{ n_2 } }"
+            , "  \\phinoConclusion{ \\phinoContextualize{ n_0 ( \\phiTerminal{\\alpha_{i0}} -> e_1 ) }{ k_0 }{ n_1 ( \\phiTerminal{\\alpha_{i0}} -> n_2 ) } }"
             , "\\end{phinoContextualizationInference}"
             ]
         ]
@@ -1838,13 +1923,19 @@
     it "builds substitutions with conditions" $
       withStdin "[[ x -> Q.y ]].x" $
         testCLISucceeded
-          ["match", "--pattern=[[ !t -> Q.y, !B ]].!t", "--when=eq(length(!B),1)"]
-          ["B >> ⟦ ρ ↦ ∅ ⟧\nt >> x"]
+          ["match", "--pattern=[[ !t1 -> Q.y, !B1 ]].!t1", "--when=eq(length(!B1),1)"]
+          ["B1 >> ⟦ ρ ↦ ∅ ⟧\nt1 >> x"]
 
     it "builds with condition from file" $
       testCLISucceeded
-        ["match", "--pattern=[[ !B ]]", "--when=eq(length(!B),2)", "test-resources/cli/foo.phi"]
-        ["B >> ⟦ foo ↦ Φ.org.eolang.x, ρ ↦ ∅ ⟧"]
+        ["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),2)", "test-resources/cli/foo.phi"]
+        ["B1 >> ⟦ foo ↦ Φ.org.eolang.x, ρ ↦ ∅ ⟧"]
+
+    it "rejects an anonymous meta in --when" $
+      withStdin "[[ x -> Q.y ]]" $
+        testCLIFailed
+          ["match", "--pattern=[[ !B ]]", "--when=eq(length(!B),1)"]
+          ["[ERROR]: Anonymous meta '!B' cannot be referenced in --when"]
 
     it "fails on parsing --when condition" $
       withStdin "[[]]" $
diff --git a/test/ConditionSpec.hs b/test/ConditionSpec.hs
--- a/test/ConditionSpec.hs
+++ b/test/ConditionSpec.hs
@@ -27,22 +27,22 @@
       , "absolute(!e1)"
       , "matches(\"hello(\\\"\\u0000)\", !e)"
       , "part-of ( [[ x -> 1 ]] , !B ) "
-      , "not(formation(!n))"
+      , "not(formation(!n1))"
       ]
       (\expr -> it expr (parseCondition expr `shouldSatisfy` isRight))
 
   describe "parses correctly" $
     forM_
-      [ ("in(!t, !B)", Y.In (AtMeta "t") (BiMeta "B"))
-      , ("not(in(!t,!B))", Y.Not (Y.In (AtMeta "t") (BiMeta "B")))
+      [ ("in(!t1, !B1)", Y.In (AtMeta "t1") (BiMeta "B1"))
+      , ("not(in(!t1,!B1))", Y.Not (Y.In (AtMeta "t1") (BiMeta "B1")))
       , ("eq(1,-2)", Y.Eq (Y.CmpNum (Y.Literal 1)) (Y.CmpNum (Y.Literal (-2))))
-      , ("eq(!i,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i")) (Y.CmpNum (Y.Length (BiMeta "B1"))))
+      , ("eq(!i1,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i1")) (Y.CmpNum (Y.Length (BiMeta "B1"))))
       , ("eq(!i2,domain(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i2")) (Y.CmpNum (Y.Domain (BiMeta "B1"))))
-      , ("gt(domain(!B1),!i)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i")))
+      , ("gt(domain(!B1),!i1)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i1")))
       , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2")))
       , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])
-      , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])
-      , ("not(formation(!n))", Y.Not (Y.IsFormation (ExMeta "n")))
+      , ("and(matches(\"hi\", !e1),part-of(!e1, !B1))", Y.And [Y.Matches "hi" (ExMeta "e1"), Y.PartOf (ExMeta "e1") (BiMeta "B1")])
+      , ("not(formation(!n1))", Y.Not (Y.IsFormation (ExMeta "n1")))
       ]
       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res))
 
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -7,14 +7,16 @@
 module DataizeSpec (spec) where
 
 import AST
+import Atoms (Registry, emptyRegistry)
 import Control.Exception (SomeException)
 import Control.Monad
 import Data.IORef (modifyIORef', newIORef, readIORef)
 import Data.List (find, isInfixOf, nub)
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Maybe (fromMaybe, isJust)
-import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, morph, morph')
+import Dataize (DataizeContext (..), Outcome (..), Steps (..), dataize, dataize', emptyState, execBuildTerm, insideUniverse, morph, morph')
 import Deps (Evaluation (..), Term (TeExpression), dontSaveEval, dontSaveStep)
+import Fixtures (fixtureRegistry, withNode)
 import Functions (buildTerm)
 import Matcher (substEmpty)
 import Parser (parseExpressionThrows)
@@ -26,10 +28,16 @@
 
 -- Shuffle is enabled so the suite exercises the order-independence of the
 -- dataization rules (#909): a hidden overlap surfaces as a nondeterministic
--- failure instead of staying silently green.
+-- failure instead of staying silently green. The registry of λ functions is
+-- empty, since phino implements none of them: a case that needs an atom to
+-- answer brings the fixture registry in through 'withAtoms'.
 defaultDataizeContext :: Expression -> DataizeContext
-defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False buildTerm dontSaveStep dontSaveEval
+defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval
 
+-- The same context with the fixture λ functions registered (see 'Fixtures').
+withAtoms :: Registry -> DataizeContext -> DataizeContext
+withAtoms registry ctx = ctx{_atoms = registry}
+
 test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> String -> DataizeContext -> IO ((a, [Rewritten]), String)) -> [(String, Expression, Expression, a)] -> Spec
 test func useCases =
   forM_ useCases $ \(desc, input, expr, output) ->
@@ -63,18 +71,18 @@
       (morphed, _) <- morph expr (defaultDataizeContext loc')
       morphed `shouldBe` expected
 
--- The 12 primitive λ-atoms every EO data operation reduces to, declared the way
--- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell the
--- The 12 primitive λ-atoms every EO data operation reduces to, declared the way
--- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell the
--- expression under φ. 'number.eq' is the one operation with no atom of its own:
--- EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the same
--- way. Alongside them stand the objects the atoms hand results to: 'string'
--- carries the 'cant-slice' complaint, while 'true' and 'false' fill in for the
--- real bool objects, since the single byte an EO bool dataizes to is all these
--- cases assert. Those bytes are EO's own: 'true.eo' asserts
+-- The EO objects the fixture λ functions answer for, declared the way
+-- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell
+-- the expression under φ. 'number.eq' is the one operation with no atom of its
+-- own: EO spells it out of 'L_bytes_eq' (eq.eo), so the fixture composes it the
+-- same way. Alongside them stand the objects the atoms hand results to: 'string'
+-- carries what a byte-array complaint would say, while 'true' and 'false' fill
+-- in for the real bool objects, since the single byte an EO bool dataizes to is
+-- all these cases assert. Those bytes are EO's own: 'true.eo' asserts
 -- 'true.as-bytes.eq FF-' and 'bool.eo' branches 'if' over 'FF-' and '00-', so a
 -- universe copied from here starts with a bool an EO program recognizes.
+-- 'number.nope' is declared and left out of the registry on purpose: it is the
+-- λ function that cannot fire, the one '--partial' parks on.
 primitives :: String -> String
 primitives src =
   unlines
@@ -82,14 +90,8 @@
     , "  bytes -> [["
     , "    data -> ?,"
     , "    @ -> $.data,"
-    , "    and -> [[ b -> ?, L> L_bytes_and ]],"
-    , "    or -> [[ b -> ?, L> L_bytes_or ]],"
     , "    not -> [[ L> L_bytes_not ]],"
-    , "    concat -> [[ b -> ?, L> L_bytes_concat ]],"
-    , "    eq -> [[ b -> ?, L> L_bytes_eq ]],"
-    , "    size -> [[ L> L_bytes_size ]],"
-    , "    right -> [[ x -> ?, L> L_bytes_right ]],"
-    , "    slice -> [[ start -> ?, len -> ?, cant-slice -> ?, L> L_bytes_slice ]]"
+    , "    eq -> [[ b -> ?, L> L_bytes_eq ]]"
     , "  ]],"
     , "  number -> [["
     , "    as-bytes -> ?,"
@@ -98,7 +100,8 @@
     , "    times -> [[ x -> ?, L> L_number_times ]],"
     , "    div -> [[ x -> ?, L> L_number_div ]],"
     , "    gt -> [[ x -> ?, L> L_number_gt ]],"
-    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]"
+    , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]],"
+    , "    nope -> [[ L> L_number_nope ]]"
     , "  ]],"
     , "  string -> [[ as-bytes -> ?, @ -> $.as-bytes ]],"
     , "  true -> [[ @ -> [[ D> FF- ]] ]],"
@@ -111,38 +114,51 @@
 raw :: String -> String
 raw bts = "Q.bytes( data -> [[ D> " ++ bts ++ " ]] )"
 
-testAtom :: [(String, String, Bytes)] -> Spec
-testAtom useCases =
+-- Dataize an expression against the fixture universe, with the fixture λ
+-- functions registered. Every such case runs an external script, so it is
+-- pending where 'node' is not installed.
+testAtom :: Registry -> [(String, String, Bytes)] -> Spec
+testAtom registry useCases =
   forM_ useCases $ \(name, src, res) ->
-    it name $ do
-      expr <- parseExpressionThrows (primitives src)
-      loc <- parseExpressionThrows "Q"
-      (value, _) <- dataize expr (defaultDataizeContext loc)
-      value `shouldBe` Dataized res
+    it name $
+      withNode $ do
+        expr <- parseExpressionThrows (primitives src)
+        loc <- parseExpressionThrows "Q"
+        (value, _) <- dataize expr (withAtoms registry (defaultDataizeContext loc))
+        value `shouldBe` Dataized res
 
 -- Dataize under '--partial', collecting every report 𝔼 makes on the way, in
 -- the order it makes them
-partially :: String -> IO ((Outcome, [Rewritten]), [Evaluation])
-partially src = do
+partially :: Registry -> String -> IO ((Outcome, [Rewritten]), [Evaluation])
+partially registry src = do
   expr <- parseExpressionThrows (primitives src)
   reports <- newIORef []
-  let ctx = (defaultDataizeContext ExRoot){_partial = True, _saveEval = \report -> modifyIORef' reports (report :)}
+  let ctx =
+        (withAtoms registry (defaultDataizeContext ExRoot))
+          { _partial = True
+          , _saveEval = \report -> modifyIORef' reports (report :)
+          }
   result <- dataize expr ctx
   collected <- readIORef reports
   pure (result, reverse collected)
 
 -- An atom with no answer yields ⊥, which stops the whole dataization
-testStuckAtom :: [(String, String)] -> Spec
-testStuckAtom useCases =
+testStuckAtom :: Registry -> [(String, String)] -> Spec
+testStuckAtom registry useCases =
   forM_ useCases $ \(name, src) ->
-    it name $ do
-      expr <- parseExpressionThrows (primitives src)
-      loc <- parseExpressionThrows "Q"
-      dataize expr (defaultDataizeContext loc)
-        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
+    it name $
+      withNode $ do
+        expr <- parseExpressionThrows (primitives src)
+        loc <- parseExpressionThrows "Q"
+        dataize expr (withAtoms registry (defaultDataizeContext loc))
+          `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
 
 spec :: Spec
 spec = do
+  -- Every λ function a case may fire comes from the fixture registry, read
+  -- once here: phino carries none of its own (see 'Fixtures').
+  registry <- runIO fixtureRegistry
+
   -- The top-level 𝕄 entry point, the one the 'morph' command runs: it locates
   -- the subterm, threads the whole input expression as the universe and hands
   -- back the morphed expression together with the chain that led to it (#1114).
@@ -253,7 +269,7 @@
   -- 'execBuildTerm', the same way the matcher would call it.
   describe "execBuildTerm 'evaluate'" $ do
     let univ = ExFormation []
-        ctx = defaultDataizeContext ExRoot
+        ctx = withAtoms registry (defaultDataizeContext ExRoot)
         runEvaluate args = execBuildTerm univ ctx "evaluate" args substEmpty
     forM_
       [
@@ -281,12 +297,13 @@
           it ("throws when " ++ desc) $
             runEvaluate args `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))
       )
-    it "evaluates a λ-bearing formation to the atom's normalized result" $ do
-      let form = ExFormation [BiLambda (Function "L_bytes_not"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])]
-      result <- runEvaluate [ArgExpression form, ArgExpression univ]
-      case result of
-        TeExpression expr -> expr `shouldBe` dataBytes (BtOne "FF")
-        _ -> expectationFailure "expected TeExpression"
+    it "evaluates a λ-bearing formation to the atom's normalized result" $
+      withNode $ do
+        let form = ExFormation [BiLambda (Function "L_bytes_not"), BiTau AtRho (ExFormation [BiDelta (BtOne "00")])]
+        result <- runEvaluate [ArgExpression form, ArgExpression univ]
+        case result of
+          TeExpression expr -> expr `shouldBe` dataBytes (BtOne "FF")
+          _ -> expectationFailure "expected TeExpression"
 
   describe "execBuildTerm 'morph'" $ do
     let univ = ExFormation []
@@ -300,18 +317,32 @@
         TeExpression expr -> expr `shouldBe` ExFormation [BiDelta (BtOne "00")]
         _ -> expectationFailure "expected TeExpression"
 
-  -- Every atom's operand is fetched through the synthetic '_dataize', which
-  -- rebuilds the universe as a formation to bind the operand into before
-  -- reducing it. A universe that is not itself a formation can never arise
-  -- from the public 'dataize' entry point (its own universe argument doubles
-  -- as the located root of a real program, always a formation), but 'dataize''
-  -- lets a test drive an atom-bearing term against one directly, proving the
-  -- guard fires instead of the atom looping or crashing some other way.
-  describe "atoms refuse to run under a non-formation universe" $
-    it "fails fast instead of dispatching against a non-formation universe" $ do
-      let form = ExFormation [BiLambda (Function "L_bytes_not"), BiVoid AtRho]
-      dataize' (form, (ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)
-        `shouldThrow` (\e -> "non-formation universe" `isInfixOf` show (e :: SomeException))
+  -- An expression that is not part of the program — the operand an atom script
+  -- asks phino to reduce — is bound to a synthetic attribute of the universe and
+  -- that attribute is what 𝔻 is aimed at. This is what the '--inside' option
+  -- runs, and what phino did internally while the atoms still lived in the
+  -- binary.
+  describe "insideUniverse" $ do
+    let universe = "[[ y -> [[ D> 02- ]] ]]"
+        reduced src = do
+          univ <- parseExpressionThrows universe
+          target <- parseExpressionThrows src
+          (extended, ctx) <- insideUniverse target univ (defaultDataizeContext ExRoot)
+          fst <$> dataize extended ctx
+    it "reduces an expression the program does not contain" $ do
+      value <- reduced "Q.y"
+      value `shouldBe` Dataized (BtOne "02")
+    -- 𝔻 accepts normal forms only, and a dispatch off a formation is not one:
+    -- 'dot' still applies to it. So the expression is normalized first, which
+    -- is the whole reason an atom script cannot simply splice it into the
+    -- universe itself.
+    it "normalizes what it is handed before 𝔻 sees it" $ do
+      value <- reduced "[[ x -> [[ D> 01- ]] ]].x"
+      value `shouldBe` Dataized (BtOne "01")
+    it "refuses a universe which is not a formation" $ do
+      target <- parseExpressionThrows "Q.y"
+      insideUniverse target ExRoot (defaultDataizeContext ExRoot)
+        `shouldThrow` (\e -> "not a formation" `isInfixOf` show (e :: SomeException))
 
   -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph'' walks the
   -- morphing rules in a random order on every step. Every clause is
@@ -453,76 +484,79 @@
   -- stop it (#1052). '--max-steps' bounds that recursion and fails once the
   -- budget is gone.
   describe "stops a dataization that never reaches bytes" $
-    it "fails on the step limit instead of morphing forever" $ do
-      expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧"
-      dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False buildTerm dontSaveStep dontSaveEval)
-        `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))
+    it "fails on the step limit instead of morphing forever" $
+      withNode $ do
+        expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧"
+        dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False registry buildTerm dontSaveStep dontSaveEval)
+          `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException))
 
-  -- An atom phino does not know — a placeholder such as ⟦ λ ⤍ Sym_arg_0 ⟧
-  -- standing in for a data input (#1060) — fails the run, and so does a known
-  -- atom whose input reaches one. Under '_partial' the run ends on the residue
+  -- An atom phino does not know — a name the '--atoms' registry does not carry,
+  -- such as the placeholder ⟦ λ ⤍ Sym_arg_0 ⟧ standing in for a data input
+  -- (#1060) — fails the run. Under '_partial' the run ends on the residue
   -- instead: the working expression the spine had reached, with the stuck
   -- application intact and everything the calculus demanded before it already
-  -- evaluated, while 𝔼 reports each parked site with no result.
+  -- evaluated, while 𝔼 reports each parked site with no result. Since the atoms
+  -- moved out of the binary, an operand that cannot be reduced is the script's
+  -- own business, so what parks here is the unregistered λ function alone.
   describe "partially evaluates around an atom that cannot fire (--partial)" $ do
     -- the parser gives every formation its void ρ
     let placeholder = ExFormation [BiLambda (Function "Sym_arg_0"), BiVoid AtRho]
-    it "fails on it without the flag, naming the unknown atom" $ do
-      expr <- parseExpressionThrows (primitives "2.times(3).plus([[ L> Sym_arg_0 ]])")
-      dataize expr (defaultDataizeContext ExRoot)
-        `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException))
-    it "leaves the saturated application of the known atom in place, the placeholder inside it" $ do
-      ((outcome, _), _) <- partially "2.times(3).plus([[ L> Sym_arg_0 ]])"
-      case outcome of
-        Residual (ExFormation bds) -> do
-          bds `shouldContain` [BiLambda (Function "L_number_plus")]
-          bds `shouldContain` [BiTau (AtLabel "x") placeholder]
-        other -> expectationFailure ("expected a residual formation, got " ++ show other)
-    it "keeps what was evaluated before the stuck site in the residue" $ do
-      ((outcome, _), _) <- partially "2.times(3).plus([[ L> Sym_arg_0 ]])"
-      case outcome of
-        Residual (ExFormation bds) -> do
-          let rho = [value | BiTau AtRho value <- bds]
-          length rho `shouldBe` 1
-          -- 2 × 3 = 6.0, whose IEEE 754 bytes are 40-18-00-00-00-00-00-00
-          show rho `shouldContain` show (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])
-          -- the times application is gone: ρ is the number it produced, its 'as-bytes' bound
-          [() | ExFormation inner <- rho, BiTau (AtLabel "as-bytes") _ <- inner] `shouldBe` [()]
-        other -> expectationFailure ("expected a residual formation, got " ++ show other)
-    it "reports the firing that succeeded with its result and every stuck site without one" $ do
-      (_, reports) <- partially "2.times(3).plus([[ L> Sym_arg_0 ]])"
-      map (._function) reports `shouldBe` ["L_number_times", "Sym_arg_0", "L_number_plus"]
-      map (isJust . (._result)) reports `shouldBe` [True, False, False]
-    it "leaves an unknown atom dataized directly as the whole residue" $ do
-      ((outcome, chain), reports) <- partially "[[ L> Sym_arg_0 ]]"
-      outcome `shouldBe` Residual placeholder
-      map (._function) reports `shouldBe` ["Sym_arg_0"]
-      map fst chain `shouldEndWith` [placeholder]
-    it "still reaches bytes when nothing is stuck" $ do
-      ((outcome, _), reports) <- partially "2.times(3)"
-      outcome `shouldBe` Dataized (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])
-      map (._function) reports `shouldBe` ["L_number_times"]
-    it "stops on the terminator ⊥ as before, since a wrong operand is not a stuck atom" $ do
-      expr <- parseExpressionThrows (primitives (raw "20-1F" ++ ".and( " ++ raw "CA-FE-BE" ++ " )"))
-      dataize expr ((defaultDataizeContext ExRoot){_partial = True})
-        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
+    it "fails on it without the flag, naming the unknown atom" $
+      withNode $ do
+        expr <- parseExpressionThrows (primitives "2.times(3).nope")
+        dataize expr (withAtoms registry (defaultDataizeContext ExRoot))
+          `shouldThrow` (\e -> "Atom 'L_number_nope' does not exist" `isInfixOf` show (e :: SomeException))
+    it "leaves the application of the unregistered atom in place" $
+      withNode $ do
+        ((outcome, _), _) <- partially registry "2.times(3).nope"
+        case outcome of
+          Residual (ExFormation bds) -> bds `shouldContain` [BiLambda (Function "L_number_nope")]
+          other -> expectationFailure ("expected a residual formation, got " ++ show other)
+    it "keeps what was evaluated before the stuck site in the residue" $
+      withNode $ do
+        ((outcome, _), _) <- partially registry "2.times(3).nope"
+        case outcome of
+          Residual (ExFormation bds) -> do
+            let rho = [value | BiTau AtRho value <- bds]
+            length rho `shouldBe` 1
+            -- 2 × 3 = 6.0, whose IEEE 754 bytes are 40-18-00-00-00-00-00-00
+            show rho `shouldContain` show (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])
+            -- the times application is gone: ρ is the number it produced, its 'as-bytes' bound
+            [() | ExFormation inner <- rho, BiTau (AtLabel "as-bytes") _ <- inner] `shouldBe` [()]
+          other -> expectationFailure ("expected a residual formation, got " ++ show other)
+    it "reports the firing that succeeded with its result and the stuck site without one" $
+      withNode $ do
+        (_, reports) <- partially registry "2.times(3).nope"
+        map (._function) reports `shouldBe` ["L_number_times", "L_number_nope"]
+        map (isJust . (._result)) reports `shouldBe` [True, False]
+    it "leaves an unknown atom dataized directly as the whole residue" $
+      withNode $ do
+        ((outcome, chain), reports) <- partially registry "[[ L> Sym_arg_0 ]]"
+        outcome `shouldBe` Residual placeholder
+        map (._function) reports `shouldBe` ["Sym_arg_0"]
+        map fst chain `shouldEndWith` [placeholder]
+    it "still reaches bytes when nothing is stuck" $
+      withNode $ do
+        ((outcome, _), reports) <- partially registry "2.times(3)"
+        outcome `shouldBe` Dataized (BtMany ["40", "18", "00", "00", "00", "00", "00", "00"])
+        map (._function) reports `shouldBe` ["L_number_times"]
+    it "stops on the terminator ⊥ as before, since a wrong operand is not a stuck atom" $
+      withNode $ do
+        expr <- parseExpressionThrows (primitives ("5.plus( " ++ raw "--" ++ " )"))
+        dataize expr ((withAtoms registry (defaultDataizeContext ExRoot)){_partial = True})
+          `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
 
-  -- '_maxDepth'/'_maxCycles' bound the normalization rewriter that a 'box' or
-  -- 'norm' dataization step splices in (see 'normalized'); with
-  -- '_depthSensitive' on, exhausting either one propagates the very same
-  -- exception the rewriter itself throws, and with it off the limit is
-  -- absorbed silently, so dataization still reaches an answer.
   describe "DataizeContext's --max-depth/--max-cycles reach into the normalization it splices in" $ do
     let boxed = "[[ @ -> [[ D> 00- ]] ]]"
     forM_
       [
         ( "--max-cycles"
-        , DataizeContext ExRoot 25 0 (Steps 250 0) True True False buildTerm dontSaveStep dontSaveEval
+        , DataizeContext ExRoot 25 0 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval
         , "--max-cycles=0"
         )
       ,
         ( "--max-depth"
-        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False buildTerm dontSaveStep dontSaveEval
+        , DataizeContext ExRoot 0 25 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval
         , "--max-depth=0"
         )
       ]
@@ -532,8 +566,8 @@
             dataize expr ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))
       )
     forM_
-      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False buildTerm dontSaveStep dontSaveEval)
-      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False buildTerm dontSaveStep dontSaveEval)
+      [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval)
+      , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval)
       ]
       ( \(flag, ctx) ->
           it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do
@@ -555,23 +589,15 @@
             ++ map (.name) Yaml.normalizationRules
             ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.morphingRules
             ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.dataizationRules
-    it "uses no step label without a defining rule or operation" $ do
-      expr <-
-        parseExpressionThrows
-          ( unlines
-              [ "[["
-              , "  bytes(data) -> [[ @ -> $.data ]],"
-              , "  number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]],"
-              , "  @ -> 5.plus(6)"
-              , "]]"
-              ]
-          )
-      loc <- parseExpressionThrows "Q"
-      (_, chain) <- dataize expr (defaultDataizeContext loc)
-      let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]
-      unless
-        (null orphans)
-        (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))
+    it "uses no step label without a defining rule or operation" $
+      withNode $ do
+        expr <- parseExpressionThrows (primitives "5.plus(6)")
+        loc <- parseExpressionThrows "Q"
+        (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc))
+        let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]
+        unless
+          (null orphans)
+          (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))
 
   describe "names every rule uniquely across rule sets" $
     it "shares no rule name between morphing, dataization, normalization and contextualization" $ do
@@ -587,33 +613,34 @@
     let labelsOf loc src = do
           expr <- parseExpressionThrows src
           loc' <- parseExpressionThrows loc
-          (_, chain) <- dataize expr (defaultDataizeContext loc')
+          (_, chain) <- dataize expr (withAtoms registry (defaultDataizeContext loc'))
           pure [label | (_, Just label) <- chain]
-    it "dataizes 5.plus(6) through the expected rules" $ do
-      labels <-
-        labelsOf
-          "Q"
-          "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
-      labels
-        `shouldBe` [ "contextualize"
-                   , "maa"
-                   , "alpha"
-                   , "copy"
-                   , "mf"
-                   , "evaluate"
-                   , "ma"
-                   , "copy"
-                   , "mf"
-                   , "contextualize"
-                   , "dot"
-                   , "ma"
-                   , "stay"
-                   , "mf"
-                   , "contextualize"
-                   , "dot"
-                   , "copy"
-                   , "delta"
-                   ]
+    it "dataizes 5.plus(6) through the expected rules" $
+      withNode $ do
+        labels <-
+          labelsOf
+            "Q"
+            "[[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
+        labels
+          `shouldBe` [ "contextualize"
+                     , "maa"
+                     , "alpha"
+                     , "copy"
+                     , "mf"
+                     , "evaluate"
+                     , "ma"
+                     , "copy"
+                     , "mf"
+                     , "contextualize"
+                     , "dot"
+                     , "ma"
+                     , "stay"
+                     , "mf"
+                     , "contextualize"
+                     , "dot"
+                     , "copy"
+                     , "delta"
+                     ]
     it "dataizes a located reference through the expected rules" $ do
       labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
       labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf", "delta"]
@@ -626,77 +653,10 @@
       dataize expr (defaultDataizeContext loc)
         `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
 
+  -- Every case below reaches its bytes without firing an atom, so none of them
+  -- needs the registry: what they exercise is the calculus itself.
   testDataize
     [
-      ( "5.plus(6)"
-      , "Q"
-      , unlines
-          [ "[["
-          , "  bytes(data) -> [["
-          , "    @ -> $.data"
-          , "  ]],"
-          , "  number(as-bytes) -> [["
-          , "    @ -> $.as-bytes,"
-          , "    plus(x) -> [[ L> L_number_plus ]]"
-          , "  ]],"
-          , "  @ -> 5.plus(6)"
-          , "]]"
-          ]
-      , BtMany ["40", "26", "00", "00", "00", "00", "00", "00"]
-      )
-    ,
-      ( "Fahrenheit"
-      , "Q"
-      , unlines
-          [ "[["
-          , "  bytes -> [["
-          , "    data -> ?,"
-          , "    @ -> $.data"
-          , "  ]],"
-          , "  number -> [["
-          , "    as-bytes -> ?,"
-          , "    @ -> $.as-bytes,"
-          , "    plus -> [[ x -> ?, L> L_number_plus ]],"
-          , "    times -> [[ x -> ?, L> L_number_times ]]"
-          , "  ]],"
-          , "  @ -> $.c.times(1.8).plus(32),"
-          , "  c -> 25"
-          , "]]"
-          ]
-      , BtMany ["40", "53", "40", "00", "00", "00", "00", "00"]
-      )
-    ,
-      ( "Factorial"
-      , "Q"
-      , unlines
-          [ "[["
-          , "  bytes -> [["
-          , "    data -> ?,"
-          , "    eq -> [[ b -> ?, L> L_bytes_eq ]],"
-          , "    @ -> $.data"
-          , "  ]],"
-          , "  number -> [["
-          , "    as-bytes -> ?,"
-          , "    @ -> $.as-bytes,"
-          , "    times -> [[ x -> ?, L> L_number_times ]],"
-          , "    plus -> [[ x -> ?, L> L_number_plus ]],"
-          , "    eq -> [[ x -> ?, @ -> $.^.as-bytes.eq( x.as-bytes ) ]]"
-          , "  ]],"
-          , "  true -> [[ if -> [[ t -> ?, f -> ?, @ -> t ]] ]],"
-          , "  false -> [[ if -> [[ t -> ?, f -> ?, @ -> f ]] ]],"
-          , "  fac -> [["
-          , "    x -> ?,"
-          , "    @ -> $.x.eq( 1 ).if("
-          , "      1,"
-          , "      $.x.times($.^.fac($.x.plus(-1)))"
-          , "    )"
-          , "  ]],"
-          , "  @ -> $.fac(3)"
-          , "]]"
-          ]
-      , BtMany ["40", "18", "00", "00", "00", "00", "00", "00"]
-      )
-    ,
       ( "Located"
       , "Q.foo.bar"
       , unlines
@@ -737,88 +697,81 @@
       )
     ]
 
-  describe "atoms" $ do
+  -- Which λ functions exist is no longer phino's business: the registry given
+  -- with '--atoms' decides, and each one runs as an external script (see
+  -- 'Atoms'). What the cases below assert is that the answer of such a script
+  -- lands in the derivation exactly where a built-in atom's answer used to: 𝔼
+  -- normalizes it and 𝔻 carries on. The λ functions themselves are the fixture
+  -- ones (see 'Fixtures'), and 'number.eq' is composed out of 'L_bytes_eq' the
+  -- way 'eq.eo' composes it, so the EO-level composition is exercised too.
+  describe "atoms come from the registry" $ do
     testAtom
-      [ ("divides a positive dividend", "256.div( 16 )", BtMany ["40", "30", "00", "00", "00", "00", "00", "00"])
+      registry
+      [ ("adds two numbers", "5.plus( 6 )", BtMany ["40", "26", "00", "00", "00", "00", "00", "00"])
+      , ("multiplies two numbers", "5.times( 6 )", BtMany ["40", "3E", "00", "00", "00", "00", "00", "00"])
+      , -- Two firings in a row: 'ml' reduces the head of the second dispatch,
+        -- which fires the first atom, before the second one is handed its own
+        -- formation to fire against
+        ("fires twice down a chain of dispatches", "5.plus( 6 ).plus( 7 )", BtMany ["40", "32", "00", "00", "00", "00", "00", "00"])
+      , ("divides a positive dividend", "256.div( 16 )", BtMany ["40", "30", "00", "00", "00", "00", "00", "00"])
       , ("divides by zero into infinity", "2.div( 0 )", BtMany ["7F", "F0", "00", "00", "00", "00", "00", "00"])
       , ("tells 1000 is greater than 200", "1000.gt( 200 )", BtOne "FF")
       , ("tells 42 is not greater than 42.5", "42.gt( 42.5 )", BtOne "00")
       , ("tells zero is greater than a negative", "0.gt( -5 )", BtOne "FF")
       , ("tells 5 equals 5", "5.eq( 5 )", BtOne "FF")
       , ("tells 5 is not equal to 6", "5.eq( 6 )", BtOne "00")
-      , ("adds two numbers", "5.plus( 6 )", BtMany ["40", "26", "00", "00", "00", "00", "00", "00"])
-      , ("multiplies two numbers", "5.times( 6 )", BtMany ["40", "3E", "00", "00", "00", "00", "00", "00"])
-      ,
-        ( "conjoins two long bytes"
-        , raw "02-EF-D4-05-5E-78-3A" ++ ".and( " ++ raw "12-33-C1-B5-5E-71-55" ++ " )"
-        , BtMany ["02", "23", "C0", "05", "5E", "70", "10"]
-        )
-      ,
-        ( "disjoins negative bytes with one"
-        , raw "FF-FF-FF-FF-00-00-00-00" ++ ".or( " ++ raw "00-00-00-00-00-00-00-01" ++ " )"
-        , BtMany ["FF", "FF", "FF", "FF", "00", "00", "00", "01"]
-        )
       , ("inverts bytes", raw "CA-FE-BE-BE" ++ ".not", BtMany ["35", "01", "41", "41"])
-      ,
-        ( "concats two long bytes"
-        , raw "02-EF-D4-05-5E-78-3A" ++ ".concat( " ++ raw "12-33-C1-B5-5E-71-55" ++ " )"
-        , BtMany ["02", "EF", "D4", "05", "5E", "78", "3A", "12", "33", "C1", "B5", "5E", "71", "55"]
-        )
-      ,
-        ( "concats bytes with empty ones"
-        , raw "05-5E-78" ++ ".concat( " ++ raw "--" ++ " )"
-        , BtMany ["05", "5E", "78"]
-        )
-      , ("counts the size of bytes", raw "F1-20-5F-EC-B5-90-32" ++ ".size", BtMany ["40", "1C", "00", "00", "00", "00", "00", "00"])
       , ("tells equal bytes are equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FE" ++ " )", BtOne "FF")
       , ("tells different bytes are not equal", raw "CA-FE" ++ ".eq( " ++ raw "CA-FF" ++ " )", BtOne "00")
-      , ("takes a part of bytes", raw "20-1F-EE-B5-90" ++ ".slice( 1, 3 )", BtMany ["1F", "EE", "B5"])
-      ,
-        ( "shifts right an even negative"
-        , raw "C0-43-00-00-00-00-00-00" ++ ".right( 1 )"
-        , BtMany ["60", "21", "80", "00", "00", "00", "00", "00"]
-        )
-      ,
-        ( "shifts right minus one"
-        , raw "BF-F0-00-00-00-00-00-00" ++ ".right( 4 )"
-        , BtMany ["0B", "FF", "00", "00", "00", "00", "00", "00"]
-        )
-      ,
-        ( "shifts right by the integer minimum"
-        , raw "BF-F0-00-00-00-00-00-00" ++ ".right( -2147483648 )"
-        , BtMany ["00", "00", "00", "00", "00", "00", "00", "00"]
-        )
-      ,
-        ( "recovers from an out-of-bounds slice"
-        , raw "20-1F-EE-B5-90" ++ ".slice( 3, 10, [[ message -> ?, @ -> \"recovered\" ]] )"
-        , BtMany ["72", "65", "63", "6F", "76", "65", "72", "65", "64"]
-        )
-      ,
-        ( "recovers from a slice whose start plus length overflows"
-        , raw "20-1F-EE-B5-90" ++ ".slice( 2000000000, 2000000000, [[ message -> ?, @ -> \"recovered\" ]] )"
-        , BtMany ["72", "65", "63", "6F", "76", "65", "72", "65", "64"]
-        )
       ]
+
+    -- A whole program, not a single operation: every atom on the way is an
+    -- external script and the run still lands on the bytes EO's own
+    -- 'Fahrenheit' example lands on
+    it "dataizes a program whose every operation is an external atom" $
+      withNode $ do
+        expr <-
+          parseExpressionThrows
+            ( unlines
+                [ "[["
+                , "  bytes -> [["
+                , "    data -> ?,"
+                , "    @ -> $.data"
+                , "  ]],"
+                , "  number -> [["
+                , "    as-bytes -> ?,"
+                , "    @ -> $.as-bytes,"
+                , "    plus -> [[ x -> ?, L> L_number_plus ]],"
+                , "    times -> [[ x -> ?, L> L_number_times ]]"
+                , "  ]],"
+                , "  @ -> $.c.times(1.8).plus(32),"
+                , "  c -> 25"
+                , "]]"
+                ]
+            )
+        loc <- parseExpressionThrows "Q"
+        (value, _) <- dataize expr (withAtoms registry (defaultDataizeContext loc))
+        value `shouldBe` Dataized (BtMany ["40", "53", "40", "00", "00", "00", "00", "00"])
+
+    -- A name the registry does not carry has no λ function at all: 𝔼 gets
+    -- stuck on it, which is the only behaviour phino itself is left with
+    it "gets stuck on a λ function the registry does not carry" $ do
+      expr <- parseExpressionThrows (primitives "5.nope")
+      loc <- parseExpressionThrows "Q"
+      dataize expr (withAtoms registry (defaultDataizeContext loc))
+        `shouldThrow` (\e -> "Atom 'L_number_nope' does not exist" `isInfixOf` show (e :: SomeException))
+
+    -- An operand carrying no number is what an EO number atom answers ⊥ to, and
+    -- dataizing ⊥ fails through the terminator path. The judgment is the
+    -- script's now, so what these cases prove is that a ⊥ coming back from a
+    -- script stops 𝔻 exactly as a built-in ⊥ used to.
     testStuckAtom
-      [ ("cannot conjoin bytes of different lengths", raw "20-1F" ++ ".and( " ++ raw "CA-FE-BE" ++ " )")
-      , ("cannot disjoin bytes of different lengths", raw "20-1F" ++ ".or( " ++ raw "CA-FE-BE" ++ " )")
-      , ("cannot slice from an offset beyond the int range", raw "20-1F-EE-B5-90" ++ ".slice( 3000000000, 1 )")
-      , ("cannot slice a negative length", raw "20-1F-EE-B5-90" ++ ".slice( 1, -1 )")
-      , -- A number atom rejects an operand that carries no number (empty bytes),
-        -- yielding ⊥ rather than a result; dataizing ⊥ then fails through the
-        -- terminator path, exactly like the bytes-atom cases above.
-        ("cannot add a non-numeric operand", "5.plus( " ++ raw "--" ++ " )")
+      registry
+      [ ("cannot add a non-numeric operand", "5.plus( " ++ raw "--" ++ " )")
       , ("cannot multiply by a non-numeric operand", "5.times( " ++ raw "--" ++ " )")
       , ("cannot divide by a non-numeric divisor", "5.div( " ++ raw "--" ++ " )")
       , ("cannot compare against a non-numeric threshold", "5.gt( " ++ raw "--" ++ " )")
-      , -- A number atom also rejects a non-empty operand whose byte array is not
-        -- 8 bytes long (e.g. 2 or 5 bytes): such an array carries no number, and
-        -- the atom must yield ⊥ instead of crashing on 'btsToNum' (issue #1072).
+      , -- A byte array whose length is not 8 carries no number either (#1072)
         ("cannot add a 5-byte operand", "5.plus( " ++ raw "68-65-6C-6C-6F" ++ " )")
       , ("cannot multiply by a 2-byte operand", "5.times( " ++ raw "20-1F" ++ " )")
-      , ("cannot divide by a 3-byte divisor", "5.div( " ++ raw "CA-FE-BE" ++ " )")
-      , ("cannot compare against a 4-byte threshold", "5.gt( " ++ raw "FF-FF-FF-FF" ++ " )")
-      , -- 'right' rejects a shift distance that is not a plain 8-byte integer;
-        -- empty bytes carry no such integer, so the shift atom is stuck too.
-        ("cannot shift right by a non-integer distance", raw "C0-43-00-00-00-00-00-00" ++ ".right( " ++ raw "--" ++ " )")
       ]
diff --git a/test/Fixtures.hs b/test/Fixtures.hs
new file mode 100644
--- /dev/null
+++ b/test/Fixtures.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+-- The λ functions the specs fire. phino implements none of them, so a spec that
+-- needs an atom to answer brings its own: one JavaScript fixture,
+-- 'test-resources/atoms/primitives.js', registered under every name in
+-- 'fixtureAtoms' and branching on the one it is handed as its first
+-- command-line argument.
+module Fixtures (fixtureAtoms, fixtureRegistry, withFixtureRegistry, withNode) where
+
+import Atoms (Atom (..), Registry, Runtime (RtNode))
+import Control.Exception (bracket)
+import Data.Aeson (encode, object, (.=))
+import Data.Aeson.Key qualified as Key
+import Data.ByteString qualified as BS
+import Data.ByteString.Lazy qualified as BSL
+import Data.Map.Strict qualified as Map
+import Data.Maybe (isNothing)
+import Data.Text qualified as T
+import Data.Text.Encoding (decodeUtf8)
+import System.Directory (findExecutable, getTemporaryDirectory, removePathForcibly)
+import System.IO (Handle, hClose, openBinaryTempFile)
+import Test.Hspec (Expectation, pendingWith)
+
+-- Every λ function the fixture answers for. A name outside this list is
+-- unregistered, which is how a spec asks for an atom that cannot fire.
+fixtureAtoms :: [T.Text]
+fixtureAtoms =
+  [ "L_number_plus"
+  , "L_number_times"
+  , "L_number_div"
+  , "L_number_gt"
+  , "L_bytes_eq"
+  , "L_bytes_not"
+  ]
+
+-- The fixture script itself, read as UTF-8 rather than through the locale,
+-- since it spells 𝜑 expressions.
+fixtureScript :: IO T.Text
+fixtureScript = decodeUtf8 <$> BS.readFile "test-resources/atoms/primitives.js"
+
+-- The registry the specs that drive 'Dataize' directly run against.
+fixtureRegistry :: IO Registry
+fixtureRegistry = do
+  script <- fixtureScript
+  pure (Map.fromList [(name, Atom RtNode script) | name <- fixtureAtoms])
+
+-- The same registry as the JSON file '--atoms' reads, in a temporary file
+-- removed afterwards, for the specs that go through the command line.
+withFixtureRegistry :: (FilePath -> IO a) -> IO a
+withFixtureRegistry action = do
+  script <- fixtureScript
+  dir <- getTemporaryDirectory
+  bracket (openBinaryTempFile dir "phino-atoms-.json") discarded $ \(path, handle) -> do
+    BSL.hPut handle (encode (object [Key.fromText name .= entry script | name <- fixtureAtoms]))
+    hClose handle
+    action path
+  where
+    entry script = object ["rt" .= ("node" :: T.Text), "script" .= script]
+    discarded :: (FilePath, Handle) -> IO ()
+    discarded (path, handle) = hClose handle >> removePathForcibly path
+
+-- Every atom the fixture provides runs under 'node', so a machine without it
+-- cannot fire one at all: such an expectation is pending rather than red.
+withNode :: Expectation -> Expectation
+withNode expectation = do
+  node <- findExecutable "node"
+  if isNothing node
+    then pendingWith "'node' is not installed, so no λ function can be fired"
+    else expectation
diff --git a/test/FunctionsSpec.hs b/test/FunctionsSpec.hs
--- a/test/FunctionsSpec.hs
+++ b/test/FunctionsSpec.hs
@@ -14,7 +14,7 @@
 import Deps (Term (TeAttribute, TeBindings, TeBytes, TeExpression))
 import Functions (buildTerm)
 import Logger (logDebug)
-import Matcher (MetaValue (MvBindings), Subst (Subst), substEmpty)
+import Matcher (Meta (Named), MetaValue (MvBindings), Subst (Subst), substEmpty)
 import Misc (uniqueBindings')
 import Printer (printExpression)
 import Test.Hspec (Expectation, Spec, describe, it, shouldBe, shouldThrow)
@@ -44,9 +44,9 @@
 spec = describe "Functions" $ do
   describe "join" $ do
     it "contains only unique bindings after 'join'" $ do
-      let first = ("B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "a0")])
-          second = ("B2", MvBindings [BiTau AtRho ExXi, BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid (AtLabel "a1")])
-          third = ("B3", MvBindings [BiLambda (Function "Some"), BiTau (AtLabel "y") ExXi, BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "a0")])
+      let first = (Named "B1", MvBindings [BiVoid AtRho, BiDelta BtEmpty, BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "a0")])
+          second = (Named "B2", MvBindings [BiTau AtRho ExXi, BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid (AtLabel "a1")])
+          third = (Named "B3", MvBindings [BiLambda (Function "Some"), BiTau (AtLabel "y") ExXi, BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "a0")])
           subst = Subst (Map.fromList [first, second, third])
       TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2"), ArgBinding (BiMeta "B3")] subst
       bds' <- uniqueBindings' bds
@@ -54,8 +54,8 @@
       length bds' `shouldBe` 9
 
     it "renames a duplicate tau binding (not rho/delta/lambda) instead of dropping it" $ do
-      let first = ("B1", MvBindings [BiTau (AtLabel "x") ExRoot])
-          second = ("B2", MvBindings [BiTau (AtLabel "x") ExXi])
+      let first = (Named "B1", MvBindings [BiTau (AtLabel "x") ExRoot])
+          second = (Named "B2", MvBindings [BiTau (AtLabel "x") ExXi])
           subst = Subst (Map.fromList [first, second])
       TeBindings bds <- buildTerm "join" [ArgBinding (BiMeta "B1"), ArgBinding (BiMeta "B2")] subst
       length bds `shouldBe` 2
@@ -86,7 +86,7 @@
 
   describe "size" $
     it "counts the bindings bound to a meta" $ do
-      let subst = Subst (Map.singleton "B" (MvBindings [BiVoid AtRho, BiVoid (AtLabel "x")]))
+      let subst = Subst (Map.singleton (Named "B") (MvBindings [BiVoid AtRho, BiVoid (AtLabel "x")]))
       term <- buildTerm "size" [ArgBinding (BiMeta "B")] subst
       expectExpression term (DataNumber (numToBts 2))
 
diff --git a/test/MatcherSpec.hs b/test/MatcherSpec.hs
--- a/test/MatcherSpec.hs
+++ b/test/MatcherSpec.hs
@@ -13,7 +13,7 @@
 import Test.Hspec (Example (Arg), Expectation, Spec, SpecWith, describe, it, shouldBe)
 
 substs :: [[(T.Text, MetaValue)]] -> [Subst]
-substs = map (Subst . Map.fromList)
+substs = map (Subst . Map.mapKeys Named . Map.fromList)
 
 test ::
   (a -> a -> [Subst]) ->
@@ -466,6 +466,44 @@
         )
       ]
 
+  describe "matches an anonymous meta independently at every occurrence" $
+    -- Two anonymous metas of one kind sit at different offsets, so they are
+    -- different keys and bind different terms. That is what lets a pattern say
+    -- "any two attributes" without inventing a name for either of them (#218).
+    forM_
+      [
+        ( "[[ !t -> !e, !t -> !e ]] => [[ a -> Q, b -> $ ]] => both bindings bind their own slots"
+        , ExFormation
+            [ BiTau (AtAny (Slot "t" 1)) (ExAny (Slot "e" 2))
+            , BiTau (AtAny (Slot "t" 3)) (ExAny (Slot "e" 4))
+            ]
+        , ExFormation
+            [ BiTau (AtLabel "a") ExRoot
+            , BiTau (AtLabel "b") ExXi
+            ]
+        ,
+          [ Subst
+              ( Map.fromList
+                  [ (Anon (Slot "t" 1), MvAttribute (AtLabel "a"))
+                  , (Anon (Slot "e" 2), MvExpression ExRoot)
+                  , (Anon (Slot "t" 3), MvAttribute (AtLabel "b"))
+                  , (Anon (Slot "e" 4), MvExpression ExXi)
+                  ]
+              )
+          ]
+        )
+      ,
+        ( "[[ !t -> Q, !t -> Q ]] => [[ a -> Q ]] => no match, since one binding cannot fill two slots"
+        , ExFormation
+            [ BiTau (AtAny (Slot "t" 1)) ExRoot
+            , BiTau (AtAny (Slot "t" 3)) ExRoot
+            ]
+        , ExFormation [BiTau (AtLabel "a") ExRoot]
+        , []
+        )
+      ]
+      (\(desc, ptn, tgt, expected) -> it desc (matchExpression ptn tgt `shouldBe` expected))
+
   describe "combine" $
     forM_
       [ ("combines two empty substitutions", substEmpty, substEmpty, Just substEmpty)
@@ -473,26 +511,26 @@
       ,
         ( "combines an empty subst with a single-entry one"
         , substEmpty
-        , Subst (Map.singleton "at" (MvAttribute AtPhi))
-        , Just (Subst (Map.singleton "at" (MvAttribute AtPhi)))
+        , Subst (Map.singleton (Named "at") (MvAttribute AtPhi))
+        , Just (Subst (Map.singleton (Named "at") (MvAttribute AtPhi)))
         )
       ,
         ( "combines two substs with disjoint keys"
-        , Subst (Map.singleton "first" (MvAttribute AtPhi))
-        , Subst (Map.singleton "second" (MvBytes (BtOne "00")))
-        , Just (Subst (Map.fromList [("first", MvAttribute AtPhi), ("second", MvBytes (BtOne "00"))]))
+        , Subst (Map.singleton (Named "first") (MvAttribute AtPhi))
+        , Subst (Map.singleton (Named "second") (MvBytes (BtOne "00")))
+        , Just (Subst (Map.fromList [(Named "first", MvAttribute AtPhi), (Named "second", MvBytes (BtOne "00"))]))
         )
       ,
         ( "keeps a shared key when both substs agree on its value"
-        , Subst (Map.fromList [("first", MvAttribute AtRho), ("second", MvAttribute AtPhi)])
-        , Subst (Map.singleton "first" (MvAttribute AtRho))
-        , Just (Subst (Map.fromList [("first", MvAttribute AtRho), ("second", MvAttribute AtPhi)]))
+        , Subst (Map.fromList [(Named "first", MvAttribute AtRho), (Named "second", MvAttribute AtPhi)])
+        , Subst (Map.singleton (Named "first") (MvAttribute AtRho))
+        , Just (Subst (Map.fromList [(Named "first", MvAttribute AtRho), (Named "second", MvAttribute AtPhi)]))
         )
-      , ("returns Nothing when a shared key disagrees", Subst (Map.singleton "x" (MvAttribute AtPhi)), Subst (Map.singleton "x" (MvAttribute AtRho)), Nothing)
+      , ("returns Nothing when a shared key disagrees", Subst (Map.singleton (Named "x") (MvAttribute AtPhi)), Subst (Map.singleton (Named "x") (MvAttribute AtRho)), Nothing)
       ,
         ( "returns Nothing for the whole merge when any key conflicts"
-        , Subst (Map.fromList [("x", MvAttribute AtRho), ("y", MvBytes (BtOne "1F"))])
-        , Subst (Map.singleton "x" (MvAttribute AtPhi))
+        , Subst (Map.fromList [(Named "x", MvAttribute AtRho), (Named "y", MvBytes (BtOne "1F"))])
+        , Subst (Map.singleton (Named "x") (MvAttribute AtPhi))
         , Nothing
         )
       ]
diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs
--- a/test/ParserSpec.hs
+++ b/test/ParserSpec.hs
@@ -57,7 +57,7 @@
       , ("T(x -> Q)", Just (ExApplication ExTermination (ArTau (AtLabel "x") ExRoot)))
       , ("Q.org.eolang", Just (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")))
       , ("[[x -> $, y -> ?]]", Just (ExFormation [BiTau (AtLabel "x") ExXi, BiVoid (AtLabel "y"), BiVoid AtRho]))
-      , ("Q.!t", Just (ExDispatch ExRoot (AtMeta "t")))
+      , ("Q.!t1", Just (ExDispatch ExRoot (AtMeta "t1")))
       , ("[[]](!t1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtMeta "t1") ExXi)))
       ,
         ( "[[]](~0 -> $)(~11 -> Q)"
@@ -71,13 +71,13 @@
             )
         )
       , ("[[]](x -> $, y -> Q)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArTau (AtLabel "x") ExXi)) (ArTau (AtLabel "y") ExRoot)))
-      , ("[[!B, !B1]]", Just (ExFormation [BiMeta "B", BiMeta "B1"]))
+      , ("[[!B0, !B1]]", Just (ExFormation [BiMeta "B0", BiMeta "B1"]))
       , ("[[!B2, !t2 -> $]]", Just (ExFormation [BiMeta "B2", BiTau (AtMeta "t2") ExXi]))
       , ("!e0", Just (ExMeta "e0"))
-      , ("!k", Just (ExMeta "k"))
+      , ("!k1", Just (ExMeta "k1"))
       , ("[[x -> !k1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "k1"), BiVoid AtRho]))
-      , ("[[x -> !e]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e"), BiVoid AtRho]))
-      , ("[[!t -> !e1]]", Just (ExFormation [BiTau (AtMeta "t") (ExMeta "e1")]))
+      , ("[[x -> !e1]]", Just (ExFormation [BiTau (AtLabel "x") (ExMeta "e1"), BiVoid AtRho]))
+      , ("[[!t1 -> !e1]]", Just (ExFormation [BiTau (AtMeta "t1") (ExMeta "e1")]))
       , ("[[D> --]]", Just (ExFormation [BiDelta BtEmpty, BiVoid AtRho]))
       , ("[[D> 1F-]]", Just (ExFormation [BiDelta (BtOne "1F"), BiVoid AtRho]))
       , ("[[\n  L> Func,\n  D> 00-\n]]", Just (ExFormation [BiLambda (Function "Func"), BiDelta (BtOne "00"), BiVoid AtRho]))
@@ -104,10 +104,10 @@
             )
         )
       ,
-        ( "!e(x(^,@) -> [[w -> !e1]])"
+        ( "!e0(x(^,@) -> [[w -> !e1]])"
         , Just
             ( ExApplication
-                (ExMeta "e")
+                (ExMeta "e0")
                 ( ArTau
                     (AtLabel "x")
                     ( ExFormation
@@ -120,7 +120,7 @@
             )
         )
       ,
-        ( "[[x -> y.z, w -> ^, u -> @, p -> !t, q -> !e]]"
+        ( "[[x -> y.z, w -> ^, u -> @, p -> !t1, q -> !e1]]"
         , Just
             ( ExFormation
                 [ BiTau
@@ -134,10 +134,10 @@
                     (ExDispatch ExXi AtPhi)
                 , BiTau
                     (AtLabel "p")
-                    (ExDispatch ExXi (AtMeta "t"))
+                    (ExDispatch ExXi (AtMeta "t1"))
                 , BiTau
                     (AtLabel "q")
-                    (ExMeta "e")
+                    (ExMeta "e1")
                 , BiVoid AtRho
                 ]
             )
@@ -192,12 +192,12 @@
             )
         )
       ,
-        ( "[[𝐵1, 𝜏0 -> $, x -> 𝑒]]"
+        ( "[[𝐵1, 𝜏0 -> $, x -> 𝑒1]]"
         , Just
             ( ExFormation
                 [ BiMeta "B1"
                 , BiTau (AtMeta "t0") ExXi
-                , BiTau (AtLabel "x") (ExMeta "e")
+                , BiTau (AtLabel "x") (ExMeta "e1")
                 ]
             )
         )
@@ -309,10 +309,10 @@
       , ("AB-", Just (BtOne "AB"))
       , ("1F-2A-00", Just (BtMany ["1F", "2A", "00"]))
       , ("01-02-03-04-05", Just (BtMany ["01", "02", "03", "04", "05"]))
-      , ("!d", Just (BtMeta "d"))
+      , ("!d1", Just (BtMeta "d1"))
       , ("!d0", Just (BtMeta "d0"))
       , ("!d_test", Just (BtMeta "d_test"))
-      , ("δ", Just (BtMeta "d"))
+      , ("δ1", Just (BtMeta "d1"))
       , ("δ0", Just (BtMeta "d0"))
       , ("GG-", Nothing)
       , ("0-", Nothing)
@@ -331,27 +331,27 @@
       , ("@ -> $", Just (BiTau AtPhi ExXi))
       , ("ρ -> Q", Just (BiTau AtRho ExRoot))
       , ("φ -> T", Just (BiTau AtPhi ExTermination))
-      , ("!t -> $", Just (BiTau (AtMeta "t") ExXi))
+      , ("!t1 -> $", Just (BiTau (AtMeta "t1") ExXi))
       , ("!t0 -> Q", Just (BiTau (AtMeta "t0") ExRoot))
       , ("D> --", Just (BiDelta BtEmpty))
       , ("D> 42-", Just (BiDelta (BtOne "42")))
       , ("D> 01-02-03", Just (BiDelta (BtMany ["01", "02", "03"])))
-      , ("D> !d", Just (BiDelta (BtMeta "d")))
+      , ("D> !d1", Just (BiDelta (BtMeta "d1")))
       , ("Δ ⤍ FF-", Just (BiDelta (BtOne "FF")))
       , ("Δ ⤍ --", Just (BiDelta BtEmpty))
       , ("L> Func", Just (BiLambda (Function "Func")))
       , ("L> Function_name", Just (BiLambda (Function "Function_name")))
       , ("L> Aφ", Just (BiLambda (Function "Aφ")))
       , ("λ ⤍ Test", Just (BiLambda (Function "Test")))
-      , ("L> !F", Just (BiLambda (FnMeta "F")))
+      , ("L> !F1", Just (BiLambda (FnMeta "F1")))
       , ("L> !F0", Just (BiLambda (FnMeta "F0")))
-      , ("λ ⤍ 𝑓", Just (BiLambda (FnMeta "F")))
+      , ("λ ⤍ 𝑓1", Just (BiLambda (FnMeta "F1")))
       , ("L> 𝑓2", Just (BiLambda (FnMeta "F2")))
-      , ("!B", Just (BiMeta "B"))
+      , ("!B1", Just (BiMeta "B1"))
       , ("!B0", Just (BiMeta "B0"))
       , ("!B_test", Just (BiMeta "B_test"))
-      , ("𝐵", Just (BiMeta "B"))
       , ("𝐵1", Just (BiMeta "B1"))
+      , ("𝐵1", Just (BiMeta "B1"))
       , ("x() -> [[]]", Just (BiTau (AtLabel "x") (ExFormation [BiVoid AtRho])))
       , ("y(^) -> [[]]", Just (BiTau (AtLabel "y") (ExFormation [BiVoid AtRho])))
       , ("z(^, @) -> [[]]", Just (BiTau (AtLabel "z") (ExFormation [BiVoid AtRho, BiVoid AtPhi])))
@@ -375,10 +375,10 @@
       , ("ρ", Just AtRho)
       , ("@", Just AtPhi)
       , ("φ", Just AtPhi)
-      , ("!t", Just (AtMeta "t"))
+      , ("!t1", Just (AtMeta "t1"))
       , ("!t0", Just (AtMeta "t0"))
       , ("!t_test", Just (AtMeta "t_test"))
-      , ("𝜏", Just (AtMeta "t"))
+      , ("𝜏1", Just (AtMeta "t1"))
       , ("𝜏0", Just (AtMeta "t0"))
       , ("a0", Just (AtLabel "a0"))
       , ("a1", Just (AtLabel "a1"))
@@ -526,28 +526,51 @@
       , ("[[]](Q, T)", Just (ExApplication (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (Alpha 0) ExRoot)) (ArAlpha (Alpha 1) ExTermination)))
       , ("Q.x(y -> $)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArTau (AtLabel "y") ExXi)))
       , ("[[x -> ?]].x(Q)", Just (ExApplication (ExDispatch (ExFormation [BiVoid (AtLabel "x"), BiVoid AtRho]) (AtLabel "x")) (ArAlpha (Alpha 0) ExRoot)))
-      , ("[[]](~!i -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExXi)))
-      , ("[[]](α𝑖 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i") ExRoot)))
+      , ("[[]](~!i1 -> $)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i1") ExXi)))
+      , ("[[]](α𝑖1 -> Q)", Just (ExApplication (ExFormation [BiVoid AtRho]) (ArAlpha (AlMeta "i1") ExRoot)))
       , ("Q.foo(a1 -> Q.y)", Just (ExApplication (ExDispatch ExRoot (AtLabel "foo")) (ArTau (AtLabel "a1") (ExDispatch ExRoot (AtLabel "y"))))) -- #875: "a"-prefixed label in argument position is a named binding, not a positional alpha
       ]
 
   describe "parse meta expressions" $
     test
       parseExpression
-      [ ("!e", Just (ExMeta "e"))
+      [ ("!e1", Just (ExMeta "e1"))
       , ("!e0", Just (ExMeta "e0"))
       , ("!e_test", Just (ExMeta "e_test"))
-      , ("𝑒", Just (ExMeta "e"))
+      , ("𝑒1", Just (ExMeta "e1"))
       , ("𝑒0", Just (ExMeta "e0"))
-      , ("!e.x", Just (ExDispatch (ExMeta "e") (AtLabel "x")))
-      , ("!e(Q)", Just (ExApplication (ExMeta "e") (ArAlpha (Alpha 0) ExRoot)))
-      , ("!n", Just (ExMeta "n"))
+      , ("!e1.x", Just (ExDispatch (ExMeta "e1") (AtLabel "x")))
+      , ("!e1(Q)", Just (ExApplication (ExMeta "e1") (ArAlpha (Alpha 0) ExRoot)))
       , ("!n1", Just (ExMeta "n1"))
-      , ("𝑛", Just (ExMeta "n"))
+      , ("!n1", Just (ExMeta "n1"))
       , ("𝑛1", Just (ExMeta "n1"))
-      , ("𝑛.x", Just (ExDispatch (ExMeta "n") (AtLabel "x")))
+      , ("𝑛1", Just (ExMeta "n1"))
+      , ("𝑛1.x", Just (ExDispatch (ExMeta "n1") (AtLabel "x")))
       ]
 
+  describe "parse anonymous meta-variables" $
+    -- A meta written without an index is anonymous: it stands for whatever term
+    -- fills its place and no rule may name it afterwards. It is told apart from
+    -- every other anonymous meta of the same term by the offset it starts at,
+    -- which is why one formation may carry two of the same kind (#218).
+    test
+      parseExpression
+      [ ("!e", Just (ExAny (Slot "e" 0)))
+      , ("𝑒", Just (ExAny (Slot "e" 0)))
+      , ("!n", Just (ExAny (Slot "n" 0)))
+      , ("𝑘", Just (ExAny (Slot "k" 0)))
+      , ("!e.x", Just (ExDispatch (ExAny (Slot "e" 0)) (AtLabel "x")))
+      ,
+        ( "⟦ 𝜏 ↦ 𝑒, 𝜏 ↦ 𝑒 ⟧"
+        , Just
+            ( ExFormation
+                [ BiTau (AtAny (Slot "t" 2)) (ExAny (Slot "e" 6))
+                , BiTau (AtAny (Slot "t" 9)) (ExAny (Slot "e" 13))
+                ]
+            )
+        )
+      ]
+
   describe "parse whitespace handling" $
     forM_
       [ "[[  x   ->   Q  ]]"
@@ -561,9 +584,9 @@
   describe "parse unicode meta-k expression" $
     test
       parseExpression
-      [ ("𝑘", Just (ExMeta "k"))
+      [ ("𝑘1", Just (ExMeta "k1"))
       , ("𝑘1", Just (ExMeta "k1"))
-      , ("𝑘.x", Just (ExDispatch (ExMeta "k") (AtLabel "x")))
+      , ("𝑘1.x", Just (ExDispatch (ExMeta "k1") (AtLabel "x")))
       ]
 
   describe "ParserException Show instance" $
@@ -597,7 +620,7 @@
     forM_
       [ ("exposes an _alpha field parsing an alpha directly", parseMaybe (_alpha phiParser) "~3" `shouldBe` Just (Alpha 3))
       , ("exposes an _attribute field parsing an attribute directly", parseMaybe (_attribute phiParser) "foo" `shouldBe` Just (AtLabel "foo"))
-      , ("exposes an _index field parsing an index meta directly", parseMaybe (_index phiParser) "!i0" `shouldBe` Just "i0")
+      , ("exposes an _index field parsing an index meta directly", parseMaybe (_index phiParser) "!i0" `shouldBe` Just (Right "i0"))
       , ("exposes a _binding field parsing a binding directly", parseMaybe (_binding phiParser) "x -> $" `shouldBe` Just (BiTau (AtLabel "x") ExXi))
       , ("exposes an _expression field parsing an expression directly", parseMaybe (_expression phiParser) "Q.x" `shouldBe` Just (ExDispatch ExRoot (AtLabel "x")))
       , ("exposes a _string field parsing a quoted string directly", parseMaybe (_string phiParser) "\"hi\"" `shouldBe` Just "hi")
diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs
--- a/test/PrinterSpec.hs
+++ b/test/PrinterSpec.hs
@@ -15,7 +15,7 @@
 import Encoding (Encoding (..))
 import Lining (LineFormat (..))
 import Margin (defaultMargin)
-import Matcher (MetaValue (..), Subst (Subst))
+import Matcher (Meta (Named), MetaValue (..), Subst (Subst))
 import Parser (parseExpression)
 import Printer
 import Sugar (SugarType (..))
@@ -258,28 +258,28 @@
 
   describe "printSubsts and printSubsts' render substitutions" $
     forM_
-      [ ("MvAttribute", [Subst (Map.singleton "t" (MvAttribute (AtLabel "x")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "t >> x")
-      , ("MvIndex", [Subst (Map.singleton "i" (MvIndex 3))], (SWEET, UNICODE, MULTILINE, defaultMargin), "i >> 3")
-      , ("MvExpression", [Subst (Map.singleton "e" (MvExpression ExRoot))], (SWEET, UNICODE, MULTILINE, defaultMargin), "e >> Φ")
-      , ("MvBytes", [Subst (Map.singleton "b" (MvBytes (BtOne "1F")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "b >> 1F-")
-      , ("MvBindings", [Subst (Map.singleton "bnd" (MvBindings [BiVoid (AtLabel "y")]))], (SWEET, UNICODE, MULTILINE, defaultMargin), "bnd >> ⟦ y ↦ ∅ ⟧")
-      , ("MvFunction", [Subst (Map.singleton "f" (MvFunction "func"))], (SWEET, UNICODE, MULTILINE, defaultMargin), "f >> func")
+      [ ("MvAttribute", [Subst (Map.singleton (Named "t") (MvAttribute (AtLabel "x")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "t >> x")
+      , ("MvIndex", [Subst (Map.singleton (Named "i") (MvIndex 3))], (SWEET, UNICODE, MULTILINE, defaultMargin), "i >> 3")
+      , ("MvExpression", [Subst (Map.singleton (Named "e") (MvExpression ExRoot))], (SWEET, UNICODE, MULTILINE, defaultMargin), "e >> Φ")
+      , ("MvBytes", [Subst (Map.singleton (Named "b") (MvBytes (BtOne "1F")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "b >> 1F-")
+      , ("MvBindings", [Subst (Map.singleton (Named "bnd") (MvBindings [BiVoid (AtLabel "y")]))], (SWEET, UNICODE, MULTILINE, defaultMargin), "bnd >> ⟦ y ↦ ∅ ⟧")
+      , ("MvFunction", [Subst (Map.singleton (Named "f") (MvFunction "func"))], (SWEET, UNICODE, MULTILINE, defaultMargin), "f >> func")
       ,
         ( "keys of a multi-entry substitution are sorted and each is on its own line"
-        , [Subst (Map.fromList [("a", MvIndex 1), ("b", MvIndex 2)])]
+        , [Subst (Map.fromList [(Named "a", MvIndex 1), (Named "b", MvIndex 2)])]
         , (SWEET, UNICODE, MULTILINE, defaultMargin)
         , "a >> 1\nb >> 2"
         )
       ,
         ( "multiple substitutions are separated with a dashed line"
-        , [Subst (Map.singleton "a" (MvIndex 1)), Subst (Map.singleton "b" (MvIndex 2))]
+        , [Subst (Map.singleton (Named "a") (MvIndex 1)), Subst (Map.singleton (Named "b") (MvIndex 2))]
         , (SWEET, UNICODE, MULTILINE, defaultMargin)
         , "a >> 1\n------\nb >> 2"
         )
       , ("an empty substitution list renders the dashed placeholder", [], (SWEET, UNICODE, SINGLELINE, defaultMargin), "------")
       ,
         ( "picks the encoding from its PrintConfig for an attribute meta value (ASCII rho)"
-        , [Subst (Map.singleton "t" (MvAttribute AtRho))]
+        , [Subst (Map.singleton (Named "t") (MvAttribute AtRho))]
         , (SWEET, ASCII, SINGLELINE, defaultMargin)
         , "t >> ^"
         )
diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs
--- a/test/YamlSpec.hs
+++ b/test/YamlSpec.hs
@@ -18,16 +18,19 @@
 import Files (allPathsIn)
 import System.FilePath
 import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldSatisfy, shouldThrow)
-import Yaml (Condition (..), ContextualizeRule (..), DataizeRule (..), MorphRule (..), Number, Operation (..), Premise (..), contextualizationRules, dataizationRules, morphingRules, yamlRule)
+import Yaml (Condition (..), ContextualizeRule (..), DataizeRule (..), MorphRule (..), Number, Operation (..), Premise (..), Rule, contextualizationRules, dataizationRules, morphingRules, yamlRule)
 
 decodeYaml' :: (Yaml.FromJSON a) => String -> Either Yaml.ParseException a
 decodeYaml' = Yaml.decodeEither' . encodeUtf8 . T.pack
 
-failsAsRedundant :: Either Yaml.ParseException a -> Bool
-failsAsRedundant decoded = case decoded of
-  Left err -> "redundant" `isInfixOf` Yaml.prettyPrintParseException err
+failsWith :: String -> Either Yaml.ParseException a -> Bool
+failsWith fragment decoded = case decoded of
+  Left err -> fragment `isInfixOf` Yaml.prettyPrintParseException err
   Right _ -> False
 
+failsAsRedundant :: Either Yaml.ParseException a -> Bool
+failsAsRedundant = failsWith "redundant"
+
 spec :: Spec
 spec = do
   describe "parses yaml rule" $ do
@@ -70,6 +73,103 @@
       ( \(desc, yaml, valid) ->
           it ("rejects " ++ desc) (unless valid (expectationFailure ("expected rejection for: " ++ yaml)))
       )
+
+  describe "rejects an anonymous meta outside a pattern" $ do
+    -- An anonymous meta is bound by the pattern it stands in and forgotten as
+    -- soon as that pattern matches, so no other part of a rule has a name to
+    -- read it back by. Writing one there is a mistake in the rule, caught as
+    -- the rule loads rather than left to surface as a silent non-match.
+    let rewriting :: String -> String
+        rewriting field = "name: foo\npattern: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\n" ++ field
+        inferring :: String -> String
+        inferring field = "name: foo\nmatch: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\n" ++ field
+    forM_
+      [
+        ( "in 'result' of a rewriting rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'result' of rule 'foo'"
+            (decodeYaml' (rewriting "result: '𝑒'") :: Either Yaml.ParseException Rule)
+        )
+      ,
+        ( "in 'when' of a rewriting rule"
+        , failsWith
+            "anonymous meta '!t' cannot be referenced in 'when' of rule 'foo'"
+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  in: ['𝜏', '!B1']") :: Either Yaml.ParseException Rule)
+        )
+      ,
+        ( "in 'where' of a rewriting rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'where' of rule 'foo'"
+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhere:\n  - meta: '!t1'\n    function: concat\n    args: ['𝑒']") :: Either Yaml.ParseException Rule)
+        )
+      ,
+        ( "in 'having' of a rewriting rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'having' of rule 'foo'"
+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nhaving:\n  formation: '𝑒'") :: Either Yaml.ParseException Rule)
+        )
+      ,
+        ( "as a bare index meta in 'when' of a rewriting rule"
+        , failsWith
+            "anonymous meta '!i' cannot be referenced in 'when' of rule 'foo'"
+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  eq: ['𝑖', 1]") :: Either Yaml.ParseException Rule)
+        )
+      ,
+        ( "inside an 'nf' condition of a rewriting rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"
+            (decodeYaml' (rewriting "result: '⟦ ⟧'\nwhen:\n  nf: '𝑒'") :: Either Yaml.ParseException Rule)
+        )
+      ,
+        ( "in 'n-result' of a morphing rule"
+        , failsWith
+            "anonymous meta '!n' cannot be referenced in 'n-result' of rule 'foo'"
+            (decodeYaml' (inferring "e-match: 𝑒0\nn-result: '𝑛'") :: Either Yaml.ParseException MorphRule)
+        )
+      ,
+        ( "in a premise of a morphing rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"
+            (decodeYaml' (inferring "e-match: 𝑒0\nn-result: 𝑛1\npremises:\n  - n-result: 𝑛1\n    normalize: '𝑒'") :: Either Yaml.ParseException MorphRule)
+        )
+      ,
+        ( "in 'when' of a morphing rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"
+            (decodeYaml' (inferring "e-match: 𝑒0\nn-result: 𝑛1\nwhen:\n  formation: '𝑒'") :: Either Yaml.ParseException MorphRule)
+        )
+      ,
+        ( "in 'd-result' of a dataization rule"
+        , failsWith
+            "anonymous meta '!d' cannot be referenced in 'd-result' of rule 'foo'"
+            (decodeYaml' (inferring "e-match: 𝑒0\nd-result: 'δ'") :: Either Yaml.ParseException DataizeRule)
+        )
+      ,
+        ( "in 'when' of a dataization rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'when' of rule 'foo'"
+            (decodeYaml' (inferring "e-match: 𝑒0\nd-result: δ0\nwhen:\n  formation: '𝑒'") :: Either Yaml.ParseException DataizeRule)
+        )
+      ,
+        ( "in a premise of a dataization rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"
+            (decodeYaml' (inferring "e-match: 𝑒0\nd-result: δ0\npremises:\n  - d-result: δ0\n    dataize: '𝑒'") :: Either Yaml.ParseException DataizeRule)
+        )
+      ,
+        ( "in a premise of a contextualization rule"
+        , failsWith
+            "anonymous meta '!e' cannot be referenced in 'premises' of rule 'foo'"
+            (decodeYaml' (inferring "c-match: 𝑘0\nc-result: 𝑛1\npremises:\n  - n-result: 𝑛1\n    normalize: '𝑒'") :: Either Yaml.ParseException ContextualizeRule)
+        )
+      ,
+        ( "in 'c-result' of a contextualization rule"
+        , failsWith
+            "anonymous meta '!k' cannot be referenced in 'c-result' of rule 'foo'"
+            (decodeYaml' (inferring "c-match: 𝑘0\nc-result: '𝑘'") :: Either Yaml.ParseException ContextualizeRule)
+        )
+      ]
+      (\(desc, rejected) -> it ("rejects an anonymous meta " ++ desc) (rejected `shouldBe` True))
 
   describe "keeps effective labels unique across rule sets" $
     -- The effective label of a rule is its 'label' when present, else its