rules_spec

bazel_dep(name = "rules_spec", version = "0.5.1")

bazel_dep(name = "spec", version = "0.8.3")

spec/
  README.md                 # this file — spine vehicle
  LEDGER.md                 # every include / optional / absorb / exclude row
  MODULE.bazel              # module(name = "spec", version = "0.8.3")
  tools/ledger-check.sh     # CI: LEDGER include dirs exist; excludes do not
  lean/                     # Lean spec libs + proof ratchet
  crank/                    # E(G)-descent harness
  rdf/                      # ontology, SPARQL gates, readmodel queries
  corpus/                   # flagship corpora + gate data
  grounding/                # grounding_verified + adversarial gate
  console/                  # hosted grounding / authoring console
  agent/                    # Eve markup assistant
  conformance/              # shared JSON cases
  smoke/consumer/           # module(name = "spec_smoke_consumer", version = "0.0.0")
  java/                     # Jena/RDF corpus toolkit
  services/                 # Rust spec plugin + materialized readmodel

v0.8.3

Real usage, taken from the module’s examples/.

examples/diff_gate/BUILD.bazel

load("@spec//tools:diff.bzl", "emit_diff_test")

package(default_visibility = ["//visibility:public"])

# Stand-in for a real emitter (lean_emit / genrule): produces a file
# byte-identical to the committed copy, so the gate passes.
genrule(
    name = "generated",
    srcs = ["committed.txt"],
    outs = ["generated.txt"],
    cmd = "cp $< $@",
)

# Smoke: the gate is green when the generated artifact matches the committed
# copy. (The failure path — drift → exit 1 — is exercised by real consumers.)
emit_diff_test(
    name = "generated_diff_test",
    generated = ":generated",
    committed = "committed.txt",
    update_target = "//examples/diff_gate:update_generated",
)

from docs/compaction.md

Deterministic compaction — the corrector pass (RFC-001 §5 / RFC-001b §5)

The reverse-diffusion step is predict then project. The corrector P is the deterministic, machine-checkable projection that never raises the energy — the safe half of each crank. This is its first implementation over the materialized graph, built as the hybrid you chose: a Lean-proven core + executable passes over the live graph: a Lean-proven core + SPARQL passes, with Lean→Rust emission available later via the kernel’s existing path.

Correction (2026-08-05). This section previously said Rust passes were deferred because “rules_rust isn’t in the ecosystem.” That is no longer true — MODULE.bazel declares bazel_dep(name = "rules_rust", version = "0.70.0") with a Rust 1.95.0 toolchain and an isolated crate_universe, and services/spec/ is a Rust binary. The SPARQL passes below remain the right first cut on their own merits (they run where the data lives), but the hot-path Rust option RFC-001 §5 wanted is available today and needs no new dependency. See RFC-002 §3.2.

Lean-proven core — the corrector invariants

lean/Spec/Compaction/Projection.lean, built by //lean:compaction_test (pure Lean 4 core, no Mathlib, no sorry). For the redundancy-collapse pass dedupE over the asserted-edge list, with redundancy cost R(l) := l.length:

invariant	theorem	meaning
meaning-preserving	mem_dedupE : x ∈ dedupE l ↔ x ∈ l	the edge set is unchanged
energy-non-increasing	dedupE_length_le : (dedupE l).length ≤ l.length	E(P G) ≤ E(G) for R
idempotent	dedupE_idem : dedupE (dedupE l) = dedupE l	P is a true projection (a crystal fixed point)

These are exactly the three properties RFC-001b §5 requires of the corrector. redCost_dedupE_le restates the second in energy terms.

Executable passes — over the live graph (//corpus)

Transitive reduction (L↓). compaction-reduce.rq drops every :dependsOn edge implied by a longer path. Because :dependsOn is owl:TransitiveProperty, the transitive closure (reachability) is invariant, so the reduction is meaning-preserving. Measured (//corpus:compaction_measure, //corpus:redundant_edges):

• 20 → 16 dependsOn edges; 4 redundant removed: RFC-0905→RFC-0900 (via RFC-0901), RFC-0906→RFC-0900 (via RFC-0901), RFC-0910→RFC-0900 (via RFC-0902), RFC-0912→RFC-0900 (via RFC-0902).

Symmetry detection (S). motifs.ttl makes the motif structure explicit; motif-orbits.rq groups the components into orbits. Measured: 7 motif templates cover all 16 components (25 realizesMotif edges), confirming crank-001’s S = 7 from the graph itself:

motif	members
M1 propose → kernel admits	7
M7 content-addressed artifact	4
M3 read-only projection	3
M4 gRPC extension	3
M5 typed fact plane	3
M6 conserved-dimension generalization	3
M2 sandboxed simulation	2

Net E(G) movement (this corrector pass)

• L (connectivity): redundant edges down 4 (20 → 16), closure preserved.
• S (symmetry): 7 templates extracted over 16 components — the recoverable symmetry is now explicit and measured, ready for the collapse-to-template step.
• R (redundancy): the dedup pass is proven energy-non-increasing in Lean.

What’s next

1. Collapse to templates: rewrite each orbit’s per-instance claims to a single parametrized motif template + thin instance tuples (the full S↑ realization; detection is done, rewrite is next).
2. Wire P into the crank loop: run predict (LLM) → project (this corrector) per crank and record the E(G) series.
3. Lean transitive reduction: lift the L↓ closure-preservation proof into Lean (needs a reachability model) to match the dedup pass’s rigor.

from docs/consumer-onboarding.md

Onboarding a consumer corpus

A private project — its requirements, its glossary, its conflicts — brought onto the spec plane with none of its data in this repository.

That last clause is the constraint everything below is shaped by. It is not a preference: a consumer’s corpus is the product’s own normative content, this repository is public, and a design that needed a copy here would be a design no consumer could adopt. So the corpus stays in the consumer’s repository, the log stays in the consumer’s database, and what crosses the boundary is spec’s module going out and, at most, a count and a hash coming back (tools/evaluation/README.md).

---

1. The topology: one console per consumer

Decided. One deployment of the console per consumer organization, each with its own corpus, its own log, and its own domain gate. Not multi-tenant.

The reason is that every piece of state the console holds is already per-tenant, and the three that matter are the three whose failure modes are worst:

	per-tenant, because
the corpus	it is the consumer’s normative content, and frozenReadPoint() already refuses payloads spanning two corpora — the read point every proposal names is one corpus’s
the append-only log	spec.proposal_log has no DELETE by design. Two tenants’ proposals in one table cannot be separated afterwards, ever
the domain gate	GOOGLE_ALLOWED_DOMAIN is one Workspace, and it fails closed — one console cannot admit two Workspaces without admitting everybody

A multi-tenant console would have to add a tenant column to an append-only log and a per-row authorization check in front of it, and get both right on the first try, because there is no migration back out of a log you cannot delete from. The per-deployment answer needs neither: the isolation is the deployment boundary, which is a boundary the platform already enforces.

The cost is real and worth stating: N consoles is N Vercel projects, N Neon databases, N sets of secrets, and N migration runs. It buys an isolation property that does not depend on anybody’s code being correct.

---

2. What crosses the boundary

   this repository                          the consumer's repository
   ──────────────                           ─────────────────────────
   @spec//rdf gate macros      ───────►     runs over its own TTL in its CI
   emit_readmodel.py           ───────►     runs over its own TTL, emits payloads
   the console source          ───────►     deployed per tenant

   a claim's id + a count + a query hash   ◄───  POST /api/evaluation
   (never SQL, never rows — see tools/evaluation/README.md)

Nothing else. In particular no corpus TTL, no read-model payload, and no log line from a consumer belongs in this repository. console/test/fixtures/readmodel/ is spec’s own fixture corpus standing in for one, and is the shape of the only consumer-like data that ever lives here.

---

3. The steps

3.1 Gates in the consumer’s own CI

smoke/consumer/ is the worked example, held permanently in CI: spec resolved from the registry, its gate macros loaded across the repo boundary.

bazel_dep(name = "spec", version = "0.8.1")
bazel_dep(name = "rules_rdf", version = "0.3.0")
bazel_dep(name = "rules_jena", version = "0.3.2")

load("@rules_rdf//rdf:dataset.bzl", "rdf_dataset")
load("@spec//rdf:gates.bzl", "spec_corpus_gates")
load("@spec//rdf:authoring_gates.bzl", "spec_authoring_gates")

rdf_dataset(
    name = "corpus",
    srcs = glob(["*.ttl"]),
    in_format = "turtle",
    # ⛔ authoring_vocab (rfc: + au:), NOT vocab. The authoring gates key on au:
    # terms and pass VACUOUSLY without them — the same defect they exist to catch.
    deps = ["@spec//rdf:authoring_vocab"],
)

spec_corpus_gates(name = "corpus_gates", dataset = ":corpus")
spec_authoring_gates(name = "corpus_authoring", dataset = ":corpus")

File layout. One TTL per act, never one big file — corpus/ampere/ is the model: the imported claims, the disciplines, the named holes from decomposition, and the promoted proposals each in their own file, because each is regenerated by a different tool at a different time.

⛔ And the corpus directory contains ONLY the corpus. Fixtures, overlays, scratch TTLs and anything else that is not what the project commits to go in a subdirectory. This is not tidiness:

tools/readmodel/emit_readmodel.py decides what a corpus IS by listing the directory (*.ttl), while the gates decide by reading the rdf_dataset’s srcs. Two derivation-test overlays landed beside corpus/ampere/’s files, each declaring in its own first line “NOT part of the committed corpus”, and the next regeneration would have shown conflict INV-03 as resolved in the console while every gate saw it open — plus a claim carrying no au:rung, planted so ladder-integrity.rq could catch it, rendered as an ordinary requirement. Nine rows across five of the eight payloads, silently.

//tools/readmodel:corpus_is_the_corpus_test holds spec’s own corpora to it, by comparing the dataset’s srcs against glob(["*.ttl"]). A consumer wiring the same two tools should hold its own corpus to the same rule — the failure is silent in both directions and the console is the side that ends up lying.

The honest-import posture. A freshly imported corpus lands at R0, nothing decomposed, nothing grounded, nothing proven, dark fraction 100% — that is what corpus/studio/ reads and it is correct. A corpus that imported at R2 because the sentences “looked structured” would be inventing the thing being measured.

3.2 The read model

The console renders eight payloads. Derive them in your own build, from the same corpus your gates run over:

load("@spec//rdf/readmodel:readmodel.bzl", "spec_readmodel")

spec_readmodel(
    name = "readmodel",
    dataset = ":corpus",         # the SAME dataset the gates use
    project = "myproject",       # the value every row carries
    srcs = MY_CORPUS,            # the dataset's own srcs — see the ⚠ below
)

bazel build //:readmodel writes readmodel/{claims,conflicts,disciplines, envelopes,frontier,requirements,terms,witness}.json. Point SPEC_READMODEL_DIR at that directory (§3.3) and the console builds against it.

This runs the engine of record. The eight questions execute under ARQ via sparql_query — the same binary every gate runs — so the numbers in the console and the numbers that decide the gates come from one engine. That was not true before, and it was not a theoretical concern:

The envelopes route was written in a form that returns rows under rdflib and zero rows under ARQ for every input. A consumer’s empty-envelopes panel would have read “no infeasibilities” for a corpus full of them. See RFC-005 §3③ — it is the third instance of a defect this repository had already found and fixed twice, in gates, and it survived in the read model precisely because the read model ran a different engine.

⚠ srcs must be exactly the dataset’s own srcs. Nothing ties them together — a macro cannot read a target’s providers — and srcs is what the corpus_version digest is taken over. Listing fewer files than the dataset contains yields a read point that does not describe what was queried. Keep one list and pass it to both, the way corpus/ampere/BUILD.bazel keeps AMPERE_CORPUS.

⚠ deps must include @spec//rdf:authoring_vocab — same rule as the gates. Without the au: terms every pattern matches nothing and all eight payloads emit empty, which is a vacuous pass wearing a green build.

The script, if you cannot run the build

tools/readmodel/emit_readmodel.py asks the same eight questions — it reads the same .rq files — under rdflib:

pip install 'rdflib>=7,<8'
python3 emit_readmodel.py --out readmodel --corpus myproject=corpus/

It is what spec’s own committed payloads are still emitted with, and they are gated in both halves: //tools/readmodel:engine_agreement_test compares the two engines row for row over spec’s corpora, and check_wiring.py §2a recomputes the read point from the corpus itself. So the divergence is measured rather than assumed, and a stale payload fails rather than sits.

Prefer the macro: it needs no Python environment, it runs the engine that decides the gates, and it is the path that will not be retired.

3.3 The console deployment

One Vercel project per consumer. The environment is console/DEPLOY.md’s, plus the one variable that makes it theirs:

variable	value
SPEC_READMODEL_DIR	the directory of payloads from §3.2. Unset means this repository’s own corpus — a consumer console that forgets it renders the flagship’s requirements, which is why the CI step asserts both directions
GOOGLE_ALLOWED_DOMAIN	the consumer’s Workspace domain. Fails closed if unset; proved to refuse in console/test/google.test.ts
DATABASE_URL	the consumer’s own Neon, as spec_app — never the owner
SESSION_SECRET	its own, 32+ chars
SPEC_MACHINE_TOKEN_SECRET	its own, ≠ SESSION_SECRET, if its CI will post populations
SPEC_KERNEL_SUBS	its own kernel principals. Empty means nobody, deliberately

Then the migrations, as owner, from CI — console/db/migrations/ through db/migrate.mjs, followed by db/verify.mjs, which re-proves every refusal against the live database in a transaction it rolls back.

3.4 Populations, from the consumer’s CI

tools/evaluation/post_evaluation.mjs — dependency-free, copied into the consumer’s repository, run under a machine credential minted by the console operator. A count and a query fingerprint cross the wire; never SQL, never rows. A machine reports Examined; it may not report Passes (RFC-004a §4), and the console, the plugin and the database each refuse one separately.

3.5 Authoring, and promotion

Proposals go through the console’s door — POST /api/proposal (multi-op) or POST /api/proposal/op (the flat one-op form). Each gets a content address and an au:Verdict; nothing is edited in place.

Promotion is the consumer’s own copy of .github/workflows/promote.yml: export the log with a SELECT-only credential, re-materialize proposals.ttl, run the gates over the result, and open a PR a person merges. The corpus is generated (invariant ⑥) — the promotion PR is where a human sees what the log did to it.

---

4. What is not built

Named because a consumer will hit these, and finding out by hitting them is worse than reading it here.

• No npm package for the read model. RFC-003 §10 names it; the console still imports payloads by path. SPEC_READMODEL_DIR is the seam that makes a per-tenant build possible without one — it is not the packaged handoff.
• The emitter is rdflib, the gates are ARQ. Closed for the consumer path: spec_readmodel runs the engine of record (§3.2). Still open for spec’s own committed payloads, which are emitted by the rdflib script — the two are compared row for row by //tools/readmodel:engine_agreement_test and currently agree, and switching spec over is the next step rather than this one.
• No provisioning automation. Every console is a Vercel project, a Neon database, a set of secrets and a migration run, done by hand.
• The domain gate’s refusal is proved as a RULE, not as a deployment. console/test/google.test.ts runs every branch, including a consumer account wearing the right address with no hd. No sign-in has been attempted from outside a hosted domain against a live deployment.
• One promoted proposal end to end — #52’s own done-bar — needs a real consumer repository, and is the step after this one.

from docs/crank-001-first-step.md

Crank-001 — the first measured reverse-diffusion step

Status: Result log · Companion to: RFC-001, RFC-001b Corpus (rough $G_0$): the 17 ratio competitive component specs + the ratio whitepaper + the positioning brief + RFC-001/001b + Ratio.Core (Lean). Method: one predict → project → gate → frontier pass, run as four parallel cloud-style agents (the predictor/corrector/gate stages plus a frontier stage that fanned out its own sub-researchers). This is the first turn of the crank described in RFC-001b §4 — not yet over the materialized Jena graph (Phase 0), but over the document corpus directly.

---

1. Measured energy snapshot $E(G_0)$

First measurement of the RFC-001b §3 energy terms over the rough corpus:

Term	Meaning	First measurement
$R$ redundancy	duplicated claims/edges	8 clusters (R1–R8); top-5 boilerplate sentences repeated 5–7× each
$C$ contradictions	claims that can’t co-hold	3 (C1–C3)
$D$ dangling	loose references / missing definers	5 (D1–D5)
$U$ under-spec	frontier (thin, ungrounded leaves)	~8 leaves, mappable to ~20 external standards
$L$ connectivity	meaningful typed edges	64 edges over 73 claims; 3 hub nodes
$S$ symmetry	MDL gain from collapsing isomorphic sub-graphs	7 motif templates cover all 16 component specs

The dominant signal: the corpus is highly symmetric and highly redundant (big recoverable $S$, big $R$), with a small but important contradiction set ($C$) concentrated on one overclaim, and a well-defined frontier ($U$) that is mostly groundable from open sources.

---

2. Predictor — claims & edges (the score step)

• 73 claims extracted (13 core/paper + 60 across the 17 components), each with RFC-2119 modality and a tier guess (Structural / Derivational / Implemented).
• 64 typed edges: 19 livesIn, 20 refines, 9 realizes, 16 dependsOn, 5 benchmarkedAgainst.
• Three hub nodes (highest centrality):
  1. core:2 — a transaction conserves value iff its net vector is zero (the sole invariant nearly every component refines/realizes).
  2. core:12 — CreateTransaction rejects non-conserving transactions (the single write-door every proposing component routes through).
  3. portfolio-accounting:3 — read-only ledger projections (dependency root for client-portal, CRM, BI, billing).

This is the connectivity backbone $L$: the graph is a near-star around conservation.

3. Corrector — projection targets (the deterministic step)

The 16 specs are one document orbit that collapses to 7 parametrized motif templates (this is the bankable symmetry $S$):

Motif	Template	Members
M1 propose → kernel admits	\proposeadmit{proposer}{artifact}{check}{records?}	trading, billing, compliance, proposal, model-mgmt, integrations, ai-insights
M2 sandboxed sim over kernel	\simover{states}{facts}{output}	proposal-generation, risk-analytics
M3 read-only projection	\readproj{surface}{audience}{guarantee}	portfolio-accounting, client-portal, BI (+read sides)
M4 extension over gRPC API	\extension{app}{lang}{holds}	crm, integrations, client-portal, connectors
M5 typed facts / fact plane	\factplane{external-data}	data-aggregation, alts, risk-analytics
M6 conserved-dimension generalization	\dimension{asset-line}{new-dims}	alts, specialized-servicing, portfolio-accounting
M7 content-addressed artifact	\cca{artifact} (cross-cutting)	model-mgmt, billing, compliance, data-governance, …

• Redundancy clusters R1–R8 deduped to canonical forms (e.g. R1 “admission runs through the kernel / can never produce an unbalanced book” appears verbatim in 5 specs → one M1 sentence; R7 the boilerplate statusbox is identical in all 16 → hoist to _preamble.tex).
• Transitively-reducible edges E2–E7 dropped (e.g. billing → portfolio-accounting is implied by billing → M1 → kernel).
• Compaction estimate: 16 specs → 7 templates + 16 thin parameter tuples; only portfolio-accounting and data-governance keep a small bespoke remainder. $R$ falls steeply, $S$ rises steeply, meaning-preserving.

4. Gate — tensions (what blocks the manifold $\mathcal{M}$)

15 tensions: 3 contradictions, 2 modality conflicts, 4 term-drift, 5 dangling. The cross-cutting pattern: the conservation theorem is being silently widened to cover properties it does not prove. Resolve first — C1 + D2 together:

• C1 (overclaim): the positioning brief says an LLM “cannot write an unbalanced or unauthorized entry,” but the kernel’s sole proven invariant is conservation; authorization is not a kernel theorem. The guarantee rides on a proof it doesn’t have.
• D2 (missing definer): the authorization claim is grounded only in specs/components/security/ specs that are referenced but absent from the corpus.
• Fix: either (a) scope the marketing guarantee to conservation only, or (b) admit the security specs and prove an authorization invariant the kernel actually enforces. (This is a real correction to our own ratio marketing copy.)

Other notable: T1 term-drift “trusted core” vs “proven kernel” vs “trusted computing base” (pick one canonical definer); T3 “claim” means both the prose assertion and the graph primitive — will collide at Phase-0 ingest, so name them apart now.

5. Frontier — standards to internalize ($U$ → groundings)

~8 under-specified leaves map to external standards; most are OPEN-licensed (per the RFC-001 §7.1 licensing gate). Highest-value, all OPEN:

Leaf	Standard	Body	License
NAV / fund pricing	Investment Company Act Rule 2a-4 / 22c-1 (17 CFR 270)	SEC	OPEN (public domain)
Fair-value valuation	FASB ASC 820 (IFRS 13 convergent)	FASB	OPEN (Basic View, free reg.)
Performance returns (TWR/MWR)	GIPS 2020	CFA Institute	OPEN-to-read (copyrighted)
Tax-lot / cost basis	IRC §1012, §6045 + Treas. Reg.	IRS/Treasury	OPEN (public domain)
Books & records / compliance	17 CFR 275.204-2, 206(4)-7	SEC	OPEN (public domain)
Alt-investment valuation	IPEV Guidelines 2025	IPEV Board	OPEN (free PDF)
API / HTTP layer	RFC 9110 / 9113 + gRPC	IETF / CNCF	OPEN
Identifiers	FIGI (OMG), LEI (ISO 17442 data)	OMG / GLEIF	OPEN (data)
Content hashing	FIPS 180-4 / 202 (SHA-2/3)	NIST	OPEN (public domain)
Money arithmetic	IEEE 754-2019	IEEE	PAYWALLED (metadata-only)
Risk (VaR/ES)	Basel/FRTB (open) · ISO 31000 (paywalled)	BCBS/BIS · ISO	mixed

Recommended first internalization: SEC Rule 2a-4 (NAV) — open, public-domain, load-bearing for the valuation/P&L dimensions, and the exact “Wikipedia → standard” path from RFC-001 Appendix A.

6. Next reverse step (the prioritized action queue)

1. Project (deterministic, safe): collapse the 16 specs to the 7 M-templates; dedupe R1–R8; drop E2–E7. Banks $S$, cuts $R$ — no semantic risk.
2. Gate-fix (highest priority): resolve C1+D2 (scope the authorization claim or add+prove a security invariant); disambiguate T3 “claim” before Phase-0 ingest.
3. Frontier: internalize SEC Rule 2a-4 (NAV) first, then FASB ASC 820 and GIPS — all OPEN; formalize via the RFC-001 §6 normative-document track.
4. Materialize: feed these claims/edges as the seed for Phase 0 (the Jena graph), so subsequent cranks measure $E(G)$ over the real graph, not the corpus.

7. Provenance & reproducibility

Four agents, run in parallel; each read the corpus read-only and returned structured, mergeable output (claims keyed by <slug>:<n> for dedup). Re-running is cheap and convergent because claim identity is content-addressable (RFC-001 §3.1). Counts here are this pass’s measurement, not a fixed ground truth; the next crank should move them monotonically (more $S$/$L$, less $R$/$C$/$D$/$U$) — the $E(G)$ descent of RFC-001b §6.

from docs/crank-proof.md

Proving the crank works (and isn’t fooling itself)

The crank’s claim: an agent fleet proposes graph edits; the deterministic corrector + gates keep the result sound; and the result raises the Spec Score on a real spec. The danger with any LLM-in-the-loop system is that the number goes up because the model gamed the metric, not because the spec got better. So this proof is built to be hard to fake — the LLM is treated as an adversary.

It separates two questions: (1) is the loop sound and un-gameable? (2) is the LLM reliable at it? This is the existence proof for (1), with zero API spend — a real but hand-written Lean proof stands in for the fleet’s proposal. (2) is the statistical question that follows once the real proposer is wired.

The principle: “proven” is machine-checked

Grounding is the score’s biggest lever (weight 0.45), and the cheapest fake is to slap :provenBy "Ratio.Lemma.Foo" on a claim with no proof. So the rule is:

A claim counts as grounded only when a sorry-free Lean theorem backs it.

No LLM output can fake a compiling Lean proof of a false statement, so the only way the score rises is a real proof.

The existence proof

• A real proof — lean/Spec/Grounding/WriteDoor.lean proves trades_compose_conserving (a rebalance of conserving trades conserves, so it passes the kernel write-door). //lean:grounding_test compiles it, sorry-free.
• Wired to a real claim — RFC-0903 trading-1 now carries :provenBy "Spec.Grounding.WriteDoor.trades_compose_conserving".
• The score moved, for a verified reason — proven claims 2 → 3, grounding 0.105 → 0.158, Spec Score 32.4 → 34.8 (crank/spec-score.tsv, crank 003).

The controls (what makes it a proof, not a demo)

Control	Target	What it shows
Grounding gate + negative control	//grounding:grounding_verified	every in-repo :provenBy resolves to a sorry-free theorem; a fabricated :provenBy is rejected. The score’s grounding term is un-gameable.
Adversarial gate-rejection	//grounding:adversarial_gate	the consistency gates detect a planted dependsOn cycle, dangling reference, and MUST/MUST_NOT contradiction; a clean DAG trips none. The gates reject, they aren’t decorative.
Corrector ablation	//corpus:compaction_measure	the corrector removes 4 transitively-implied edges (dependsOn 20 → 16) — without it, that redundancy survives and the energy is worse. It earns its keep.

Soundness is a gate, not points: a red gate voids the score rather than lowering it, so the fleet can’t bank maturity on an unsound graph.

What this proves — and what it doesn’t

Proven: the loop is sound and the score is un-gameable. A claim’s grounding counts only when Lean says so; unsound deltas are rejected; the corrector reduces real redundancy; and a verified grounding moves the real, graph-measured score.

Not yet proven: that an LLM can produce such proofs reliably. That’s the next step — swap the hand-written WriteDoor.lean for a real proposer (an ANTHROPIC_API_KEY call), run it N times on a real under-specified leaf, and report the success rate (proposals that pass the gates and yield a compiling proof). The harness above is exactly what that proposer plugs into — the existence proof shows the rails are real before the first token is spent.

Run it

bazel test //lean:grounding_test //grounding:grounding_verified //grounding:adversarial_gate
bazel build //crank:spec_score && cat bazel-bin/crank/spec-score.snapshot.tsv

from docs/grounding-authoring-roadmap.md

Grounding authoring — issue-ready roadmap

Companion roadmap for #54. Each section below is scoped to become one GitHub issue.

The boundary

Two systems are deliberately separate:

• The decomposer reads an author’s backticks and emphasis and identifies the terms a requirement depends on. It never decides what a term means.
• The project Probe adapter evaluates candidate locators inside the project’s environment. It can return counts, fingerprints, caveats, and transit-only examples without giving spec access to project data.

A locator remains opaque to spec. The console must not invent a SQL-like grammar or imply that a visually assembled expression is valid unless the project adapter supplied and accepted its structure.

Dependency order

1. Shared composer over known bindings
2. Installable project connector bootstrap
3. Declarative adapter model
4. Visual adapter authoring studio
5. Project catalog search contract
6. Probe candidate comparison
7. Binding evidence in the proposal vocabulary
8. Reference adapter and conformance kit
9. Deterministic catalog matcher
10. Grounding interviewer
11. Accessibility and interaction coverage

Items 1, 4, and 11 are console-owned. Items 2–3 and 5–8 define the consumer boundary. Item 9 must precede item 10 so an agent is measured against the deterministic baseline.

---

Issue: Shared visual grounding composer

Goal

Replace duplicated free-text locator fields with one component that supports search, reuse, exact-entry fallback, and future adapter candidates.

Scope

• Add a shared GroundingComposer.
• Autocomplete from existing bindings in the selected project.
• Display which terms already use a locator.
• Keep free text as an explicit advanced fallback.
• Accept adapter candidates through a stable display type carrying optional count and caveat fields.
• Use the component from requirement and term grounding flows.

Done means

• Both grounding entry points render the same component and submit the same bindTerm op as before.
• Choosing an existing binding requires no locator retyping.
• The component never parses or executes a locator.
• Empty, loading, read-only, and submission-error states remain distinguishable.

---

Issue: Ship an installable project connector bootstrap

Goal

Replace “build and host a grounding adapter” with a standard runtime a project can install in its own trust boundary. The bootstrap provides connectivity and catalog introspection; the project still authors what the adapter means in the visual studio below.

Scope

• Publish a small connector runtime for a serverless function or container.
• Read a versioned .spec/grounding.yaml adapter model from the project repository.
• Keep database credentials and query execution entirely inside the project.
• Expose health, catalog suggestion, and Probe routes.
• Authenticate console calls with audience-scoped OIDC rather than a copied long-lived token.
• Provide framework presets for Next.js, Node, and a standalone container.

Done means

• A sample project can install the connector without importing spec’s ontology or protobuf model.
• The connector starts from one manifest and project-owned environment credentials.
• No customer row, SQL statement, or database credential is stored by spec.
• The same conformance suite runs against every preset.

---

Issue: Define the declarative grounding adapter model

Goal

Make the adapter a reviewable project artifact rather than custom endpoint code. The model says what project concepts exist and how to measure them; a standard runtime supplies the HTTP behavior.

Model

• Data source references: names and driver kinds only. Credentials stay in project environment variables and never enter the model.
• Resources: project-recognizable entities backed by allowlisted tables, views, API collections, or permission catalogs.
• Fields: label, type, sensitivity, searchability, and whether a field may appear in transit-only examples.
• Relationships: allowlisted joins between resources, with cardinality made explicit.
• Referents: stable IDs with human labels and a typed expression tree over resources, fields, relationships, operators, and parameters.
• Suggestion metadata: aliases, descriptions, owner, deprecation state, and business vocabulary used by catalog search.
• Probe policy: count ceiling, timeout, example limit, and redaction rules.

Expression constraints

• Store a typed AST, never free-form SQL.
• Permit only driver-supported operators.
• Parameterize every value.
• Require explicit joins from the relationship allowlist.
• Compile and execute only inside the project connector.
• Give every compiled query a reproducible fingerprint.

Done means

• JSON Schema validates the complete adapter model.
• Invalid fields, joins, operators, and secret literals are refused before deployment.
• Postgres and static-catalog fixtures compile the same referent AST deterministically.
• The model contains no credential, customer row, or executable free-form query.
• Model diffs are understandable in an ordinary project pull request.

---

Issue: Visual grounding adapter authoring studio

Goal

Let a project owner define what the adapter is and does without writing code, SQL, protobuf, or environment-variable plumbing.

User flow

1. Choose a connected project data source.
2. Import its schema metadata and select the resources the adapter may see.
3. Rename technical resources and fields into recognizable project language.
4. Mark sensitive fields and choose the small subset safe for transient examples.
5. Define relationships by selecting source field, target resource, and target field.
6. Create a named referent with a visual condition builder: Resource → relationship → field → operator → parameter/value.
7. Preview the generated human-readable meaning, candidate count, fingerprint, and redacted examples.
8. Save a draft, test every referent, then create a project-side manifest PR.

Component model

• DataSourcePicker
• ResourceCatalog
• FieldPolicyEditor
• RelationshipBuilder
• ReferentBuilder
• ConditionGroup with nested AND/OR groups
• ProbePreview
• AdapterReadinessChecklist

The same typed expression editor should be used when a grounding author creates an ad hoc candidate. The adapter studio saves reusable named referents; the grounding composer selects or specializes them.

Done means

• A user can author a multi-condition referent with one allowlisted relationship using only pointer or keyboard controls.
• Field and operator choices are type-aware and autocomplete from imported catalog metadata.
• Every edit can be previewed without persisting customer rows.
• Saving creates a deterministic .spec/grounding.yaml change in the project repository.
• Reopening the model reconstructs the visual form byte-for-byte.
• Advanced users may inspect the manifest but never need to edit it manually.

---

Issue: Point-and-click project data connection and authoring wizard

Goal

Let a project owner install the runtime and open the adapter authoring studio using recognizable product language rather than an environment variable named GROUNDING_ADAPTER_URL.

User flow

1. Open Settings → Connect project data.
2. Choose the project repository and connector preset.
3. Choose a project-owned data source.
4. Open the adapter studio to select resources, describe relationships, and author named referents.
5. Review the privacy boundary: metadata, counts, fingerprints, and optional transit-only examples.
6. Click Create connector PR.
7. After that PR deploys, click Test connection and see each capability verified separately.

Scope

• Add connection states: not connected, installing, deployed, authenticated, catalog ready, Probe ready, and degraded.
• Generate the connector bootstrap and empty adapter model from wizard choices.
• Launch the visual authoring studio against catalog metadata returned by the project-side connector.
• Use a GitHub App to open the project-side PR; the console never writes project code directly.
• Verify health, OIDC audience, Suggest, positive Probe, zero handling, and example redaction.
• Store non-secret connection metadata per console deployment; keep project credentials project-side.
• Retain an advanced “connect an existing endpoint” path for teams that already run an adapter.

Done means

• A project owner completes setup without writing an adapter or manually copying a secret.
• Every wizard step is resumable and names the next blocked action.
• “Connected” means the signed Probe handshake succeeded, not merely that a URL exists.
• Removing the generated project manifest disables the connector without leaving a credential behind in spec.

---

Issue: Add project-owned catalog search for schema-backed autocomplete

Goal

Let a person search recognizable project concepts instead of guessing textual locators.

Scope

• Define a Suggest contract separate from Probe.
• Request fields: term surface, requirement context, user query, and result limit.
• Response fields: human label, opaque locator, kind, safe description, and optional deprecation/caveat metadata.
• Keep customer rows out of this response; it is catalog metadata only.
• Proxy through the console so adapter credentials never reach the browser.

Done means

• Search returns deterministic, ranked catalog entries from a fixture adapter.
• The console merges catalog entries with existing bindings and clearly labels their source.
• An unavailable adapter produces a named unavailable state, never an empty result.
• A zero-result search is visibly different from adapter failure.

---

Issue: Compare candidate readings with Probe

Goal

Turn “what does this point at?” into a choice between measured populations.

Scope

• Send selected candidate locators to POST /api/ground/probe.
• Render count, query fingerprint, caveat, and transit-only display examples.
• Compare candidates side by side.
• Refuse to present count zero as a valid binding.
• Discard examples when the view closes; do not place them in proposal state, logs, telemetry, or durable agent storage.

Done means

• A person can select a positive-population candidate and see exactly what will be proposed.
• Zero renders as Vacuous and cannot be submitted as Examined.
• 400 (no proposed reading), 502 (unreachable), 503 (unconfigured), zero, and a positive result each have distinct UI states.
• Conformance fixtures prove examples never enter persisted types.

---

Issue: Carry measured binding evidence through the proposal door

Goal

Make an adopted binding distinguishable from an unmeasured guess.

Scope

• Add optional locator, population, and query_fingerprint fields to bindTerm in TypeScript and Rust.
• Preserve the closed 17-operation vocabulary.
• Include evidence in canonical proposal bytes and promoted TTL.
• Require server-observed Probe evidence for measured bindings; the browser or an agent may not type population or fingerprint values.

Done means

• TypeScript and Rust accept and address identical proposal bytes.
• Replayers and materialization retain the evidence.
• A fabricated count or fingerprint is refused.
• Existing unmeasured bindings remain readable and are explicitly labeled unmeasured.

---

Issue: Ship a Probe reference adapter and conformance kit

Goal

Give each consumer a runnable implementation boundary rather than only a proto.

Scope

• Fixture-backed Suggest and Probe handlers.
• Audience-scoped OIDC verification.
• Timeout, redaction, and safe-example guidance.
• Consumer-side conformance tests for positive, zero, unavailable, and malformed responses.
• Example deployment and environment configuration.

Done means

• A consumer can implement the contract without granting spec database access.
• The reference adapter passes the same response fixtures as the console proxy.
• Authentication failure, adapter failure, and no-match are mechanically distinct.
• /api/health reports configured only when the integration is usable.

---

Issue: Deterministic binding catalog before agent assistance

Goal

Dispose of exact-match permission tokens and schema identifiers without an LLM.

Scope

• Build a catalog from project-provided permission and schema identifiers.
• Exact matching only; no fuzzy semantic claims.
• Produce a reviewable batch of bindTerm proposals.
• Rank unmatched terms for manual work.

Done means

• Every generated binding names its catalog source.
• A human can review the batch before it reaches the door.
• Re-running against the same inputs is byte-identical.
• The residual queue becomes the measured baseline for any grounding agent.

---

Issue: Grounding interviewer for residual business language

Goal

Ask focused questions only where catalog search and deterministic matching lose.

Scope

• Read requirement context and suggest candidate locators.
• Probe before proposing.
• Park for human approval on every write.
• Keep examples out of model and durable workflow state.
• Expose no tools for requirement authoring, evaluation, or conflict resolution.

Done means

• A probe returning zero cannot reach bindTerm.
• Population and fingerprint are copied server-side from Probe state, never model-authored.
• Click and conversational flows produce the same proposal address.
• Evaluation shows the interviewer beating ranked autocomplete on the residual queue; otherwise it is not shipped.

---

Issue: Component and accessibility coverage for grounding

Goal

Make the shared interaction safe to evolve.

Scope

• Add DOM tests for autocomplete keyboard navigation and free-text fallback.
• Test busy, success, failure, read-only, and adapter-unavailable transitions.
• Test requirement and term entry points against the same behavior suite.
• Verify focus restoration, labels, announcements, and narrow layouts.

Done means

• Keyboard-only users can search, inspect, select, and submit a locator.
• Screen readers announce candidate source, population, caveat, and disabled reason.
• No component maintains a second copy of proposal lifecycle state.
• CI catches drift between the two grounding entry points.

from docs/phase-0-materialization.md

Phase 0 — the ratio spec corpus, materialized as a gated graph

Status: Done (slice 1) · Companion to: RFC-001, RFC-001b, crank-001

The crank-001 measurements were computed by agents reading prose. Phase 0 turns the corpus into an actual graph: every claim, edge, and hub now has a triple behind it, loaded into Jena, validated by SHACL, gated by the consistency invariants, and measured by SPARQL — so subsequent cranks descend E(G) over real data, not estimates.

What landed

• Seed graph — corpus/ratio-corpus.ttl: the conservation kernel + the 16 advertised components as :Documents / :NormativeStatements in the shared vocabulary (rdf/ontology/aion-rfc.ttl). No new vocabulary was needed — the existing Aion RFC ontology + gates already speak claims, modalities, and dependsOn/refines edges, and its semantic lints (claim-contradiction, modality-conflict, dead-depends-on, grounding, term-drift) map onto the E(G) terms.

• Gates green — //corpus:ratio_corpus_gates_*: SHACL conformance + the four consistency invariants (dangling refs, dependency cycles, diagnostic-code collisions, asymmetric inverse edges) all pass over the real graph.

• Measured E(G) — //corpus:eg_measure (bazel build → bazel-bin/corpus/eg_measure.tsv), read off the graph:

  metric	value
  documents	17
  claims (NormativeStatements)	19
  dependsOn / refines / containsRule edges	20 / 1 / 19
  conservation-hub (RFC-0900) in-degree	13
  read-projection-hub (RFC-0901) in-degree	5
  MUST / MAY / MUST_NOT	16 / 2 / 1
  proven (provenBy)	2

  The near-star crank-001 estimated is now quantitatively confirmed: the conservation hub dominates connectivity.

• First frontier standard internalized — corpus/nav-sec-2a4.ttl: SEC mutual-fund NAV (17 CFR 270.2a-4 / 22c-1 / 2a-5; §2(a)(41)) as 19 :NormativeStatements with modality, citation, and verbatim :evidence, linked into the corpus via :references (portfolio-accounting, alternative-investments). The combined //corpus:corpus_standards_gates_* pass (the internalization edges resolve); //corpus:standards_measure: 38 total claims, 18 documents, 8 with verbatim evidence, 2 components grounded. Source research: docs/frontier/nav-sec-2a4.claims.json.

• Topology from SPARQL — //corpus:corpus_edges reads the graph’s typed edges straight from the store: the data a SPARQL→dot renderer turns into the hero graph (the “deck is an output of the pipeline” step).

What’s next

1. tsv → dot render: format //corpus:corpus_edges output as .dot and dot_pdf it, so the hero graph regenerates from the graph (mechanical).
2. Deterministic compaction (RFC-001 §5): symmetry detection + redundancy collapse (16 → 7 motifs) over the graph — the corrector pass; the before/after E(G) drop becomes graph-measured.
3. NAV → theorems (RFC-001 §6): materialize each NAV :NormativeStatement as a :Theorem (normative-is-theorem.rule) and turn the JSON depends_on into :premise/:derivedVia so grounding is checkable.
4. uslm bridge: IRC tax-lot (§1012/§6045, Title 26 USC) is internalizable via the uslm legislative-KG vertical today; CFR Title 17 (NAV) is regulation, so it stays on the §6 document track for now.

from docs/releasing.md

Releasing spec

Spec is a Bazel module before it is anything else: the corpus gates, the authoring vocabulary and the fanout derivation are all consumed by other repositories through bazel_dep(name = "spec", ...). A release is therefore not “we tagged it” — it is “a consumer can resolve it”, and those have been different things twice.

What went wrong the two times it went wrong

Both were invisible from inside this repository, and both shipped green:

• #58 — rules_shell was declared dev_dependency = True. Dev deps are dropped from every module graph but this one’s, so sh_test resolved here and nowhere else. The first external corpus got No repository visible as '@rules_shell'.
• #59 — use_extension(..., isolate = True) on the crate extension. The usage was dev-scoped, but Bazel rejects the keyword before it considers the scope, so a consumer’s module graph failed to compute at all — with an error naming an experimental flag and not spec.

Neither is a subtle bug. Both are simply unreachable from the position this repo’s own CI stands in, which is why the checklist below ends where it does.

The checklist

1. Merge to main, green. The gate job builds the working tree; the consumer job builds smoke/consumer twice — once against the published pin, once against the commit under review. The second is what catches a consumer-visible break before it is published.

2. Bump module(version = ...) in MODULE.bazel if main is not already at the version you intend to publish.

3. Simulate the registry ratchet before tagging. tomato-bazel/gate blocks any new module version that makes D2 (undeclared toolchain leak), D3 (unnamespaced repo chosen on a shared extension) or C1 (atom multi-version) worse. There is no override and admins are not exempt, so a ratchet failure discovered after tagging means a new version rather than a fixed one. Run the gate at the ref gate-ratchet.yml pins, over a staged registry carrying the proposed MODULE.bazel.

   The three questions worth asking by hand first, because they answer most cases in a minute:

   • Did a bazel_dep move from dev_dependency = True to non-dev, or a new non-dev one appear? That changes what consumers resolve.
   • Does any new tag on a foreign extension pass an explicit name =? That is what D3 means by “chose” — a python.toolchain(python_version = ...) chooses nothing and is fine; an oci.pull(name = "distroless_static") is the exact bug D3 exists for.
   • Does a module in the registry depend on spec? If so, a new selection here can silently upgrade what it resolves.

4. Tag and push vX.Y.Z on the merge commit.

5. Publish to tomato-bazel/bazel-registry: modules/spec/X.Y.Z/MODULE.bazel (a copy of the tag’s), modules/spec/X.Y.Z/source.json (the sha256 of the GitHub tag tarball, base64, as integrity), and the version appended to modules/spec/metadata.json. Regenerate the README with its own tool rather than by hand. Land it as a PR — the real ratchet runs there.

   ⚠ That repository is shared and often parked on someone else’s branch. Check git branch --show-current before committing, or work from a worktree off origin/main.

6. Bump the smoke pin. smoke/consumer/MODULE.bazel moves to the version you just published, and CI’s first consumer step resolves it from registry.tbzl.dev for real. This is the step that proves the release exists, and it is deliberately last: until the registry entry is live, the pin cannot resolve, so a green consumer job after the bump is the release verifying itself.

   For v0.7.0 this had to be done by hand, in another repository, by a person who thought to try. That is the gap the smoke module closes.

Known-flaky, not your change

• “warm the tectonic cache” fails with 429 — the LaTeX bundle CDN (fullyjustified.net) rate-limiting the org, not the PR. Reruns feed the limiter; back off before retrying. The Actions cache added in #62 converges across attempts because a partial download is still saved, but the cache is branch-scoped, so main starts cold until one run gets through.
• A network error naming registry.tbzl.dev in the consumer job is the Fastly CDN, not the release. Bazel only falls through registries on a 404, so a mirror second in line would not absorb an outage.

from docs/rfc-001-unified-spec-graph.md

RFC-001 — The Unified Spec Graph

Status: Draft · Spine: spec · Depends on: decomposer, mycelium, agora Author: (scaffold) · Date: 2026-06-26

Crystallize a vision — or a normative standard — into a proven, compact, self-extending knowledge graph, by alternating stochastic refinement (cloud agents) with a deterministic, machine-checked projection.

---

1. Motivation

fastverk has, independently, built almost every piece of a system that can turn prose into a verified semantic graph — but the pieces live in three repos with three overlapping copies of five things:

Concern	spec / @spec	agora	mycelium
Graph store / reasoner	Jena 5 + kg.Loader (inference)	Jena (in CompositeMergeFn)	Jena (in kg_research spike)
Claim model	Spec.Corpus.Schema (Modality, Tier), :NormativeStatement	decomposer.v1.Claim + agora.v1.Fragment + graph.proto	kg_research claim:contradicts
Grounding vocabulary	rules_rdf gates	OntologyValidator (schema.org TSVs)	Wikidata Q-IDs
Content-addressing	md5(rfc|section|predicate)	claim.hash, ClaimCache	sha256(sparql)
Gates / validation	kg.GateHarness, rdf/lint/semantic/*.rq	SidecarDeriveGateFn	—

Three Jenas, three claim schemas, three hashes. The spec library “doesn’t scale” not because anything is missing, but because there is no single spine: no one canonical claim identity for parallel agents to dedupe against, no one ontology for the deterministic optimizer to canonicalize, no one gate harness.

This RFC unifies the three behind spec as the spine, adds the one genuinely missing capability — a deterministic projection kernel — and shows how the result turns “improve the spec library” into a single, formal, scalable loop.

---

2. The crystallization model (diffusion)

Refinement is modeled as a diffusion / denoising process over a graph G.

Forward (noising) operator — decompose. A vision narrative (or a normative document) is exploded into a cloud of atomic, content-hashed claims — high entropy: redundant, loosely linked, locally contradictory. This is the seed graph G₀.

Reverse (denoising) step — two alternating halves:

1. Stochastic score step (cloud agents): propose links, merges, rewrites, and new claims (agora: ClaimPropose → CompositeMerge → Ensemble → Verify). This is the learned sampler — it guesses the direction of lower energy.
2. Deterministic projection step (the new kernel): exact, idempotent passes that project G onto the coherent manifold — dedup by content hash, transitive reduction, symmetry/automorphism collapse, canonical normal form. Entropy-non-increasing and replayable, the way the ratio kernel is.

The alternation is annealed Langevin / proximal-gradient: noisy explore, then project to the constraint set, repeat at a falling temperature.

Energy descended (“make it better”):

E(G) = w1·R + w2·C + w3·D + w4·U  −  w5·L − w6·S
       └─── entropy ───┘             └── order ──┘
  R = redundancy        L = meaningful connectivity
  C = contradictions    S = symmetry compression (MDL gain)
  D = dangling links / loose threads
  U = under-specification (frontier)

• Stochastic steps mostly cut C, D, U and add L.
• Deterministic steps provably cut R and bank S (a symmetry is a compression — Occam / minimum description length).
• Crystallized = a fixed point of the loop: a compact, strongly-linked, contradiction-free canonical graph. Lower E ⇒ a better spec.

Temperature schedule = ensemble tiering. Early steps are hot/broad (agora’s Haiku×2 breadth, many parallel trajectories); late steps are cold/precise (Sonnet→Opus verify, then the deterministic projection).

Reproducibility (“never lose the thread”). Every claim is content-addressed and every projection pass is deterministic, so the whole narrative → crystal trajectory replays bit-for-bit — and parallel cloud trajectories never collide, because they dedupe through the content-addressed ClaimCache.

---

3. Unified architecture: one spine, three jobs, no cycles

Make spec the spine — it already hosts Jena + the Lean spec framework + the gates. Each repo gets exactly one job and a single dependency direction:

decomposer ──▶ spec ──▶ mycelium
   (forward     (SPINE)      (grounding service:
    operator)      │          implements spec's
                   ▼          GroundingService iface)
                 agora
            (pipelines + cloud fan-out + frontier)

• decomposer — the forward/noising operator only: decompose(nl) → List<Claim>, each Claim{hash, raw, index} content-addressed. Leaf dependency.
• spec (SPINE) — owns:
  • the one canonical Claim/Graph ontology (authored in Spec.Corpus.Schema Lean, emitted to TTL via Spec.Emit.TtlEmit — the ontology is itself Lean-defined and proven);
  • the one gate harness (kg.GateHarness + rdf/lint/semantic/*.rq);
  • the Lean proofs (Spec.Kernel, Spec.Axioms, kg.lean.{GenerateProofs, ValidateProofs, ProvenBySyncCheck});
  • the new deterministic projection kernel (§5).
• mycelium — promoted from Wikidata-accessor to the grounding service: implements a GroundingService interface defined in spec (“does IRI X ground? what is its canonical Q-ID anchor?”), absorbing agora’s schema.org OntologyValidator so there is one grounding tier.
• agora — the pipelines: the Beam decompose → propose → merge → ensemble → verify → gate flow, the content-addressed ClaimCache, the research_closure frontier BFS, and the Beam→Dataflow + RunPod cloud fan-out. Consumes spec’s ontology/gates/projection and mycelium’s grounding — drops its private copies.

This resolves the source-of-truth question: RDF/Jena in spec is the store; graph.proto is the wire format between the Rust projection passes and Beam (exactly what agora’s sidecar already does); mycelium is the grounding tier.

3.1 Seams (contracts that make it one system)

1. One Claim/Graph schema. Spec.Corpus.Schema is canonical (Lean → TTL + proto). decomposer.v1.Claim is its forward-op subset; agora.v1.Fragment / graph.proto import it; kg_research’s claim:contradicts merges in.
2. One grounding service. spec defines GroundingService; mycelium implements it (Wikidata + schema.org closures under one API); agora wires it into gates.
3. One content hash. Standardize on the decomposer canonical claim hash for ClaimCache, the projection passes, and replay. (mycelium’s sha256(sparql) stays internal to its Wikidata cache.)
4. One gate harness. All validation — grounding, contradiction, modality conflict, dangling, and the new canonical-form gate — runs through kg.GateHarness, callable from agora’s DeriveGate and from CLI.

3.2 Migration deltas (what moves)

• Consolidate the claim/graph schemas into Spec.Corpus.Schema (+ a thin graph.proto profile). agora and decomposer import rather than redefine.
• Lift agora.OntologyValidator grounding into mycelium’s GroundingService.
• Point agora.ClaimCache and the projection at the one canonical hash.
• Generalize aion-rfc.ttl → a normative ontology that aion-rfc becomes a profile of (§6).

---

4. Reuse vs. build

Diffusion role	Component	Status
Forward / noising	decompose(nl) → List<Claim>	exists (@decomposer)
Stochastic reverse	ClaimPropose → CompositeMerge(Jena) → Ensemble → Verify	exists (agora)
Grounding / guidance	mycelium (Q-IDs) + schema.org closure	exists
Gates	kg.GateHarness, rdf/lint/semantic/*.rq, DeriveGate	exists
Reproducible, parallel-safe	ClaimCache (content-addressed)	exists
Parallel trajectories	Beam fan-out → RunPod vLLM autoscale	exists (DirectRunner; Dataflow-ready)
Frontier expansion	research_closure multi-hop BFS	exists (re-point at standards)
Crystal store + Lean proofs	spec (Jena + Lean + CorpusToLean + emit)	exists
RFC formalization	Schema.lean (Modality, Tier), aion-rfc.ttl, normative-is-theorem.rule	exists (Aion RFCs)
Deterministic projection kernel	symmetry / redundancy / compaction + E(G)	← build (§5)
Typed spec ontology edges (refines / dependsOn / conflictsWith / realizes / livesIn…)	extend Schema.lean	← build
External normative-doc ingest	mycelium front-end (§6)	← build
Internalize gate (relevance + licensing)	new gate (§7)	← build

The spine is ~70–80% built. The new work is the provable reverse-diffusion kernel, the typed ontology, and the ingest/discovery front-end.

---

5. The deterministic projection kernel

The novel contribution: a set of deterministic, meaning-preserving graph transformations that lower E(G) and are machine-checked. Per the chosen hybrid implementation:

• Lean-proven core (Spec.Kernel / a new Spec.Graph.Projection): the invariants — each pass is (a) meaning-preserving (the quotient/rewrite admits a graph homomorphism back to the original modulo the collapsed symmetry) and (b) entropy-non-increasing (E after ≤ E before). These mirror ratio’s conservation theorems: a small proven core relied on forever.
• Rust passes (emitted/aligned with the Lean spec, run via the graph.proto sidecar) for the hot path:
  1. Content-hash dedup — identical claims (same canonical hash) collapse to one node; provenance edges union.
  2. Transitive reduction — drop A→C when A→B→C exists for transitive edge types (dependsOn, refines).
  3. Symmetry / automorphism detection — find isomorphic claim sub-graphs (e.g. the “control-plane proposes → kernel checks” motif recurring across trading / billing / compliance) and collapse each orbit into one parametrized template node, banking the MDL gain S.
  4. Canonical normal form — a deterministic, replayable serialization so two runs over the same claim set produce byte-identical graphs.

E(G) is computed by SPARQL over Jena (the rdf/queries/* and rdf/lint/* families already compute most terms: dangling-references.rq → D, claim-contradiction.rq/modality-conflict.rq → C, dependency-graph.rq → L). The kernel reports E before/after each step so progress is measurable.

---

6. Normative-document formalization track

Point mycelium at RFC / ANSI / IEEE / ISO / SEC documents and fully formalize them.

The spine already formalizes Aion’s own RFCs: each :NormativeStatement is materialized as a :Theorem (normative-is-theorem.rule), grounded, and discharged at a Tier (Structural / Derivational / Implemented). Generalizing to external normative documents is an ingest + ontology-profile job, not a new engine.

Pipeline (per document):

1. Fetch (mycelium front-end): retrieve the document (IETF RFCs are open; see §7 on licensing for ANSI/IEEE/ISO).
2. Segment → sections, with SectionKind (Normative / Definitions / Grammar / …) from Schema.lean.
3. Decompose each normative clause → content-hashed Claims, tagged with RFC-2119 Modality (MUST / MUST_NOT / SHOULD / MAY / …).
4. Propose → merge → ground (agora + mycelium): claims → RDF fragments, grounded against the normative ontology + Wikidata anchors.
5. Gate: claim-contradiction.rq, modality-conflict.rq, term-drift.rq, grounding.rq, dangling-references.rq.
6. Project (§5): dedupe, reduce, collapse symmetries, canonicalize.
7. Formalize: CorpusToLean emits Spec.Corpus.Schema-typed Lean; each NormativeStatement → Theorem; GenerateProofs / ValidateProofs discharge them up the Tier ladder; ProvenBySyncCheck keeps Lean ⇄ TTL in lockstep.

“Fully formalized” is defined operationally as: every normative statement is a Lean theorem, grounded, contradiction-free, and discharged at ≥ its target Tier. Because the Tier ladder is explicit, formalization is progressive and measurable (most clauses land Structural first; the frontier is the set not yet Derivational/Implemented) — not an all-or-nothing claim.

Ontology delta: generalize aion-rfc.ttl into a reusable normative ontology (:Document, :Section, :NormativeStatement, :Term, :Grammar, :CrossReference, …) with aion-rfc as one profile and ietf-rfc, ieee, iso, ansi as additional profiles (each adding its document-numbering

• section conventions).

The first profile landed in #50, inside aion-rfc.ttl rather than as a new ontology: rfc:documentProfile with rfc:RfcDocument (the default — RFC-NNNN numbering plus at least one section) and rfc:PlainDocument (any stable id the source already carries, sections optional). A requirements document now types as a :Document without a minted number, and DocumentShape validates each document against the profile it declares.

---

7. Discovery / frontier expansion

Wikipedia could have an article on “NAV calculation” that links to a standard, and we’d want to internalize that standard if it made sense.

This is research_closure’s multi-hop BFS, generalized: the frontier edges are no longer arXiv citations but Wikidata/Wikipedia → external-standard links, and each candidate passes an internalize gate before it is pulled in.

Loop:

1. Anchor a seed concept (e.g. wd: “net asset value”) via mycelium → its Wikidata/Wikipedia node.
2. Expand the frontier: follow cites / seeAlso / external-standard links (Wikidata properties like described by source, standards body) to candidate normative documents.
3. Internalize gate decides whether to pull each candidate in:
   • Relevance — does the candidate connect (within k hops) to a node already in the working graph / the active vision? (graph proximity + LLM judge).
   • Marginal E gain — would internalizing it lower E(G) (fill under-specification U, add connectivity L) more than it adds entropy?
   • Licensing — only documents we have the right to ingest (see below).
4. Formalize accepted documents via §6; loop.

This is exactly “advance the innovation frontier reliably without losing the thread”: the frontier is U (under-specification) in E(G); each accepted standard provably reduces it; everything is content-addressed and replayable.

7.1 Licensing constraint (important)

research_closure/the internalize gate must respect document licensing. IETF RFCs are freely usable. ANSI / IEEE / ISO standards are copyrighted and typically paywalled — the system may store metadata, citations, and our own formalized claims about a standard we are licensed to read, but must not redistribute the standard’s text. The internalize gate therefore carries a licensing predicate (mayIngestFullText / metadataOnly) and defaults to metadata-only for non-open sources. This is a first-class gate, not an afterthought.

---

8. Cloud-parallel execution

• Fan-out: Beam ParDo over claims/documents. DirectRunner today; the beam_pipeline_binary _deploy.jar is built to swap to Dataflow/Flink for true horizontal scale.
• LLM tier: rules_runpod serverless vLLM endpoints (gemma3 / Llama-3.x for decompose; Anthropic Haiku→Sonnet→Opus for propose/verify), with per-model rate limiters.
• Dedup: the content-addressed ClaimCache lets N parallel agents share work for free and makes reruns cheap — the substrate that makes parallel refinement converge rather than thrash.

---

9. Phased roadmap

• Phase 0 — Ontology + seed. Extend Spec.Corpus.Schema with the typed spec edges; load the 17 ratio competitive component specs (LaTeX → TTL via AstToTtl) as G₀; anchor concepts to Wikidata via mycelium. (first milestone)
• Phase 1 — Forward. Run decompose over the specs’ prose → content-hashed claims → propose → merge → one grounded RDF graph.
• Phase 2 — Deterministic projection. Implement the kernel (§5) + E(G); render before/after compaction so symmetries visibly collapse. (first milestone)
• Phase 3 — Refinement loop. Alternate stochastic propose ↔ deterministic project at a falling temperature; gates reject incoherent steps.
• Phase 4 — Normative ingest. mycelium front-end + normative ontology; formalize a first external RFC end-to-end (§6).
• Phase 5 — Frontier discovery. Wikidata-anchored BFS + internalize gate (relevance + marginal-E + licensing) (§7); cloud fan-out (§8).

First milestone (this RFC’s companion build): Phases 0–2 on the 17 specs, local, inspectable.

---

10. Decisions & open questions

Decided (this RFC): spine = spec; store = RDF/Jena truth + graph.proto wire + mycelium grounding; projection = hybrid Lean-proven core + Rust passes; first milestone = seed graph + compaction on the 17 specs, local.

Open:

• Internalize-gate policy. Exact thresholds for relevance + marginal-E; human-in-the-loop for accept/reject at the frontier vs. fully automatic.
• Ontology generalization. Naming/namespace for the generic normative ontology and how aion-rfc becomes a profile of it without breaking Aion.
• Symmetry detection cost. Subgraph isomorphism is expensive in general; scope to typed-motif templates + bounded neighborhoods first.
• Lean proof surface. Which projection invariants are worth full Lean proofs vs. property tests in the first cut.
• Licensing tooling. A source registry mapping document origin → mayIngestFullText / metadataOnly.

---

Appendix A — Worked example: “NAV calculation”

1. Anchor. mycelium grounds “net asset value” at its Wikidata Q-ID.
2. Expand. The Wikipedia/Wikidata node links to a valuation standard (e.g. an accounting/valuation rule or an industry NAV methodology).
3. Internalize gate. Relevant (connects to the ratio ledger specs’ P&L / valuation dimensions) ✓; licensing predicate checked ✓/metadata-only.
4. Formalize. Decompose the standard’s normative clauses → claims (MUST/SHOULD) → ground → gate (no contradictions with the existing valuation claims) → project → CorpusToLean → theorems discharged at a Tier.
5. Result. The NAV methodology is now a proven, contradiction-checked sub-graph wired into the spec library — and any ratio valuation claim that depends on it gains a checkable derivation back to the standard.

from docs/rfc-001b-crystallization-math.md

RFC-001b — Crystallization as Graph Diffusion (formal note)

Status: Draft companion to RFC-001 §2.

This note makes the “diffusion” framing of spec-graph refinement precise, and marks exactly where the correspondence is literal versus analogical. The summary claim: spec-graph refinement is a training-free, energy-guided, predictor–corrector annealed graph-diffusion sampler. Each clause is justified below.

---

1. State space

Let $\mathcal{G}$ be the set of typed attributed graphs $G=(V,E)$ where:

• each node $v\in V$ is a claim with categorical attributes $a(v)=(\text{modality},\text{tier},\text{sectionKind},\text{grounding})$, with $\text{modality}\in{\textsf{MUST},\textsf{MUST_NOT},\textsf{SHOULD},\textsf{SHOULD_NOT},\textsf{MAY},\textsf{REQUIRED},\textsf{RECOMMENDED}}$ and $\text{grounding}\in{\textsf{grounded},\textsf{loose}}$;
• each ordered pair $(u,v)$ carries an edge type $e(u,v)\in\mathcal{T}\cup{\bot}$, $\mathcal{T}={\textsf{refines},\textsf{dependsOn},\textsf{conflictsWith},\textsf{realizes},\textsf{benchmarkedAgainst},\textsf{livesIn},\dots}$, $\bot=$ “no edge”.

This is the categorical node/edge state space of discrete graph diffusion (DiGress; D3PM). (Literal: the data type is identical.)

2. Forward (noising) process

A Markov chain with factorized categorical kernels $$q(G_t\mid G_{t-1}) = \prod_{v} \mathrm{Cat}\big(a_t(v)\mid a_{t-1}(v)Q^V_t\big);\prod_{u,v}\mathrm{Cat}\big(e_t(u,v)\mid e_{t-1}(u,v)Q^E_t\big),$$ with $Q^V_t,Q^E_t$ chosen so the marginals relax toward a reference distribution $m$ over attributes/types. The $t$-step marginal $q(G_t\mid G_0)$ is closed form (matrix powers), as in D3PM.

Prior. $\pi_{\text{prior}}=\lim_{t\to T}q(G_t\mid G_0)$ is the max-entropy “claim gas”: node attributes i.i.d. from $m$, all edges $\bot$, grounding $\textsf{loose}$. Tractable to sample. (Analogue of the Gaussian prior.)

Note (caveat C3). In practice we seldom run this chain on a real document; decompose directly produces a high-entropy seed $G_0’$ near $\pi_{\text{prior}}$ (atomized, loosely linked claims). Starting reverse sampling from a near-prior state is standard in diffusion. So the forward chain is (i) a conceptual device, (ii) an optional robustness/augmentation tool (train/evaluate correctors by corrupting known-good graphs), not a daily component.

3. Target as a Gibbs measure (the bridge)

Define the spec energy $$E(G)=w_1 R(G)+w_2 C(G)+w_3 D(G)+w_4 U(G)-w_5 L(G)-w_6 S(G),$$ where $R$=redundancy, $C$=contradictions, $D$=dangling/loose, $U$=under-specification (the frontier), $L$=meaningful connectivity, $S$=symmetry compression (MDL gain). All terms are SPARQL-computable over Jena today (claim-contradiction.rq, modality-conflict.rq, dangling-references.rq, dependency-graph.rq, …).

The target distribution is the Gibbs/Boltzmann measure $$\pi_\tau(G)\propto e^{-E(G)/\tau}.$$ The “data manifold of coherent specs” is its low-$E$ support. On a discrete state space the role of the Stein/score $\nabla\log p$ is played by the local conditional ratios $\pi_\tau(G’)/\pi_\tau(G)$ for $G’$ a neighbor of $G$; an edit lowering $E$ is a discrete score-ascent step (D3PM’s discrete score).

4. Reverse process = predictor–corrector

We instantiate the reverse (denoising) dynamics as Song et al.’s predictor–corrector sampler:

• Predictor $\mathsf{Pred}{\tau_t}$ — the LLM ensemble (decompose→ClaimPropose→CompositeMerge→Ensemble→Verify). One reverse step: given the current (noisy) neighborhood, predict a cleaner graph $G{t}\to \tilde G_{t-1}$. This is a training-free, in-context approximate denoiser, conditioned on the vision $y$ (guidance). (Caveat C1: not score-matched.)
• Corrector $P$ — the deterministic projection kernel: content-hash dedup, transitive reduction, symmetry/orbit collapse, canonicalization. Each pass is a monotone projection onto the gate-passing manifold $\mathcal{M}={G:\text{gates pass}}$ with the proven invariants $$P(G)\in\mathcal{M},\qquad P(P(G))=P(G),\qquad E(P(G))\le E(G),$$ and a meaning-preservation homomorphism $G\to P(G)$ (modulo collapsed symmetry). These are $\tau{=}0$ corrector moves — always accepted.

One refinement round is $G_{t-1}=P\big(\mathsf{Pred}_{\tau_t}(G_t)\big)$, i.e. predict then project — a proximal/splitting sampler.

5. Schedule and guidance

• Schedule. $\tau_t:;T\to 0$ is the noise schedule: hot/broad exploration early (Haiku$\times$2 breadth, many parallel trajectories), cold/precise late (Sonnet→Opus verify, then deterministic projection).
• Guidance. Vision $y$ + grounding vocabulary enter as a guided target $$\pi_\tau(G\mid y)\propto \exp!\Big(-\tfrac{1}{\tau}\big(E(G)+\lambda E_{\text{cond}}(G,y)\big)\Big),$$ with the predictor prompted on $y$ (a conditional denoiser) and $\lambda$ the guidance weight — structurally classifier-free guidance.

6. Convergence (crystallization)

Acceptance rule. A predictor proposal $G\to G’$ is accepted iff $\Delta E=E(G’)-E(G)\le 0$, or with Metropolis probability $\min{1,e^{-\Delta E/\tau_t}}$. Corrector steps (monotone projection) are always accepted.

Claim. Under this rule $E(G_t)$ is a supermartingale (corrector: $\le 0$; predictor: MH-reversible w.r.t. $\pi_{\tau_t}$), hence converges a.s.; and with $\tau_t\to 0$ the chain concentrates on local minima of $E$ within $\mathcal{M}$.

A crystal is a fixed point $G^*$ with $P(G^*)=G^*$ and no accepted move lowering $E$. We obtain descent + local optimality — the same guarantee practical diffusion provides; neither reaches the global mode. (Honest: local, not global.)

7. Correspondence table

Diffusion (generative AI)	Spec-graph crystallization	Fidelity
Categorical node/edge state (DiGress/D3PM)	typed claim/edge graph $\mathcal{G}$	literal
Forward SDE / categorical corruption	$q(G_t\mid G_{t-1})$ via $Q^V_t,Q^E_t$	literal (defined); rarely run (C3)
Gaussian / marginal prior $p_T$	max-entropy “claim gas” $\pi_{\text{prior}}$	literal
Data distribution $p_0$	Gibbs $\pi_0\propto e^{-E/\tau_0}$	analogical (energy, not data)
Score $\nabla\log p_t$	discrete conditional ratios of $\pi_\tau$	literal (discrete score)
Learned denoiser $\epsilon_\theta$	LLM ensemble (in-context)	analogical — training-free (C1)
Predictor step	LLM propose/merge/verify	literal
Corrector (Langevin) step	deterministic projection $P$	literal (proven monotone)
Noise schedule $\beta_t$	temperature $\tau_t$ / ensemble tier	literal
Classifier-free guidance	vision + grounding $E_{\text{cond}}$, weight $\lambda$	literal
Sample (a generated datum)	a crystallized spec graph	literal

8. What we may and may not claim

• May claim: a training-free, energy-guided, predictor–corrector annealed graph-diffusion sampler; the deterministic projection is a proven corrector; the LLM ensemble is the predictor; crystallization = annealed descent to a local minimum of $E$ on the gate-passing manifold.
• May not claim: a trained diffusion model (no score matching, no learned $\epsilon_\theta$); a learned data manifold ($E$ is engineered/proven); global-optimality.

9. What this buys (beyond a nice metaphor)

1. An objective. $E(G)$ makes “better spec” measurable and gives the refinement a stopping criterion (a crystal).
2. A schedule. Principled hot→cold scaling of the agent fleet (where to spend Opus vs. Haiku, when to stop exploring).
3. A correctness story. The corrector’s proven monotonicity is why parallel stochastic agents converge instead of thrash — the diffusion frame names the role the ratio-style proven kernel plays here.
4. A research path. If we later want a trained model: collect (corrupted, clean) graph pairs via §2’s forward process and learn a graph-denoiser $\epsilon_\theta$ and/or an energy $E_\theta$ — turning the training-free sampler into an actual learned graph-diffusion model. The architecture is forward-compatible with that.

References (concepts, for grounding the analogy)

• Ho, Jain, Abbeel. Denoising Diffusion Probabilistic Models (DDPM), 2020.
• Song, Sohl-Dickstein, Kingma, Kumar, Ermon, Poole. Score-Based Generative Modeling through SDEs (predictor–corrector; probability-flow ODE), 2021.
• Austin et al. Structured Denoising Diffusion Models in Discrete State-Spaces (D3PM), 2021.
• Vignac et al. DiGress: Discrete Denoising Diffusion for Graph Generation, 2022.
• Song, Ermon. Generative Modeling by Estimating Gradients of the Data Distribution (annealed Langevin), 2019.
• Ho, Salimans. Classifier-Free Diffusion Guidance, 2022.

from docs/rfc-002-authoring-plane.md

RFC-002 — The Authoring Plane

Status: Draft · Spine: spec · Depends on: RFC-001, RFC-001b Date: 2026-08-05

RFC-001 made the spec graph provable. It did not make it authorable. This RFC adds the missing half: one write path, two front ends, and a cross-discipline conflict as the system’s most valuable output.

---

1. Motivation — the bottleneck moved

RFC-001 asked how to make a spec graph coherent and answered it well: a deterministic corrector with Lean-proven invariants, ten semantic gates, an un-gameable grounding check, and a measurable energy E(G). That machinery works. //grounding:grounding_verified rejects a fabricated :provenBy; //grounding:adversarial_gate detects a planted cycle, a dangling reference and a MUST/MUST_NOT contradiction; //corpus:compaction_measure removes four transitively-implied edges that a prose corpus would have kept forever.

The bottleneck is no longer checking. It is getting claims in at all.

Concretely, as of 9bac9d7:

Concern	State
Write surface	java/kg/edit/ — a CLI: add-edge, scaffold-term, scaffold-rule, scaffold-diagnostic, remove-term, one triple at a time, --apply to commit
Anything expressive	Hand-written Turtle
The one internalized external standard	corpus/nav-sec-2a4.ttl — 19 claims, researched by agents into docs/frontier/nav-sec-2a4.claims.json, then hand-transcribed
Console plugin	Read-only. 3 table panels, 3 read-only MCP tools, one static gRPC nav subtree
Provenance of a change	None. No record of who, from what intent, against which graph state
Cross-discipline conflict	Counted into E(G)’s C term by claim-contradiction.rq / modality-conflict.rq. Never witnessed, routed, or resolved as an object

The most valuable thing this system has ever produced is in docs/crank-001-first-step.md §4: C1, the discovery that ratio’s positioning brief claimed an LLM “cannot write an unbalanced or unauthorized entry” while the kernel’s only proven invariant is conservation — authorization is not a kernel theorem. A real correction to real marketing copy, found because two claims were forced into the same graph.

That is the product. And today it arrives as a row in a tension table in a markdown result log, with no owner, no witness, and no way to record that it was resolved.

1.1 Why this matters for fanout

The reason to care is scale. An agent fleet building a large system needs to be handed obligations it can bind against. Today it would be handed prose, and the failure is silent: two agents satisfy two documents that were never checked against each other, and the incoherence surfaces in production. The spec graph is the only artifact that can catch that before dispatch — but only if the obligations are actually in it, typed, and known to be mutually satisfiable.

So the three asks are one ask:

1. Authoring must be convenient or the graph stays empty and nothing else matters.
2. Coherence must be mechanical or a conveniently-authored graph is just a faster way to write contradictions.
3. Conflict must be a first-class object or the system’s best output has nowhere to live.

---

2. What exists, and what is genuinely missing

Reuse is the default. The inventory below is what an authoring plane builds on, not around.

2.1 Reusable as-is

Component	Path	Role in the authoring plane
Ontology + SHACL	rdf/ontology/{aion-rfc,shapes}.ttl	The schema authoring is typed against
Semantic gates	rdf/lint/semantic/*.rq (10)	The pre-commit gate set
Structural queries	rdf/queries/** (48)	Navigation, coverage, frontier
Gate harness	java/kg/{Gates,GateHarness,Loader,Writer}.java	The single validation entry point
Grounding check	grounding/{GroundingCheck,AdversarialGateCheck}.java	provenBy cannot be faked
Corrector core	lean/Spec/Compaction/Projection.lean	mem_dedupE / dedupE_length_le / dedupE_idem — meaning-preserving, non-increasing, idempotent
Corpus schema	lean/Spec/Corpus/Schema.lean	Modality / Tier / Document / NormativeStatement
Lean ⇄ TTL round-trip	java/kg/lean/{CorpusToLean,ProvenBySyncCheck}, lean/Spec/Emit/TtlEmit.lean	Keeps the two representations honest
Edit primitives	java/kg/edit/{WriteOps,Handles} + cmd/*	The op implementations, below a better interface
Loop contract	crank’s fastverk.crank.v1.CrankPredictor, JenaEnergy, JenaGate	Where a proposal gets measured
Plugin shape	services/spec/ + rules_fastverk_plugin + fastverk-layout	The console surface to extend
Chat plane	plugin-chat — POST /turn, SSE, confirm-gated mutation	The chat front end
Human-in-the-loop	agents HumanPrompt CRD	Fanout escalation

2.2 Genuinely missing

1. A proposal object. No content-addressed, typed, signed delta. Therefore no review, no provenance, no replay, and no way for a human-authored and an agent-authored change to be treated identically.
2. A ladder. NormativeStatement.tier defaults to .Structural and is self-declared. There is no representation for partially formalized — a claim is either in the graph or not, so authoring is all-or-nothing and a stall is invisible.
3. Conflict as an object. No witness, no owner, no resolution record, no defeasibility status.
4. Quantity and scope typing. No units, no measurement referent, no jurisdiction/edition/effective-interval. Most cross-domain errors are homonym and referent errors, and today nothing can express them as type errors.
5. Any write affordance in the UI.

---

3. Estate-fit constraints (verified — these bind the design)

Four facts about this estate were checked against the source and each one rules out an otherwise-attractive design. They are recorded here because getting any of them wrong produces a plan that cannot ship.

3.1 spec is upstream of aion, not downstream

lean/BUILD.bazel exports the Spec.* modules as source labels precisely so “cross-repo consumers (Aion’s lean_test targets)” can list them, and the namespace is deliberately neutral Spec.* “so any consumer can ground its own corpus on the kernel without inheriting an Aion-specific name.” MODULE.bazel has no aion dependency.

Consequence. The authoring plane cannot use Aion’s permission machinery — lean/Aion/Db/Policies.lean, hasPermission_emit_iff_kernelImpl, the PermissionBounds/PermissionSecurity/PermissionCache trio. Those are the natural place to enforce “an agent may not promote a claim,” and they are unavailable by dependency direction. Write capability must be enforced inside spec on its own terms, and new modules are Spec.Authoring.*, never Aion.Authoring.*.

3.2 rules_rust is present — docs/compaction.md is stale on this point

docs/compaction.md says Rust passes “were the original aspiration; since rules_rust isn’t in the ecosystem…”. That is no longer true: MODULE.bazel:150 declares bazel_dep(name = "rules_rust", version = "0.70.0") with a Rust 1.95.0 toolchain and an isolated crate_universe over the root Cargo.toml, and services/spec/ is a Rust axum binary.

Consequence. The hybrid RFC-001 §5 originally wanted — Lean-proven core plus Rust hot-path passes — is available today. The note in compaction.md should be corrected so the next reader does not re-litigate a settled question.

3.3 The meridian descriptor vocabulary — CORRECTED

This section was wrong as originally written, and the correction changes §8. It is kept, with the error visible, because the way it was wrong is the useful part: it measured the right file in the wrong version.

What it claimed: “there is no form, action, mutation, or confirmation descriptor — point-and-click authoring is not expressible in the declarative vocabulary,” and therefore every write affordance needs a botnoc ADHOC_HANDLERS entry or an upstream meridian_schemas extension.

What is actually true: botnoc/web/static/assets/main.js at HEAD dispatches body.case for table, lro, adhoc, gallery, and form — and renderFormPanelInto is a complete declarative write path: it builds each field from FormField.kind (text / masked / integer / enum_selection), validates against pattern, assembles {request_field: value} from the descriptor’s bindings, and POSTs through makeInvoker(plugin).invoke(submit.service, submit.method, request) — which resolves the route from the plugin’s own web_routes. Its own comment says so: “A FormPanel is a first-class plugin panel … This is what lets a plugin (e.g. plugin-integrations’ admin ‘Define provider’) own a native form without a meridian bundle rebuild.”

Why the error happened, and it is not a careless one: the enumeration was taken from the descriptor set available at meridian_schemas 0.5.0, which is what spec/MODULE.bazel:158 pins. The repo that ships the shell doing the rendering pins 0.19.0 (meridian_web 0.12.0 against spec’s 0.5.0). Fourteen minor versions of descriptor vocabulary were invisible from inside this repo, and the conclusion drawn — “this needs a cross-repo negotiation” — was a conclusion about a version pin mistaken for one about an architecture.

The lesson worth carrying: when a capability appears to be missing upstream, check the version the consumer pins before concluding the capability does not exist. §12.1 records the same shape of error about CI.

What survives the correction:

• The estate’s own panels.textproto files really do use only table and adhoc. That is a fact about how plugins were written, not about what the schema permits, and reading it as the latter is what produced the error.
• meridian_schemas really is an upstream module this repo does not own, and the version skew is real. It just is not a blocker — it is a bump.
• ADHOC_HANDLERS really does carry nine handlers, and access_keys really does mutate. Adhoc panels can write. They are simply no longer the only way.

Consequence — the corrected delivery decision. Declarative writes need no upstream change and no botnoc change; they need meridian_schemas bumped in spec/MODULE.bazel past the version that carries FormPanel. Three limitations found by actually writing the descriptors are recorded in mocks/ux/panels.authoring-form.textproto and are the genuine upstream asks: no binding source can supply server state (so parent, the read point, cannot be prefilled — the worst of the three); there is no decimal field kind (so a physical bound is pattern-validated text); and a form submits one flat record (so multi-op proposals with per-op triage remain an adhoc surface, which is the right division anyway).

Adhoc handlers remain necessary for exactly one class of surface: the ones whose content is a relationship between rows rather than rows — the constraint-bar axis, the faceted lattice, the per-op diff. That is a much smaller claim than the original section made, and it is the true one.

But it does not need to be. main.js carries an ADHOC_HANDLERS registry keyed by AdhocPanel.handler_id, and meridian-bridge.js’s renderPanelInto takes an adhocFactories map. The estate already ships nine adhoc handlers — chat, fleet, agents_launch, agents_graph, configs_manager, tools_gallery, image_explorer, workspaces_cards, access_keys — and access_keys mutates: it “mints a scoped RBE token via POST /api/keys/rbe.”

So mutation through an adhoc panel is established precedent, not a new hole. The authoring plane’s rich surfaces (conflict board, witness, delta review, ladder) ship as adhoc handlers against spec’s own web routes, exactly as chat does. Extending meridian_schemas with declarative descriptors becomes a later promotion step for whichever surfaces prove stable — done upstream, from evidence, once.

3.4 The gate set is real but narrower than it reads

Two honest limits on what “machine-checked” currently buys:

• //grounding:grounding_verified proves a :provenBy string resolves to a sorry-free theorem. It does not prove the theorem says what the claim says. That gap is real and should be stated in the plan rather than papered over; the ladder’s top rung is what makes it visible instead of implicit.
• lean/Spec/Grounding/WriteDoor.lean proves admit_conserves and trades_compose_conserving over Int — a genuine result about integer conservation, and the existence proof docs/crank-proof.md claims it to be. It is not a theorem about graph admission. A design that says “the write door already proves coherence is preserved” is misreading it. The admission theorem for the authoring plane has to be written.

---

4. Architecture

Three independent designs were developed and scored. The locked architecture takes one spine and grafts from the other two; where they conflicted, the choice and its one-line reason are recorded.

Spine — the proposal and the door. Nothing writes the graph directly. Every change, from any surface, is a content-addressed, signed Proposal admitted by a single Door.admit. Chosen because it is the only design whose central claim is already half-built — lean/Spec/Grounding/WriteDoor.lean is a choke point, even though what it currently proves is narrower than the name suggests (§3.4).

Graft 1 — the formalization ladder (au:R0…au:R5). Intent is a node in the same graph as formal claims, and formalization is a monotone climb with a nameable stall. Chosen because without it, authoring is all-or-nothing: a half-formalized claim has no legal representation, so the honest answer “we have captured this but not yet formalized it” cannot be recorded, counted, or ranked.

Graft 2 — a closed op vocabulary with decidable preconditions. Each op is individually reviewable and individually checkable.

Rejected — generating the authoring UI from the ontology. The most elegant of the three: make the schema be the editor, so an illegal edit has no representation in any surface. Rejected as a phase-1 goal because it requires the meridian descriptor extension that §3.3 shows is blocked on an upstream module we do not own. It is retained as the north star for the promotion step in §8.3 — and the argument for it gets stronger, not weaker, once the op vocabulary has stabilized against real use.

Rejected — dependent typing as the well-formedness mechanism. Design 1 made Proposal.ops a list of Σ op, WellTyped schema op, so an ill-typed edit is a non-term rather than a rejected term. Genuinely stronger, and the estate has precedent (the *Safe PgAst constructors certified by decide). Rejected because the write path must be callable from the Rust plugin and the Java gate harness, not only from Lean — a guarantee that exists only inside Lean does not constrain the service that actually accepts the write. The door instead runs a decidable well-typedness check and returns a witness on failure, which is weaker by exactly the gap between “cannot be constructed” and “is rejected on construction”, and that gap is stated rather than hidden.

4.1 The layers

  surfaces          meridian (adhoc panels)   chat (plugin-chat)   ingest   agent
                             │                       │              │        │
                             └───────────┬───────────┴──────────────┴────────┘
                                         ▼  composes
  IR                              au:Proposal { parent, ops, intent, provenance }
                                         │
                                         ▼  Door.admit(state, {parents, ops})
  admission          ┌─────────────────────────────────────────────────┐
                     │ well-typedness · capability · gate set · corrector│
                     └─────────────────────────────────────────────────┘
                                         │  Verdict: Admitted | Rejected | Queued
                                         ▼
  store                    Jena (RDF truth) + append-only proposal log
                                         │
                                         ▼  emit
  artifacts             corpus TTL · Spec.Corpus.* Lean · mdbook · work orders

The load-bearing structural decision is that Door.admit takes {parents, ops} and not provenance. Provenance lives one level up, in the Proposal. So “a chat-authored change and a click-authored change are indistinguishable downstream” is enforced by the signature, not by review discipline: there is no admit overload that can see who wrote it. Correspondingly the audit that keeps this true is small and static — there must be exactly one callsite that applies ops, inside the door.

Both halves of that landed in #44 and neither is a convention any more. lean/Spec/Authoring/{Op,Proposal,Door}.lean is the signature, compiled sorry-free by //lean:authoring_test: admit takes parent and ops, the Provenance type appears in the type of nothing else in the namespace, and verdict_ignores_provenance and application_ignores_provenance are rfl because there is nothing else they could be. console/lib/door.ts is the one callsite — both console write routes reach it, and the plugin’s two answer 410 Gone rather than being a second one. Two doors would have been two implementations of the pre-image above, and they had already diverged: the plugin’s flat-form lift coerced a form’s bound_value string to a float and the console’s did not, so the same submission had two canonical bodies and would now have two names.

What the Lean model deliberately does NOT contain: the 17-op vocabulary (it exists twice already, with conformance/ holding those two together; a third copy checked by nothing would be a fourth place to forget, wearing the authority of a proof) and the hash itself (what is modelled is its pre-image, which is where every claim anyone makes about the address actually lives).

5. The proposal IR

Proposal
  id          : Hash          -- content address over (parent, author, ops)
  parent      : Hash          -- the bitemporal read point the author saw
  author      : Principal
  surface     : au:Surface    -- Meridian | Chat | Ingest | Agent  (audit only)
  ops         : [Op]          -- ordered, individually reviewable
  intent      : IntentRecord  -- prose + formalization attempts, incl. REJECTED ones
  verdict     : au:Verdict    -- Admitted (may declare conflicts) | Rejected | Queued

Op is closed. Every constructor carries a decidable precondition:

Op	Effect
assertNS / amendNS / retractNS	claims (retract never deletes; it demotes)
bindTerm / alignTerm	the glossary — bindTerm is forced when a term typeahead has no match
declQuantity / assertDisjoint	the homonym registry
declScope / narrowGuard	scope and the cheapest conflict fix
promote / demote	ladder movement, with rung-tagged evidence
groundNS	attach an isAxiom or derivedVia chain
openConflict / witness / adjudicate	the conflict lifecycle
declarePrecedence	assert au:precedes — kernel capability only

id was a promise until #44. It is now computed, at the console’s door, and pinned by conformance/address_cases.json, which three implementations execute:

sha256:<64 lower-case hex>   over   canonicalJson({ author, ops, parent })

Three fields. surface and intent are stored with the proposal and deliberately left out of the pre-image — §4.1 says why, and §9.1 is the gate that would fail if they were in. Note that this is not a hash of the bytes the log stores: those carry the provenance, on purpose. Provenance is kept; it does not get a vote.

verdict is computed and recorded beside it, and is the door’s answer at the door’s width — typing and capability. §7.1 has the rest.

Three properties fall out and are worth naming:

1. Replay is by id, never by re-running a model. A chat-authored proposal replays because the ops are recorded, not because the LLM is deterministic — which it is not. This is the answer to “how can an LLM-authored spec be reproducible.” tools/proposals/replay.py is that, since #44: it names every record by hashing its own bytes (never by reading the address field — the point is to be able to disagree with it) and re-materializes the log prefix ending at the one you asked for.
2. Review is at op granularity. Accepting three of five ops emits a derived proposal against the same parent. A form panel models one record; a proposal is a diff with per-row triage.
3. Partial admission is normal. declarePrecedence requires kernel capability, so one proposal routinely splits into an admitted part and a queued part. Precedence is deliberately the expensive move: it changes the lattice for every discipline.

5.1 Why conflict is admitted rather than rejected

The counter-intuitive call. When a new claim makes an envelope empty, the door admits the proposal and attaches an au:Conflict with a witness.

Rejecting would mean the fire-safety cap could never be recorded at all, because the market commitment already in the graph contradicts it. The corpus would stay quietly wrong instead of loudly conflicted, and the system’s single most valuable output would be the thing it structurally cannot express. Admission and coherence are different questions.

This is only defensible if admitted conflicts cannot rot, which is what conflict-hygiene.rq (§7) enforces: unwitnessed, unowned, unresolved, and expired-waiver are all gate failures.

6. Ontology and schema delta

Landed in rdf/ontology/authoring.ttl — a domain-neutral profile over aion-rfc.ttl, additive only, so the 55 per-RFC diff gates and the existing corpus are unaffected. 15 classes, 51 properties, 31 vocabulary individuals.

Group	Terms	Why
Discipline	au:Discipline, au:discipline, au:stewardedBy	A conflict is interesting exactly when its parties differ here, because then no single reviewer holds the context to see it. stewardedBy gives an adjudication an addressee.
Quantity	au:Quantity + dimension, unit, measurementPoint, estimator, timeBase, viaModel, disjointQuantity	Dimension checking is insufficient. MW and MVAr share a dimension; “capacity” resolves to nameplate, accredited, contracted, insured, and permitted values. Identity is dimension plus referent.
Bound	au:Bound + boundKind, boundValue, boundGuard	Reifying bounds is what makes the feasible envelope a GROUP BY instead of a reading comprehension exercise.
Scope	au:Scope + jurisdiction/body/instrument/edition/effective interval, au:precedes	precedes is a partial order and stays partial: an undefined pair raises an owned decision instead of inventing a ranking nobody agreed to.
Ladder	au:Rung R0–R5, au:rung, promotedBy, demotedBy, stalledOn	R4 is the binding threshold. stalledOn must name the blocker — an unnamed stall is unrankable and unassignable.
Conflict	au:Conflict, 5 ConflictKinds, party, witness, detector, owner, blocksWorkOrder	blocksWorkOrder is the board’s sort key: a conflict matters in proportion to how much construction it stops.
Resolution	au:Resolution, 5 Outcomes incl. au:Refute, expires	The decision is itself a formal, expiring object. au:Refute exists because a spec system a domain expert cannot correct is worthless — it records both the correction and the detector that produced the false positive.
Defeasibility	au:defeasible, au:Defeater, 6 ComplianceStatus values	Collapsing Excused / BreachedButLiquidated / Breached / Unresolved into “allowed” is precisely the prose failure this profile exists to prevent.
Proposal	au:Proposal + parent, surface, intent, transcript, verdict	surface is recorded and never read by admission.

6.1 au:rung is orthogonal to the Lean Tier — which now has a TTL form

Spec.Corpus.Schema.Tier (Structural / Derivational / Implemented) grades how a claim’s proof is discharged. au:rung grades how far the claim has been formalized at all. A claim can be fully formalized at R4 and still Structural; it cannot be Derivational below R4. Conflating the two is what makes “partially authored” unrepresentable.

When this section was first written, rfc:tier did not exist in the TTL ontology at all — Tier was Lean-only, neither queryable nor drift-checkable, and a shipped panel that counted rfc:tier rfc:Structural read 0/0/0 forever. Closed in #50: rdf/ontology/tier.ttl is emitted from the Lean inductive (lean/Spec/Emit/TierVocab.lean, whose list of constructors is proven exhaustive) and pinned by //lean:tier_ttl_diff_test, so the vocabulary cannot drift from the type; rfc:tier is optional on a claim, at most one, and absent means untiered, not Structural; and tier-rung-coherence.rq enforces exactly the sentence above — Derivational below R4 — with its own population query, so over a corpus where nothing carries a tier it reads EXAMINED_NOTHING rather than passing. rfc:provenBy remains the authoritative TTL signal for kernel-verified: a tier is a grade, a provenBy is a theorem, and ladder-integrity.rq still checks the latter. What the note does not say — Implemented below R4, R5, whether Derivational should require a provenBy — is deliberately not gated and is filed in §13.

7. Gate set

Landed in rdf/lint/authoring/, in the style of rdf/lint/semantic/, wired by //rdf:authoring_gates.bzl and executed against a positive and a negative control (rdf/lint/authoring/fixtures/, following the grounding/AdversarialGateCheck.java discipline).

Only five of the nine are gates. The split is the important part.

Gates — zero-row, fail the build:

Gate	Rejects	conflict / clean
envelope-unrecorded.rq	an empty envelope with no au:Conflict recording it	0 / 0 †
conflict-hygiene-strict.rq	unwitnessed · unowned · unbounded or expired waiver	4 / 0
ladder-integrity.rq	hand-set rungs · unnamed stalls · provenBy below R4	4 / 0
vacuous-invariant.rq	Passes / Fails / Examined over an empty population, or with none	3 / 0
tier-rung-coherence.rq	rfc:tier rfc:Derivational below R4	1 / 0

† Correctly silent on both fixtures: the conflict fixture’s empty envelope is recorded. Strip conflicts.ttl from the AMPERE corpus and it fires with 2 rows — which is the //corpus/ampere:ampere_undocumented_authoring_* target, tagged manual + known-failing-by-design so it can be run as the demonstration that the gate has teeth.

Measures — reported, never fail:

Measure	Reports	AMPERE
empty-envelope.rq	the infeasibilities, with deficits	2
conflict-hygiene.rq	the full report, including UNRESOLVED	7
cross-discipline-coconstraint.rq	implicit co-constraint candidates	25
homonym-unregistered.rq	the glossary-alignment work queue	21

UNRESOLVED is deliberately not gated, and neither is an empty envelope. Both are true findings about the world: a real multidisciplinary corpus has open conflicts, and two instruments can genuinely be jointly unsatisfiable. Gating on them would push authors toward fake resolutions and unrecorded infeasibility — the exact failure this system exists to prevent. What is gated is an infeasibility nobody wrote down, and a conflict nobody can act on. The distinction is between “we have open problems” and “we have problems nobody can work on.”

The positive control is fixtures/expect-detections.rq: a zero-row test asserting each gate’s detection count over the planted fixture (including that the deficit computes to exactly 27.0 MW). It returns 0 rows over the conflict fixture and 5 over the clean one, so the assertions are demonstrably live. Written as counted assertions rather than an emit_diff_test against a golden TSV so it carries no dependency on the SPARQL engine’s serialization.

The headline result:

quantity                 unit  greatestLower  leastUpper  deficit  disciplines
q-sustained-discharge    MW             82.0        55.0     27.0            4

Four instruments — a capacity commitment, an OEM thermal derate, a fire-safety state-of-charge cap, a warranty throughput budget — each individually satisfiable, none citing any other, jointly infeasible by 27 MW. No document states this. It falls out of a GROUP BY with a HAVING clause, which is the whole argument for making bounds data.

These join the existing ten rdf/lint/semantic gates rather than replacing them. Not yet wired into BUILD.bazel targets — see §12 P0.

7.1 What the door can and cannot prove

Stated plainly, because the gap is where a plan like this usually cheats.

Can: that a proposal’s ops are well-typed against the schema; that the principal holds capability for each op; that every named gate returns zero rows after application; that the corrector is meaning-preserving, energy-non-increasing and idempotent for the dedup pass (mem_dedupE, dedupE_length_le, dedupE_idem, already proved); that graph state is untouched on rejection.

Where each of those now runs, since #44, because “the door can prove it” was doing too much work in one sentence:

	decided by	when
well-typedness against the closed vocabulary	the console’s door (lib/proposal.ts)	at the write, synchronously
capability	the console’s door	at the write, synchronously
the gate set	the build, //corpus/... + //rdf/...	on the promotion PR
graph state untouched on rejection	//lean:authoring_test	proved, once

The split is not a compromise, it is what the two questions are. Typing and capability are decidable from the proposal alone, so a serverless function with no query engine can answer them in a request. “Every named gate returns zero rows after application” is a GROUP BY … HAVING over the post-admission graph and needs Jena, the whole corpus and the ontology. Reporting either as the other is the failure mode: an au:Verdict of Admitted in the log means this proposal is well-formed and its author was allowed to make it, and says nothing yet about whether the corpus stays coherent — which is the promotion PR’s job, and it is a reviewed diff rather than a status code.

Preflight-at-write was considered and deferred, for four reasons each independently sufficient: the spec.v1.Derivation gate plane is gRPC-only (no HTTP path a Vercel function can call), it is not deployed alongside the console, its Preflight takes triples rather than ops, and it refuses a parent pin and any removal — so it could not answer this door’s question even if it were reachable. See RFC-006 and RFC-003 §8.

Cannot, today:

• That a provenBy theorem says what the claim says. //grounding:grounding_verified proves the name resolves to a sorry-free theorem — genuinely un-gameable as far as it goes, since no LLM output fakes a compiling proof. It does not prove correspondence. The narrowing mechanism is concrete and belongs in the roadmap: have CorpusToLean generate the theorem signature from the claim’s formal content, so the human supplies only the proof and the statement cannot drift. That converts a documentation convention into a build dependency.
• That conflict detection is complete. empty-envelope.rq is complete for claims that carry au:Bounds over a shared quantity, and silent about everything else. General cross-domain consistency is not decidable at this scale; the honest framing is a decidable fragment — linear bounds over typed quantities with comparable time bases — that grows as the corpus is typed. The dark fraction (§8) is the published measure of what is outside it.
• That an agent cannot promote a claim. This is the design’s intent, but §3.1 removes the natural mechanism: Aion’s proved permission machinery is unavailable by dependency direction. Until an equivalent exists in spec, capability is enforced by the door in ordinary Rust/Java, and that is a code property, not a theorem. Filed in §13 as the largest open gap.

8. Point-and-click authoring (meridian)

8.1 Delivery: declarative-first, adhoc where a table cannot carry it

Revised by the §3.3 correction. The original text said adhoc-first, on the strength of a descriptor vocabulary that turned out to be two years old.

Three tiers, and the ordering is now the opposite of what §8.2 assumed:

1. Declarative table panels — shipped. Six of them, in services/spec/ui/panels.textproto, populated from spec.v1.Authoring’s six GET routes. No shell code. This is the conflict board, the empty envelopes, the frontier, per-discipline coverage, the claim list and the witness parties — most of the value, and it reached the browser without touching another repo.
2. Declarative form panels — one version bump away. Written, internally checked, and not in the shipped bundle, because form { } fails to parse against spec’s pinned meridian_schemas and would break the plugin build for everyone. See mocks/ux/panels.authoring-form.textproto.
3. Adhoc panels — for the surfaces whose content is a relationship. The constraint-bar axis, the faceted lattice with conflict heat, the per-op diff, the draft bar. Four, not nine.

The mutation surface is three routes, not two:

route	method	for
POST /api/proposal	SubmitProposal	the nested, multi-op form — an MCP client or an adhoc composer
POST /api/proposal/op	SubmitOp	the flat, one-op form a declarative FormPanel can submit
POST /proposal/verdict-preview	PreviewProposal	the structural check, written to nothing

⚠ The first two moved to the console in #44; the plugin’s copies answer 410 Gone and name these. POST /proposal/verdict-preview stays where it is — it writes nothing, so it is not a door, and it now returns the address the console would give the proposal, which is what §9 step 6 (“a pid whose content hash the user already saw”) needs.

SubmitOp exists because buildRequestFromBindings produces a flat object of strings, one level deep, and a Proposal is {parent, ops: [...]}. Rather than concede that declarative writes are impossible, the door accepts the flat shape of the common case and lifts it.

⛔ This paragraph used to claim a property it could not test, and the property was false. It said: “the coercion is narrow and declared — only the named array / boolean / numeric fields, only on that route — and the property that matters is tested: a form submission and an API submission of the same op produce identical canonical bytes.” Both halves of that were true only WITHIN one implementation. There were two, and only one coerced: the plugin turned a form’s bound_value: "70" into the float 70.0 and the console left it the string "70". No suite could compare them, because one was a cargo test and the other a vitest run, and the fixtures they shared did not cover the lift. Once a proposal had a name, that divergence stopped being cosmetic — it was two permanent names for one submission.

The fix was not to make them agree. It was to have one door. The console’s fromFlat does not coerce: a value that arrived from an <input> is a string and is recorded as a string. console/test/door.test.ts executes the property across both console routes, which is now possible because both are in the same process. If coercion comes back it belongs in the one door, pinned by conformance/address_cases.json so both halves coerce identically or neither does.

What the door deliberately does not do is decide the gate set — see §7.1’s table. The build adjudicates the gates; the door decides typing and capability. verdict-preview returns its own limits array saying exactly that, because a route with that name under-delivering silently is worse than one that states its scope.

8.2 The surfaces

Navigation is faceted drill-down, never a global list — with ~8,000 in-scope claims across 12 disciplines there is no useful flat index.

Panel	Kind	What it does
atlas	adhoc	Discipline lattice with conflict-heat and dark fraction — the share of claims below R4, i.e. how much of the corpus an agent fleet may not build against.
scope	adhoc	The same lattice keyed on scope: “what constrains the thermal subsystem” — pulls every obligation from every discipline binding that scope in one aligned vocabulary. The query nobody can answer today.
conflicts	adhoc	The annunciator board, faceted by discipline pair, sorted by blocked work orders.
witness	adhoc, read-only — implemented, botnoc/web/static/assets/spec.js	The envelope: constraint bars on one axis, the intersection, the deficit, and per-party defeasibility. No editing affordances at all — you cannot fix a witness, only arbitrate the claims under it. Also shipped as a plain table in the declarative bundle, so the finding is legible before the axis exists.
claim	adhoc	Obligation normal form + the R0–R5 ladder with each rung’s evidence and gate.
proposal	adhoc	Per-op diff with accept / reject / defer, the IntentRecord prose alongside the ops, and for chat-authored proposals the rejected formalization attempts.
frontier	table	Stalls ranked by how many binding claims depend on them. A plain table suffices.
author_claim · adjudicate · narrow_guard · bind_term	form	Declarative write affordances — added by the §3.3 correction. Each composes exactly one op and submits through SubmitOp. Gated on the meridian_schemas bump, not on a botnoc change.
fanout	table	Work orders, obligation counts, disciplines bound, hold reasons.
draft bar	shell	Persistent staging with a live door-verdict chip. Composition spans screens and sessions; without it the door only speaks at submit time, which is the worst moment to learn you contradicted the safety discipline.

Authoring a claim: from a scope node, a form whose fields are the obligation normal form, prefilled from the drill path. Term fields are typeahead over the aligned glossary and cannot accept free text — an unmatched term forces an explicit bindTerm with a definition or an alignTerm against an existing concept. That is where corpus reuse is enforced rather than encouraged, and it is the single highest-leverage constraint in the UI, because most cross-domain errors are homonym errors.

Arbitration is four proposal composers, not four buttons that mutate: Narrow (narrowGuard), Prioritize (declarePrecedence, kernel capability, routes to review), Exempt (waiver with mandatory expiry), Escalate (admit the conflict standing, notify both stewards, hold orders). Nothing resolves a cross-domain conflict unilaterally.

A visual mock of all of these over the AMPERE corpus is at mocks/ux/README.md.

8.3 The promotion step

Once the op vocabulary has stabilized against real use, the surfaces that proved stable get promoted upstream into meridian_schemas as declarative descriptors — from evidence, once, rather than by guessing now. The candidate set is LatticePanel, DeltaPanel, WitnessPanel, and an Action.emits_proposal_op field that would let a descriptor lint statically prove every write affordance composes an op.

Three smaller asks now precede that list, and they are worth making first because each is generic, each benefits every plugin in the estate, and each is cheaper than a new panel kind: a context binding source (or a populate on a form) so server state can reach a field; a decimal field kind; and a parameterised populate so a table can be populated from the selected row of another — the difference between a browsable read model and a drillable one. Deferring this is a sequencing decision, not an abandonment: it is the only path to design 1’s “an illegal edit has no representation.”

9. Chat authoring — intent grounding and formalization

Same Proposal, composed conversationally, over plugin-chat’s existing loop (POST /turn, SSE HostEvents, confirm-gated mutation) and spec’s MCP surface extended with write tools. The user never reads Turtle or Lean.

The loop, and what makes each step honest:

1. Capture. The utterance is recorded at R0 with a content hash. Nothing is interpreted yet, and nothing is discarded.
2. Decompose. decomposer produces candidate claims at R2 with named holes.
3. Interview — only about the holes. Because R2 skeletons enumerate their unbound holes, the model asks about exactly those and nothing else. This is the difference between a grounding interview and a questionnaire, and it is what makes the loop survivable across thousands of claims.
4. Back-translate. The formalization is shown as a card in the expert’s own terms — who / must not / when / because / can it be waived — generated from the same op structure the door will read, not a re-description of the prose. The expert checks a claim, not a syntax.
5. Gate before commit. Gates run on the previewed proposal. On failure the user sees the specific contradiction and the model refuses to choose when resolving it needs authority it does not have. It offers the two real options and routes the one needing another signature to that person as a separate proposal.
6. Confirm. confirm:true is the only mutating call and carries a pid whose content hash the user already saw.
7. Consequences are reported, not hidden. Applying may open a conflict and a proof obligation. “This is not an error in what you wrote; it is the first time the corpus could see it.”

The persuasive property is where the model stops: unbound holes only, no adjudication without authority, no quietly widening a scope to make a gate pass. Annotated transcripts — including a case where the model is wrong about a conflict and the expert refutes it, recorded as au:Refute — are in mocks/ux/chat/.

9.1 The equal-citizen gate

The mechanical test that both front ends are one system: a scripted click sequence and a scripted chat session that author the same change must produce proposals with identical content hashes. Content-addressing collapses them to one proposal with two provenance records. If the hashes differ, the surfaces are composing different ops and the claim of equivalence is false.

Since #44 this is executable, and the precise form matters. The gate is on the address, not on the stored bytes:

address    sha256 over { author, ops, parent }        SAME from every surface
canonical  { parent, author, surface, ops, intent }   DIFFERENT, and kept

Two proposals authored through different surfaces have different stored bytes — provenance is recorded forever — and the same name. An earlier draft of §8.1 asserted the equality on canonical, which cannot hold: surface is in it. The weaker-looking claim is the true one and is also the useful one, because the address is what everything downstream keys on.

conformance/address_cases.json carries the gate as data: a same_address group naming three cases that differ in surface and intent, and different_address groups for the three things that must NOT collapse — the read point, the author (invariant ⑤: the surface collapses, the person never does), and the ORDER of the ops. Three implementations execute it, and each canonicalizes independently. console/test/door.test.ts runs the same property through the live routes, and lean/Spec/Authoring/Proposal.lean proves it about the pre-image type.

Still not covered: an actual scripted chat session. The gate proves that two proposals with the same ops get the same name; that the chat plane composes the same ops as the click plane is P5’s, and it is the part that can still be false.

10. Agent fanout over an authored spec

An agent never receives “the spec.” It receives a work order:

WorkOrder
  scope           : ScopeExpr
  obligations     : [ObligationId]   -- lattice closure over scope, ALL disciplines
  glossary        : aligned term slice
  forbidden       : [ScopeExpr]
  conflict_holds  : [ConflictId]     -- MUST be empty to dispatch
  acceptance      : [DecidableCheck]
  write_capability: Capability       -- artifact paths
  as_of           : Hash             -- bitemporal cursor, not "latest"

Four mechanisms carry the invariant claim:

1. Obligation closure, not document handoff. obligations is the upward and downward closure on the scope lattice, so the agent building the thermal module is handed the safety, market, warranty and cyber obligations that bind its scope, in one aligned vocabulary. Ignorance of a cross-discipline requirement stops being possible.
2. Only R4+ binds. R0–R3 claims arrive explicitly marked non-binding, and satisfaction evidence may only reference R4+. Half-formalized spec cannot leak into implementation as though settled — the specific failure mode that makes “author fast, formalize later” dangerous.
3. Dispatch is gated on the conflict graph. conflict_holds non-empty ⇒ no dispatch. Plus pairwise scope-disjointness with every running order.
4. Agents may write R0 only. An agent principal’s capability covers its artifact paths and assertNS at R0 — never promote, adjudicate, bindTerm or declarePrecedence. §7.1 is honest that this is currently a code property rather than a theorem.

Fanout feeds back into the spec. An agent that cannot satisfy an obligation raises a HumanPrompt (the agents CRD) naming the missing claim rather than guessing, widening its own scope, or silently marking the obligation met. Authoring the missing claim amends the spec, recomputes the closure, and resumes the agent from its checkpoint. That is the good failure mode, and it is the whole reason to put the obligations in a graph.

11. Worked corpus — AMPERE

A 400 MWh / 100 MW grid-scale battery plus an aggregated DER virtual power plant bidding into two US wholesale markets, including its financing, safety case, cybersecurity posture and control software. Twelve disciplines: electrochemistry and thermal, interconnection, market microstructure and tariff, protection and controls, fire and life safety, cybersecurity and reliability compliance, tax and project finance, accounting and revenue recognition, environmental permitting and land use, software and DER fleet control, metering and settlement, and insurance / warranty / O&M.

Chosen because four incommensurable rule systems bind the same five-minute dispatch decision: continuous physics; public law in three parallel jurisdictional stacks; private contract; and executable market software. Scale is genuinely large — roughly 500 documents and ~50,000 extractable normative statements, of which ~8,000 are in scope for one asset. But the decisive number is neither of those: it is the estimated 4,000–8,000 implicit co-constraint pairs — statements from different disciplines bounding the same physical, temporal or financial quantity while citing nothing in common — of which a few hundred bind and perhaps 60–150 are true conflicts. A citation graph finds almost none of them.

Alternatives considered: a clinical-trial platform (well-structured sources, but the conflicts are mostly within-discipline), spacecraft avionics (deep, narrow), cross-border payments (multi-jurisdiction, but one discipline’s vocabulary dominates). AMPERE wins on cross-domain conflict density, which is the property under test.

11.1 The result that justifies the whole RFC

The corpus as committed (corpus/ampere/, 2,077 triples) is SHACL-conformant and returns zero rows from all nine pre-existing coherence gates — contradiction, modality conflict, dangling references, dependency cycles, derivation cycles, term drift, diagnostic collisions, dead dependsOn, inverse edges. By every coherence check the spine had before this RFC, it is clean. (grounding.rq correctly reports 64/64 ungrounded — nothing is theorem-backed yet. That is the frontier, not a defect.)

It nevertheless contains two empty feasible envelopes, found by the new empty-envelope.rq:

q-sustained-discharge   MW    82.0 > 55.0    deficit 27.0 MW   5 disciplines
q-telemetry-latency     ms   180.0 > 150.0   deficit 30.0 ms   2 disciplines

modality-conflict.rq cannot see either, because it matches on byte-equal predicate text — and these claims share no words, no document, no discipline and no citation. The second envelope was not planted as a headline: the same aggregation found it on time rather than power, which is the evidence that the mechanism generalises rather than being tuned to one demo.

That is the argument for the whole RFC in one measurement. The existing gate set is not weak; it is structurally blind to cross-domain infeasibility, and no amount of prose review closes that gap.

Citation posture, stated once and prominently: the corpus is technically coherent and deliberately not citation-verified. Clause numbers are leads, not facts, and are marked # UNVERIFIED-CITATION. No real market operator, manufacturer, insurer or jurisdiction is named. The corpus exists to exercise mechanisms.

12. Phased roadmap

Each phase is independently shippable with a demonstrable gate. Week numbers are sequencing, not commitments.

Phase	Weeks	Deliverable	Gate
P0 Wire what exists	1–2	BUILD.bazel targets for rdf/ontology/authoring.ttl + the gates + both fixtures. Written; never exercised — see §12.1	The §7 control table runs under bazel test. Blocked on the pre-existing //java/... maven and //graph/... svg2pdf failures
P1 Proposal + door	3–8	lean/Spec/Authoring/{Proposal,Op,Door}.lean; append-only proposal log; spec propose / spec replay CLI over java/kg/edit’s existing WriteOps	spec replay <bootstrap-pid> reproduces the committed corpus TTL byte-identically
↳ landed in #44		the three Lean files (//lean:authoring_test); the content address + au:Verdict at the console door, mirrored in the plugin’s preview and in Python; migration 0004; tools/proposals/replay.py; the plugin’s write path retired to 410	//tools/proposals:replay_test replays a fixture log prefix byte-identically, refuses a record the door rejected, and refuses a record whose stored address is not the address of its own body. ⚠ The gate over the REAL log still reads zero, because logs/proposals.jsonl is empty until the first promotion — see §12.2
P2 TTL becomes emitted	6–11	The corpus becomes an emit target of the proposal log via Spec.Emit.TtlEmit	The existing 55× rfc_NNNN_ttl_diff_test pass unchanged — same tests, inverted meaning, zero test deletion. The strongest available proof the new write path is faithful
P3 Ladder + import	9–13	R0–R5 as graph state; import the existing corpus, assigning rungs from evidence	Every existing claim lands at its correct rung with zero hand annotation, and the rung histogram is published
P4 Adhoc authoring surfaces	10–16	The §8.2 panels as adhoc handlers; POST /proposal; the draft bar	A requirement authored end-to-end by clicking merges through the door
P5 Chat plane	14–19	The §9 loop in plugin-chat; spec’s MCP write tools; back-translation cards	The equal-citizen gate (§9.1): click and chat produce identical pids
P6 Conflict engine	17–24	The decidable fragment; witness computation; the four arbitration moves	At least one genuine cross-domain conflict found in a real corpus with a reviewed witness, and one conflict resolved by each of the four moves
P7 Fanout	22–28	Work-order derivation with closure; capability tokens; dispatcher disjointness	N≥8 agents build concurrently with zero cross-scope writes (verified, not observed); an order whose closure touches an open conflict refuses to dispatch
P8 Retire hand-authoring	26–30	Remove the hand-TTL workflows from CLAUDE.md; make raw writes unreachable	//ci:pr_gates green with the raw-write path absent from the dependency graph, asserted by a dep-graph test

P0 is deliberately two weeks and mostly wiring: the mechanism layer is already written and verified, and the fastest way to lose it is to leave it un-gated.

12.1 P0 is wired, but CI cannot tell you whether it works

The wiring is present. It has never been exercised, and the reason is worth recording carefully because it cost four commits to establish.

fastverk/build is red on main, and has been for a while. The evidence:

head	fastverk/build
PR #16 (merged into main)	failure
PR #17 (merged into main, = current main)	failure
this branch, at a one-line BUILD change	failure

And the cause is documented in main’s own HEAD commit message (9bac9d7):

NOT fully verified: bazel build //... does not pass on this host either before or after this change — //java/... cannot fetch maven (“Unable to locate a Java Runtime” from coursier) and //graph/... fails in svg2pdf under bun. Both reproduce identically on unmodified origin/main, so they are pre-existing and environmental.

So the check is a constant, not a signal. It says nothing about whether a change is sound, and cannot validate the P0 wiring either way.

What that cost. Three commits chased that red as though the wiring had caused it — narrowing constructs, then withdrawing the wiring entirely — before checking whether main was red too. The build log at app.fastverk.com returns 403 to the authoring environment and the check run’s output.text is empty, which removed the fastest path to the answer. But the merged-PR check history was available the whole time and would have settled it in one call. Check whether the baseline is green before treating a red check as yours.

What was genuinely found. One real bug, and it justified the exercise: an empty glob() across a new package boundary. rdf/lint/authoring/BUILD.bazel makes that directory a subpackage; glob() does not match into a subpackage; so glob(["lint/authoring/*.rq"]) in //rdf matched nothing — and an empty glob is a hard error under --incompatible_disallow_empty_glob, default-on since Bazel 7.

12.2 P1’s acceptance gate cannot run over the real log yet, and says so

spec replay <pid> reproducing the committed TTL byte-identically is the right gate and it is worth being exact about what currently satisfies it.

logs/proposals.jsonl is empty. No proposal has been promoted, because promotion needs NEON_EXPORT_URL in the corpus-production environment and that is not set yet (#49 landed the workflow; the secret is an operator step). A gate run over an empty log would pass by examining nothing — the exact defect vacuous-invariant.rq exists to catch, in a test instead of a corpus.

So //tools/proposals:replay_test runs over a fixture log that plants two defects and fails if either goes undetected: a record the door refused (which must not reach the corpus, since the door never appends one — such a record can only come from a hand-edited or restored log) and a record whose stored address disagrees with the address of its own body. A third record carries no address and no verdict at all, standing for everything written before the door computed either; it must still replay, or the whole history disappears.

When the first real promotion lands, //corpus/studio:proposals_ttl_matches_the_log and a replay --check over the last address become the same assertion by two routes, and that is the moment P1’s gate is genuinely met. That would have broken loading of //rdf for every consumer, locally as much as in CI. Fixed, with a comment at both sites naming the trap.

Still unvalidated, for whoever has a working bazel:

1. spec_authoring_gates forwarding tags into sparql_query / sparql_query_test.
2. rdf_dataset with two vocab TTLs in srcs — chosen over deps = [":vocab"] precisely because dataset-on-dataset layering has no precedent in this repo.
3. Whether Jena’s SHACL engine agrees with pyshacl on the three new datasets.
4. Whether //corpus/ampere:{measure,coverage,frontier} resolve their queries/*.rq labels. That subdirectory has no BUILD.bazel, so it should be the same package — untested.

One thing was dropped rather than fixed. An earlier draft wired a permanently red target — the AMPERE corpus minus conflicts.ttl, whose envelope_unrecorded gate then fires with 2 rows — to demonstrate the gate has teeth. In a repo whose culture is “green gates or it isn’t real”, a target that always fails is an invitation to start ignoring CI, and it is doubly wrong when the surrounding check is already a constant red. The demonstration belongs as a positive assertion: a query over the conflicts-stripped dataset whose expected row count is 2, which is zero-row exactly when the gate works — the shape fixtures/expect-detections.rq already uses. corpus/ampere/BUILD.bazel carries the verified numbers in a comment meanwhile.

The independent verification path. Everything the wiring would gate is verified by execution under rdflib 7.6 + pyshacl, and that harness reproduces docs/phase-0-materialization.md’s numbers exactly over the shipped corpus — 18 documents, 38 claims, SHACL conformant, all four consistency invariants at zero. That agreement on known-good data is what licenses trusting it on the new data. Keeping a Python-only path working is worth a little effort on its own merits: it runs where a bazel is not provisioned, which is most agent sessions.

13. Open questions

1. Capability enforcement without Aion’s permission proofs (§3.1, §7.1). The largest gap. Options: build a minimal proved policy layer in Spec.Authoring; invert the dependency so the permission tier lives in spec and Aion consumes it; or accept a code-level property and say so. This should be decided before P7, since fanout is where it bites.

2. Claim ⇄ theorem correspondence. Is generating theorem signatures from claim content (§7.1) sufficient, or does the claim’s formal content need to be expressive enough that the signature is the whole statement?

3. The rest of the tier/rung rule (§6.1). The TTL projection of Tier landed in #50 with exactly the promised check (Derivational below R4). Open: should Implemented also require R4 — or R5? Does R5 imply anything about tier? Should Derivational require an rfc:provenBy, making the tier a consequence of the theorem rather than a declared grade?

4. The decidable fragment’s boundary. Linear bounds over typed quantities with comparable time bases is the proposed starting fragment. What is the next increment that pays for itself — intervals? piecewise-linear derate curves?

5. Where the promotion step lands (§8.3). Which surfaces earn declarative descriptors, and who negotiates the meridian_schemas 0.5.0 / 0.6.0 skew.

6. Rung assignment on import (P3). Can rungs really be derived from evidence for the whole existing corpus with zero hand annotation, or is there an irreducible manual tier?

7. Adjudication authority in practice. au:stewardedBy gives a conflict an addressee, but a four-party empty envelope has four stewards and no obvious chair. Does the corpus need an explicit escalation order, and is that itself a scope-precedence claim?

8. Should the door coerce a form’s strings? Decided: it should not. bound_value from a FormPanel is recorded as the string "70", and the same op sent as JSON with 70 is a different proposal with a different address — because they are different values, and a door that quietly made them one would be deciding what an author meant. The cost is real and lands on the surfaces rather than on the rule: a console must show an author what they actually composed, or the same change submitted twice by two routes becomes two proposals and only the log says so.

   What this closes: the coercion table is not coming back, so there is no second place for it to rot (it rotted once — the plugin’s diverged from the console’s and nothing compared them). What it leaves open is the better version of the question: whether the op vocabulary should carry a type per field, so that bound_value is declared a number once and a form’s "70" is parsed at the door rather than coerced by a table. That would make “a wrong-typed field is a rejection” the same rule as “an unknown field is a rejection” — which is already how a typo’d bound_vlaue is caught — and it is a change to the vocabulary, not to the door.

9. Does the address need a drafted_by or an idempotency key? Two identical proposals from one author against one read point have the same address by construction, which is correct — content addressing means what it says, and verify.mjs proves the index is deliberately not unique. But it means “did my click land twice” is answerable only by seq. Whether that wants a separate submission id is a real question and #44 did not answer it.

10. What names a parent? The door records the read point the author saw and checks nothing about it — §7.1 has said “does NOT verify parent names a real bitemporal read point” since P0, and the address now makes that omission load-bearing: two proposals against read points that differ only in spelling are two proposals. A canonical form for parent is probably needed before there are enough of them to matter.

from docs/rfc-002a-browser-authoring-path.md

RFC-002a — The path to spec authoring in the browser

Status: Draft · Companion to: RFC-002 §8 Date: 2026-08-06 (revised)

RFC-002 §8 says what the authoring surfaces should be. This says what has to happen, in what order, for any of it to appear in a browser — and which parts are unblocked today versus gated on another repo.

Revision note. The first draft of this document had six of seven stages gated on somebody else: a botnoc PR, an upstream descriptor extension, a Lean toolchain, and a maven pinning fix. Five of those gates turned out not to exist. What follows is the corrected chain, with the reasons each gate dissolved — because the reasons generalise better than the result.

---

1. Three facts that reframe the sequencing

RFC-002 §8.1 originally concluded that the authoring surfaces should ship as meridian adhoc handlers, because the declarative descriptor vocabulary has no write primitive. Three facts say otherwise, and they were all findable by reading files in this session’s own working tree.

Fact 1 — a declarative plugin reaches the browser with no shell change at all. plugin-mycelium/ui/panels.textproto states the property in its own header:

DECLARATIVE table panels (like forge/depot/tbzl): the shell decodes the bundle, builds a nav leaf per panel, and renders each table via renderPanelInto — populating rows from populate.service/.method, which the shell routes through /api/gw/mycelium/* via the web_routes in /describe. No shell-side (main.js) code.

Fact 2 — most of the authoring read model is tabular. The conflict board, the empty envelopes, the frontier, per-discipline coverage, the claim list, and a conflict’s witness parties are all rows and columns. The genuinely non-tabular surfaces are fewer than §8.2 implied: the constraint-bar axis, the per-op proposal diff, the faceted lattice with a heat overlay, and the draft bar.

Fact 3 — the declarative vocabulary already has a write primitive. main.js dispatches body.case === 'form' to renderFormPanelInto, which is a complete declarative write path: fields from FormField.kind, pattern validation, bindings → a flat request object, and a POST through the plugin’s own web_routes. RFC-002 §3.3 said this did not exist; §3.3 was measuring meridian_schemas 0.5.0, spec’s pin, while botnoc — the repo whose shell does the rendering — pins 0.19.0.

Together: the read side of browser authoring was already unblocked, most of the value is on it, and the write side is a version bump rather than a negotiation. Seeing that two instruments are jointly infeasible by 27 MW is the product; drawing it on an axis is presentation.

2. The chain, and what actually gates each link

  [A] compute the read model             ── DONE, verified (6 queries, 128 rows)
        │
  [B] serve it from the plugin           ── DONE. 6 GET routes + 3 POST + /readmodel;
        │                                   compiled and 32 tests green
  [C] declare the panels                 ── DONE, merged into the SHIPPED bundle
        │                                   (textproto + recompiled .binpb)
  [D] read model visible in browser      ── B + C, both done. Needs a deploy, not work.
        ╎
        ╎  ── everything above landed without touching another repo ──
        ╎
  [E] rich read surfaces (the axis)      ── DONE in botnoc: web/static/assets/spec.js
        │                                   + one ADHOC_HANDLERS entry (`spec_witness`)
  [F] the write path                     ── DONE, queue-side: closed op vocabulary,
        │                                   structural check, append-only log.
        │                                   The DOOR is not here — see §6.
  [G] write affordances in the browser   ── WRITTEN, not shipped. Gated on ONE thing:
                                            meridian_schemas 0.5.0 -> a FormPanel
                                            version in spec/MODULE.bazel.

The structural point that mattered: D never depended on E, F, or G. Earlier framing made the browser story sound like one cross-repo negotiation. It was two projects, and the first one was small.

3. [A] Compute it

tools/readmodel/emit_readmodel.py runs six SPARQL queries over a corpus carrying the au: vocabulary and emits one JSON file per route in the envelope services/spec/src/json.rs already uses: {"<rows_field>": [...], "unreachable_repos": []}.

Verified against corpus/ampere (2,080 triples), byte-identical across runs:

route	rows_field	rows
conflicts	conflicts	12
envelopes	envelopes	2
frontier	stalls	5
disciplines	disciplines	12
claims	claims	64
witness	parties	33

Output lives in services/spec/readmodel/ — the directory the plugin serves, not a mocks folder, so there is one copy rather than two that can disagree.

The architectural decision this encodes: the build computes, the plugin serves. The alternative was a SPARQL engine in the Rust plugin, which means a new crate, a second RDF implementation, and a second thing to keep in agreement with the Jena gates. Instead the read model is generated the way the plugin already works — its index is “a scan of the git-synced source tree at $SPEC_SOURCE_ROOT” — and there stays exactly one SPARQL implementation of record.

The trade, stated plainly: the read model is as fresh as the last emit, not live. For a corpus where claims change at review cadence rather than per-request that is the right side of the trade. If it ever isn’t, the fix is a rebuild trigger, not a query engine in the BFF.

One column was added while building [E]: quantity on both the conflicts and witness rows. Without it a witness row says “this claim binds at 55” with no way to know 55 of what, which makes the constraint-bar axis — the screen the whole read model exists for — impossible to draw. Row counts are unchanged (the join is OPTIONAL); 21 of 33 witness rows and 7 of 12 conflicts carry one.

4. [B] Serve it — and how it got verified without Bazel

services/spec/ gained:

• src/readmodel.rs — the payload loader, TTL-cached, with a missing or malformed payload degrading to zero rows plus a note in unreachable_repos (the plugin’s existing partial-result channel) rather than an error;
• src/routes.rs — the web_routes contract as data, with no axum dependency, so it can be asserted against from both a startup check and a static one;
• src/proposal.rs — the closed op vocabulary and the append-only log (§6);
• six GET handlers, three POST handlers, and GET /readmodel (per-route row counts and availability — because “the corpus is clean” and “the payload never shipped” render identically in a panel);
• nine LayoutService nav leaves;
• three read-model MCP tools (list_conflicts, list_empty_envelopes, frontier), which are the grounding half of RFC-002 §9’s chat loop: a model cannot ask “does this contradict anything” without them.

§3.2 of the first draft said this was the one real blocker, because nobody could build or test it. That was true of Bazel and of cargo against this crate — the private fastverk-plugin-crates git deps 401 here. It was not true of the code. Three of the four new modules depend only on serde_json and tracing; http.rs adds axum and tokio. A scratch crate that pulls those four from crates.io and includes the real sources by #[path], with 60 lines of stubs standing in for the prost messages, the estate indexer, and fastverk-mcp, compiles all of it.

That found three real defects that review had not:

1. routes_match_describe compared all authoring routes against the six read routes and reported “8 declared, 6 served” on a correctly-wired plugin — it was counting the two POST writes. It would have logged an error at every boot.
2. Checked needed Debug for expect_err.
3. A doc-comment patch had silently dropped a ///, which is a parse error that cascaded into two spurious “type annotations needed” errors in a different file.

The HTTP tests boot the real router on an ephemeral port and issue real HTTP/1.1 over a socket. tower::ServiceExt::oneshot would have been the idiomatic client, but tower is not a dependency and adding one means re-pinning the crate universe; tokio::io::AsyncReadExt is behind the io-util feature this crate does not enable. So the client is a blocking std::net::TcpStream on spawn_blocking, which needs nothing new and exercises the same route table.

32 tests pass. The write path is covered end to end: refused without a principal, 503 with no log configured, 422 with nothing appended on a malformed op, 202 with exactly one line appended on a good one.

Writing those tests also surfaced a defect in the tests themselves worth recording: they originally configured the server through std::env::set_var, and Rust runs #[test]s in parallel threads of one process, so each test raced every other on the same keys. Two failed nondeterministically. The fix was ReadModel::new and ProposalLog::new — env parsing separated from construction, which is a better API independent of the tests.

5. [C] and [D] — the panels, and the one thing that would have silently failed

The six panels are in services/spec/ui/panels.textproto, merged into the shipped bundle rather than added as a second one. That is not a style choice. main.js’s fetchPluginPanels does:

loadPanelBundleFrom(`${base}/panels.binpb`)

— a single hard-coded path. It never reads manifest.panels[].bundle_path. A second meridian_panel_bundle, which is what the first draft of §3.2 proposed, would never have been discovered, and the failure mode is an empty nav section with no error anywhere.

services/spec/ui/panels.binpb is committed and generated — which is a standing staleness hazard, because the first person to edit the textproto without a working Bazel leaves the two disagreeing and nothing says so. So the regeneration is a repo tool: tools/readmodel/compile_panels.py.

Without protoc or the uiview schema, its field numbers were read off the committed bundle by decoding it on the wire (panels=2; panel_id=1, title=2, table=3; populate=1, rows_field=2, item_noun=3, placeholder=4, columns=5; header=1, field_path=2, pref_width=4 — the kind of thing that is obvious from the bytes and invisible from the textproto). Hand-rolled protobuf is only trustworthy if it is checked, so the tool checks itself on every run, before it is allowed to write anything:

1. Round-trip — decode the committed bundle and re-encode it; the result must be byte-identical. A codec that cannot reproduce protoc’s own output on real data has no business producing a replacement.
2. Agreement — compile the textproto, decode the result, and compare panel ids, populate pairs, rows_fields and column field_paths against what the textproto says. This catches a textproto the parser misread, which round-tripping cannot.

Without --write it verifies and reports staleness with a non-zero exit, so it works as a gate as well as a generator. It refuses outright on a non-table panel rather than guess a field number it has no evidence for — which is also why the form panels of [G] cannot be compiled here even setting the version bump aside.

bazel build //services/spec/ui:panels remains the real compiler and the source of truth. This is the thing that keeps the committed copy honest between builds.

5.1 The wiring check

The authoring plane is described in seven places — the emitter’s route table, the emitted payloads, the emitted /describe fragment, readmodel.rs’s ROUTES, routes.rs’s declarations, http.rs’s axum registrations, the panel textproto, the nav leaves, the compiled bundle, and the form descriptors. Every pair is connected by a string, so nothing in the type system connects them and nothing in the compiler catches a rename.

tools/readmodel/check_wiring.py catches it: 146 checks, standard library only, no Bazel and no toolchain. Each section has a demonstrated negative control — a rows_field typo in Rust, a stale compiled bundle, a missing nav leaf, a form field nothing binds, an op outside the closed vocabulary, a submit pointing at an undeclared route. All six perturbations were injected, caught, and reverted.

6. [F] The write path — what it is, and the line it does not cross

RFC-002 puts Door.admit in Lean, taking {parents, ops} and not provenance. That door is not in the plugin and was not simulated there. What the plugin does is the queue side:

• check every op against the closed 16-constructor vocabulary and its local decidable preconditions;
• append the canonical bytes to an append-only log ($SPEC_PROPOSAL_LOG; unset disables the write path entirely, which is the right default for a BFF whose other three tables are a scan of someone else’s source tree);
• return the per-op verdict split.

Three enforcement decisions are worth naming because each rules out a specific silent failure:

• An unknown field is a rejection, not a dropped key. A typo’d bound_vlaue would otherwise become an unbounded claim that passes every gate.
• declQuantity requires all six referent fields. Dimension alone is insufficient — MW and MVAr share a dimension, “capacity” is five disjoint concepts. Over corpus/ampere, metering & settlement reads 0.0% typed, and it is the discipline that fixes the referent for every energy quantity there.
• An agent principal may only assertNS at R0. RFC-002 §7.1 is honest that this is a code property rather than a theorem. proposal.rs is that code, in one place, which is the most the claim can currently mean.

Capability shortfall yields QUEUED, not REJECTED: §5 makes partial admission normal, so a proposal mixing author-capability and kernel-capability ops splits rather than failing whole. declarePrecedence fails closed — an empty $SPEC_KERNEL_SUBS means nobody holds kernel capability — deliberately unlike pluginCallerIsAdmin’s fail-open, because that one hides a nav item and this one changes every discipline’s lattice.

No content address is computed. Proposal.id is a hash over (parent, author, ops); this crate has no hash primitive and cannot acquire one without re-pinning the crate universe, which needs a cargo that can reach the private git deps. Rather than mint a plausible-looking identifier from DefaultHasher — neither stable across releases nor collision-resistant, and its own docs say so — the response returns the exact canonical bytes the address will be taken over, plus "address": null and "address_computed_by". A fabricated address is strictly worse than an absent one: it would be indistinguishable from a real one at every downstream callsite.

⚠ Overtaken by #44, and the way it was wrong is worth keeping. The reasoning above is sound and the conclusion — refuse to mint a fake — was right. The premise decayed. “Cannot acquire one without re-pinning the crate universe” turned out to be one line in Cargo.toml and a cargo update -p: eight small pure-Rust crates, no C, no build script that runs a compiler. It was true when it was written, in the sense that there was no reason to pay for it yet; what it became was a standing reason not to build the door, quoted in three files. The door is now the console’s, services/spec’s write path answers 410, and this crate computes the address for verdict-preview so an author can see the name before submitting. The lesson is not “we were too cautious” — it is that a cost estimate recorded as a constraint needs re-measuring when someone starts planning around it.

The canonicalizer is written out rather than delegated to serde_json::to_string, whose key order depends on whether preserve_order is enabled somewhere in the dependency graph — a build-configuration detail that must not be able to change a content address.

Likewise verdict-preview returns its own limits array: structural only, does not evaluate the coherence gates, does not verify parent names a real read point, no address. A route with that name that quietly under-delivers is worse than one that states its scope. (Since #44 it does return the address, and the limits array says so and says what it still does not check.)

This is the write-side reading of the same decision the read model encodes: the build adjudicates, the plugin queues. The first draft of this document said “P1 should not be written in an environment that cannot build Lean.” That still holds — and the reason the queue side could be written is that it makes no claim the Lean door will make.

7. [G] What remains, and it is one line

mocks/ux/panels.authoring-form.textproto carries four declarative write affordances — assertNS, adjudicate, narrowGuard, bindTerm — each composing exactly one op and submitting through SubmitOp. They are internally checked (bound fields match declared fields, ops are in the closed vocabulary, submits name a declared POST route) and they are not in the shipped bundle.

The single prerequisite:

spec/MODULE.bazel:  meridian_schemas 0.5.0 -> a version carrying FormPanel
                    meridian_web     0.5.0 -> the matching bundle rule

meridian_panel_bundle compiles the textproto against @meridian_schemas//proto:uiview_proto at spec’s pin. A form { } block under 0.5.0 is a textproto parse failure, which fails the panel-bundle target, which fails the plugin build for everyone. Shipping it unbuilt is exactly the §12.1 hazard, so it waits for somebody with a working Bazel — one bump, one build.

The routes those forms submit to are already live and already tested, including the property that matters: a form’s string values and an API client’s real JSON types produce identical canonical bytes, so click- and API-authored changes are the same change. That is §9.1’s equal-citizen guarantee on the write side, tested rather than hoped for.

8. [E] The axis — the one surface a table cannot carry

botnoc/web/static/assets/spec.js + one ADHOC_HANDLERS entry (spec_witness). It draws several disciplines’ bounds on one axis with the empty intersection shaded:

≥ 82  market microstructure     capacity commitment          defeasible
≤ 78  electrochemistry          OEM derate at 45 °C          NON-defeasible
≤ 70  fire & life safety        SOC window ÷ 4h              NON-defeasible
≤ 55  insurance & warranty      throughput budget spent      defeasible   ← binds
──────────────────────────────────────────────────────────────────────────
      intersection [82, 55] = ∅         deficit 27 MW, 5 disciplines

Every failure degrades to a pointer at the Envelopes table, because the finding lives there and is complete without this panel: a fetch that fails, a payload with no rows, a conflict whose parties carry no numeric bound. And an unstated defeasibility renders as “unstated” rather than as either value — the corpus not saying is not the same as the corpus saying no.

Sequencing: botnoc must ship the handler before spec declares an adhoc panel naming it, or the panel renders “No adhoc handler for spec_witness”. So the botnoc change lands first and is inert until spec’s bundle references it.

9. The critical path, in one list

1. Fix issue #19 — pin maven_install.json so //java/... fetches without an ambient JDK, and fastverk/build becomes a signal again. Everything below is ordinary once it is; nothing below is validated while it isn’t.
2. Exercise the P0 wiring — bazel test //rdf/lint/authoring/... //corpus/ampere/.... Four constructs remain unvalidated (RFC-002 §12.1).
3. Build services/spec — the code compiles and its tests pass under a scratch crate, but not against the real crate universe, and panels.textproto has not been through meridian_panel_bundle (the committed .binpb was produced by a round-trip-validated encoder, which is evidence, not a build).
4. Wire emit_readmodel.py and compile_panels.py into the build so the read model refreshes with the corpus instead of being refreshed by hand. This needs rules_python, which is not currently a bazel_dep — the honest reason it is step 4 and not step 1. check_wiring.py is the interim guard and needs no toolchain.
5. Bump meridian_schemas past FormPanel and move panels.authoring-form.textproto into the shipped bundle. This is [G].
6. Ask upstream for the three small things (§3.3): a context binding source, a decimal field kind, a parameterised populate.

Steps 1–3 are not spec-authoring work. They are the difference between building on evidence and building blind.

10. What is verified, and what merely exists

	evidence
The six SPARQL queries and their 128 rows	executed under rdflib 7.6; byte-identical across runs
readmodel.rs / routes.rs / proposal.rs / http.rs	compiled by rustc 1.94.1; 32 tests pass, including the router over real HTTP
The seven descriptions agreeing	146 checks, six negative controls injected and caught
panels.binpb	compile_panels.py: codec round-trips protoc’s own output byte-for-byte, then the compiled bytes are checked structurally against the textproto. Staleness detection has a negative control
panels.textproto (9 panels)	parses; every populate pair and rows_field cross-checked
botnoc/.../spec.js	parses as an ES module; exports resolve. Not rendered in a browser.
mocks/ux/panels.authoring-form.textproto	internally consistent. Never compiled — needs the version bump
The Bazel wiring from RFC-002 P0	still never exercised. Issue #19
Door.admit, the content address, the gate verdict	did not exist when this was written; RFC-002 P1, and correctly not attempted here. #44 landed the first two — the door and the address, in the console, with the Lean model at //lean:authoring_test — and left the gate verdict where it belongs, in the build

The distinction that line-by-line table exists to preserve: “the compiler accepted it and the tests pass” and “it ran in production” are different claims, and in a repo whose CI has been a constant red, conflating them is how §12.1 happened.

from docs/rfc-003-hosted-console.md

RFC-003 — the hosted console: Vercel, Neon, and one set of safety cases

Status: in progress. The console is built, runs, and replaces portal/; the safety rules are ported and gated. It has not been deployed against Neon or a real identity provider. §10 says exactly what is outstanding.

Companion to RFC-002 (the authoring plane) and RFC-002a (the browser authoring path). Those two describe a write path that works on one laptop. This one is about the fact that it works only on one laptop.

---

1. Why

Everything below the browser already existed and was gated: a generated TTL corpus with SPARQL/SHACL gates run by Bazel in CI, a read model projected to committed JSON, a Rust service serving it, and a Vite SPA with the full write path. None of it was reachable by a product owner. portal/ had no image, no chart, no CI publish and no deployment story of any kind — it ran as vite dev on 127.0.0.1:5174, and its identity came from a dev proxy injecting headers from an environment variable.

portal/ is now retired; the console replaces it. Keeping both would have meant two frontends against one read model, drifting — which is the same failure this RFC spends §3 avoiding between Rust and TypeScript, at the UI layer.

The measurement that makes this urgent: AUTH-24 — “sponsor:edit never implies deploy” — grounded on the deployer role, examines 0 records in Studio. A check there would report success forever, having examined nothing. The machinery to refuse that exists and nobody outside the repo can see it work.

2. The obstacles, and what each forces

obstacle	consequence
the Rust service has no natural Vercel runtime	the reads and writes are ported to Route Handlers
the JSONL logs need a filesystem serverless does not have	genuine runtime state moves to Neon; nothing else does
identity comes from a Vite dev proxy	Google OAuth restricted to one Workspace domain by the hd claim, read server-side, never from a body or a client-settable header
the adapter is reached at localhost:3010	it becomes a configured origin that degrades honestly when unset

Two things do not move. The corpus stays generated and gated in CI — the console imports the committed read-model JSON, so a page cannot render a corpus_version other than the one it shipped with. And the Rust service stays on the Bazel/plugin plane: backend.rs is a filesystem estate indexer for the Lean plane, which has no meaning on Vercel and no reason to leave.

3. The risk this RFC is mostly about

The port duplicates three rules: the vacuous refusal, the pending overlay, and the adoption computation.

Two implementations of a safety rule diverge silently. Not loudly — each keeps passing its own suite while they drift apart, and the suites are the only thing anybody looks at. The rule that decides whether a green build tested anything is the worst possible candidate for that.

So the cases live in conformance/*.json, in a language neither implementation is written in, and both execute those. Porting the tests alongside the logic was considered and rejected: it leaves two suites free to drift in exactly the way the two implementations are.

3.1 The part that does not work yet, said plainly

//services/spec:spec_test — where the Rust half runs — executes only when CI can mint a token for the private plugin crates. That step is continue-on-error and it has been skipping. On an ordinary PR the TypeScript half runs and the Rust half does not.

Three mitigations, in the order they pay off:

1. conformance/check_conformance.py — stdlib-only, no toolchain, runs unconditionally under //conformance/.... It parses the constants out of both sources and re-derives every evaluation verdict from them. Dropping Examined from POSITIVE — a one-word edit that silently permits a vacuous pass under a quieter name — fails three checks on a normal PR. Verified by making the edit and watching it fail.
2. The reader ⊆ vocabulary check (§5.2), which catches the class of bug that motivated it.
3. Making the skipped step visible in the job summary, so “did the Rust half run on the commit that shipped?” is answerable after the fact.

⚠ The residual hole. All of that checks the data the rule is made of, not the control flow that reads it. Reordering the guards in evaluation::check so the zero-check becomes unreachable leaves every constant intact and passes. Only //services/spec:spec_test catches that, and it needs the credential fixed. These are mitigations for that target being unrunnable, not a replacement.

4. Shape

One Next.js app. The eight corpus reads are imported, so those pages are pure functions of the build. Only the overlay needs the database.

console/
  lib/evaluation.ts     the vacuous refusal        <- conformance/evaluation_cases.json
  lib/overlay.ts        pending + adoption         <- conformance/overlay_cases.json
  lib/evaluated.ts      measurements, and stateOf (the display half of the refusal)
  lib/proposal.ts       the closed op vocabulary, 17 constructors
  lib/canonical.ts      canonical JSON — the pre-image of a content address
  lib/corpus.ts         the imported read model, and CORPUS_VERSION
  lib/project.ts        which project a pane opens on, and the unscoped-row rule
  lib/auth/             Google OAuth, and the session cookie
  db/migrations/        the two append-only tables
  app/                  seven panes, six route handlers
  test/conformance.test.ts
  test/project.test.ts

Requirements and Terms render the corpus statically and fetch the overlay client-side. The alternative — applying the overlay server-side — has two defects: a database outage makes the corpus itself unviewable, and it conflates “nothing is pending” with “could not ask”. With the split, the corpus is always readable and pending state is either attributed or explicitly absent:

could not read pending proposals — showing the corpus only

which is a different statement from “nothing pending”. That is the same distinction as Vacuous versus CannotBeGrounded, applied to the overlay.

The overlay is never cached. It is rebuilt on read rather than invalidated, so a write is visible on the very next request without an invalidation protocol to get wrong. A stale overlay tells an author their write did not land.

5. What landed in this change

5.1 Two op-vocabulary bugs, and one that was not one

Three of six write paths answered 422 and appended nothing:

• amendNS sent discipline; OPS did not declare it → fixed in OPS.
• assertNS sent project; OPS did not declare it → fixed in OPS.
• retractNS omitted the required reason → fixed in the caller.

The third is the interesting one. retractNS requiring a reason is deliberate — “retract never deletes; it demotes,” and a demotion with no stated ground is indistinguishable from a mistake. So Withdraw now asks for the ground rather than the vocabulary accepting its absence.

Both OPS gaps had the same shape: overlay.rs already read the fields the door rejected. The two halves of the write path disagreed in the direction where the feature simply does not work, and nothing said so.

5.2 So the disagreement is now a gate

check_conformance.py parses every s(op, "field") out of overlay.rs’s match arms and asserts the field is one that proposal.rs::OPS declares for that op. Reverting either fix fails it with the reason. Nothing in the type system connects a field read to the OpSpec that permits it, so the connection is made there.

5.3 A served route nobody declared

POST /evaluation was served since #29 and named in no routes.rs table. routes_match_describe compares GET routes only, and check_wiring.py checked declared→registered but never the reverse — so the shell could not resolve spec.v1.Authoring/SubmitEvaluation, and the failure reads in a browser as a console bug. Declared now, and check_wiring.py checks both directions (169 → 194 checks).

5.4 A silently dropped proposal

materialize.py split its log with str.splitlines(). Python splits on U+2028, U+2029 and U+0085; JSON does not, and serde_json emits all three raw inside a string. A proposal carrying a LINE SEPARATOR — pasting from a PDF is the usual way — became two fragments, neither of which parsed, and both were skipped by the except. The record stayed in the log, never promoted, and read as “pending, not yet adopted” in the console forever, with no error anywhere.

Measured, not inferred: one such line splits into 2 pieces and 0 of them json.loads(). Fixed to split("\n"), and the database refuses to hold such a line at all (§6).

6. Neon

Two tables, spec.proposal_log and spec.evaluation_log — separate, because replaying judgements and measurements from one table would make “who decided this” and “what did it measure” the same question.

Each row stores the log line verbatim plus derived columns, with a CHECK that the decomposition matches the line. Export is then SELECT line ORDER BY seq, with no serializer that could reorder keys — which matters because canonical is the pre-image of a content address, and jsonb would sort keys by length-then-bytes rather than lexicographically.

Append-only is enforced by the database:

• statement-level BEFORE UPDATE/DELETE/TRUNCATE triggers that raise. Not a rule that swallows: DO INSTEAD NOTHING makes the UPDATE succeed affecting zero rows, which is the same family of error as reporting a pass over an empty population.
• INSERT, SELECT grants and nothing else. TRUNCATE is a separate privilege and is not implied by DELETE — leaving it reachable empties the log in one statement.
• a CHECK constraint that is the fourth independent refusal of a vacuous pass, and the only one that survives a hand-written INSERT.

Ordering: an advisory lock in the append function, because GENERATED AS IDENTITY allocates seq before commit, so two invocations can take 41 and 42 and commit in the other order. “Later wins” must not depend on who fsynced first.

log_offset (a byte offset) becomes log_seq. Nothing read it, so this is a documented-surface change rather than a consumer-breaking one.

7. Identity

The rule is unchanged: a write with no principal is refused, never attributed to nobody. What changes is where the principal comes from. spec’s plugin trusts x-fastverk-user-sub because a gateway it trusts injected them; the console is the edge, so anything client-supplied is client-controlled. The session is read server-side on every write.

The dev shim returns null when unconfigured, so an unconfigured environment refuses writes. There is no dev@localhost fallback: a default author is attribution to nobody wearing a name. Because the log is append-only, a dev-authored record can never be removed — so it stamps sub as dev:<email>, self-labelling forever.

Since #48 there is a second source of a principal, and it is a different type on purpose. A consumer’s CI holds a machine credential — an HS256 JWT under its own secret, aud spec-console:evaluation, a required expiry and a revocable jti (RFC-004a §4) — and console/lib/auth/machine.ts resolves it to a MachinePrincipal: sub machine:<implementation>, no email, no kernel, no agent capability. It is not assignable to Principal, so it cannot be handed to checkProposal; only the evaluation route consults it, so it cannot reach the op door; and checkOp refuses the machine: prefix regardless. A machine reports what it measured and may not author, and the type system, the routing and the door each say so separately. Like dev:<email>, the machine: author is self-labelling forever in an append-only log.

8. The adapter, and the promotion loop

The adapter is deferred. Its commits are unpushed on a GitLab repo by standing instruction. It becomes a configured origin; unset, the proxy answers 503 with outcome: "CANNOT_BE_GROUNDED" in the shape the client already handles, so the UI renders an honest state rather than an error toast. It must never manufacture {population: {count: 0}} — that is indistinguishable from a real zero and would fabricate the exact vacuous measurement the door refuses.

This costs less than it looks. The vacuous refusal is a pure function of the submitted measurement and does not care where the count came from, so the AUTH-24 refusal is demonstrable the moment any measurement source reports zero. Wiring a live Studio is one environment variable.

Promotion runs from CI, not from Vercel — .github/workflows/promote.yml since #49: export with a SELECT-only credential (pinned to a seq, so the two logs describe one moment), materialize.py, re-emit the read model, run the gates, open a PR. A human merges it. The PR diff — appended log lines, regenerated proposals.ttl, regenerated payloads, new corpus_version — is the reviewable step between “someone clicked a button” and “the specification changed”.

The hole this used to leave, now closed. Nothing checked that corpus/studio/proposals.ttl corresponded to any log — every gate ran over it as committed, so a hand-edited one passed all of them and invariant ⑥ was a comment. logs/*.jsonl is committed and //corpus/studio:proposals_ttl_matches_the_log re-materializes from it, so promotion must update the log and the TTL together in one reviewable diff. Shown to reject both ways: editing the TTL fails, and adding a log line without promoting it fails.

The snapshot is committed rather than treated as a build artifact for a second reason: Postgres cannot defend against its own owner, and a row can vanish from a table without trace where a line cannot vanish from a reviewed diff.

On stale parent: corpus_version is one global digest across all projects, and proposals.ttl is inside it, so every promotion necessarily advances it and makes every open tab stale. parent is therefore provenance, not a precondition — it stays unvalidated at the door, the console says when it is behind, and promotion never rewrites it. Rewriting parent to the current version at promotion time would be falsifying provenance, and it is the one edit in this area that would be silently wrong.

9. What the console does not carry, and why

portal/ had ten panes. Seven are ported: Overview, Requirements, Grounding, Conflicts, Proposals, Document, Settings. Three are not, each for a reason:

pane	why not
Proof	reads the Lean estate off the filesystem via backend.rs. There is no filesystem on Vercel and no reason to invent one — it belongs to the Bazel/plugin plane, where it already works.
Plan mode	was a placeholder saying it is not built. It still is not, and a nav entry that only says so is worse than its absence.
Liveness	same.

Settings is not a port. The portal’s was a hard-coded table naming an adapter URL that was true on one laptop; the console’s reads /api/health, so it cannot be wrong about the deployment it is running in.

9.1 Which project a pane opens on

The corpora are loaded as separate graphs and never merged, so every pane showing project-scoped rows must pick one. Each picked for itself: Overview and Document spelled a preference inline, Conflicts took projects[0] — alphabetical, so ampere — and Requirements had no notion of a project at all and listed all 133 rows of both products interleaved, offering all 27 disciplines of two businesses that share none. console/lib/project.ts is now the one place that decides, and DEFAULT_PROJECT is studio.

The default moved; the data did not. ampere stays in the payloads and stays one click away, because dropping it would be a change to what the gates measure wearing the clothes of a display change:

payload	ampere	studio
conflicts	12	0
envelopes	2	0
witness rows	33	0
requirements	64	69

studio is prose at R0/R2 with no typed quantities, so nothing in it can produce an empty envelope or a modality clash. A corpus without ampere would run the conflict and envelope gates over rows that cannot trip them — a gate that examines nothing and reports success forever, which is invariant ③ inverted.

Two consequences worth stating rather than discovering:

• Conflicts now opens empty, on a pane whose only data is ampere’s. That is the honest reading: studio has no conflicts because nothing in it is typed enough to have one, and the empty state says so. The picker offers ampere.
• A row that names no project is shown in every project, never in none. assertNS and bindTerm both take project optionally, and the overlay already resolves an unscoped bindTerm against every corpus that uses the surface (overlay.find). Filtering with row.project === p instead would make a claim proposed without a project invisible in every pane at once, while sitting adopted in the log — the author submits, the list does not change, and nothing on screen says why. inProject is that rule, and it is unit-tested because this corpus has no such row to catch a regression.

10. What is not done

• The export step in §8 is documented and not automated — automated in #49 (.github/workflows/promote.yml, daily or on dispatch). ⚠ It cannot run until NEON_EXPORT_URL is set in the corpus-production environment, so logs/*.jsonl is still empty and every gate over it is examining nothing. The migrations themselves have since run against Neon, from CI under the database-production environment, and db/verify.mjs re-proved the refusals there in a rolled-back transaction.

• The npm package that carries the read model and fixtures across the repo boundary is not built; the console reads both by relative path, from one file each, so extraction is a two-line change. ⚠ Since #52’s first PR the read model is behind the @readmodel/ alias rather than a relative path — SPEC_READMODEL_DIR points a per-tenant deployment at payloads emitted from its own corpus. That is the seam that makes a second tenant possible without the package; it is not the package.

• Two live write paths. services/spec can still append to a file. Both are “the” log; neither sees the other. Retiring spec’s write path is a config change — SPEC_PROPOSAL_LOG unset already answers 503 with a stated reason — and it must happen in the same change that points the console at Neon. Closed in #44, and not as a config change. Leaving it to configuration was the wrong instinct: an unset variable is a state an operator can restore, and what was needed was for the second door to stop existing. POST /proposal and POST /proposal/op on the plugin now answer 410 Gone with a use_instead naming the console’s routes — 410 rather than 404 because the route existed and works, and its removal is a decision rather than a deployment fault.

  The reason it could not wait: two doors are two implementations of the content address, and they had already diverged. The plugin’s flat-form lift coerced bound_value: "70" to the float 70.0; the console’s leaves it a string. Same submission, two canonical bodies, and — once the door computed a name — two permanent names. services/spec still READS the log (the pending overlay is served from it); it no longer writes one. The plugin’s POST /evaluation is a separate question and is still live: a measurement is not a judgement, and it has no address to disagree about.

• The Rust conformance tests are written but not compiled. The private crates 401 in this environment and protoc is absent, which is the same hole CI has.

• The OAuth flow has since been run end to end against the live deployment by a savvifi.com account. What is still unverified is the refusal: no sign-in has been attempted from outside the hosted domain, so GOOGLE_ALLOWED_DOMAIN is proved to admit and not yet proved to reject. The RULE is proved to reject as of #52’s first PR — checkClaims was lifted out of exchangeCode (which talks to Google’s token endpoint first, and was why nothing could reach the rule) and console/test/google.test.ts runs every branch, including the case the module header exists for: a consumer Google account carrying ada@savvifi.com as an alternate address and no hd, which email alone would have admitted. The unset allow-list is proved to throw rather than admit everybody.

  ⚠ The deployment is still proved only to admit. No sign-in has been attempted from outside a hosted domain against a live console. Those are two claims and only one of them changed.

from docs/rfc-004-agents.md

RFC-004 — making the console useful: measurement first, agents where judgement lives

Status: proposed. Companion to RFC-003 (the hosted console). RFC-003 shipped a console that can write and has never been written to. This one is about the fact that nothing in it has ever moved.

---

1. What is actually broken

Agents are not the bottleneck, and the plan says so before it uses them. The request was for eve agents; the goal is a useful app. Those are not the same thing, and the evidence says the shortest path to the second does not start with the first. State it once, plainly, then get on with the plan.

Studio’s numbers, read off the committed read model at corpus:0e06b2f9fd1047a1: 69 requirements, 0 evaluated, every one carrying population "—" and outcome "NOT-EVALUATED" (services/spec/readmodel/requirements.json). 107 term rows over 60 distinct surfaces, 0 bound, 0 retired (services/spec/readmodel/terms.json). Both append-only logs are 0 bytes (wc -l logs/*.jsonl). corpus/studio/proposals.ttl is 22 lines of header. The grounding page currently reads “60 not pinned down · 60 total” (console/app/grounding/GroundingClient.tsx:39-45 groups holes by surface, not by row) above an alert that says “No grounding adapter is answering.”

Nothing here is blocked on authoring throughput. Four things are broken, in descending order of how much they cost:

1. No population source. spec.v1.GroundingAdapter (proto/spec/v1/grounding_adapter.proto:117-122) has zero implementations anywhere. The console proxies to it (console/app/api/ground/[...path]/route.ts:43) and nothing calls the proxy.
2. Binding a term does not move a requirement. blocked_on and rung are frozen literals written once by tools/import/decompose.py:138-146 and read back verbatim by tools/readmodel/emit_readmodel.py’s Q_REQUIREMENTS (OPTIONAL { ?claim au:stalledOn ?stall }). Nothing derives either.
3. Promotion drops 11 of 17 ops. tools/proposals/materialize.py:139-156 dispatches six kinds and else: continues the rest, silently.
4. Promotion is five hand-run commands. .github/workflows/ holds ci.yml and migrate.yml and nothing else.

Only (1) requires a customer. None requires an agent. And two of the four units this repo measures in are already live-rendered from the log: console/app/api/overlay/route.ts:38-48 rebuilds the overlay on every request with revalidate = 0; console/lib/evaluated.ts:63-65 overwrites population and outcome on the requirement row; console/lib/overlay.ts applyTerms sets bound_to and open. One authenticated POST /api/evaluation — a deployed, correct, authenticated route whose only mention anywhere in console/app is its own route.ts — changes AUTH-24 from — / NOT-EVALUATED to “1,412 records, undecided” (console/lib/evaluated.ts:113-116) on the next page load. No service, no promotion, no redeploy.

So the plan front-loads the parts that need nobody’s permission, and puts eve where a machine genuinely cannot decide: choosing between three readings of a word that differ by 47 records.

Assumption this plan runs under: SAVVI wants the app useful to a product owner within one quarter, and is willing to spend a Studio engineer’s time on a Probe endpoint. If Studio cannot fund that, stop after Phase 2 — everything after it is scaffolding around a count that will never arrive.

---

2. The shape

  CUSTOMER ENVIRONMENT                VERCEL (one project, one deploy)
  ─────────────────────               ────────────────────────────────
  studio-nextjs                       console/            (EXISTS)
   ├ POST /api/spec/probe    ◀──────── /api/ground/[...path]  (EXISTS, dead)
   ├ POST /api/spec/evaluate           /api/proposal/op       (EXISTS, 1 caller)
   └ GET  /api/spec/health             /api/evaluation        (EXISTS, 0 callers)
     (holds Studio's DB credential;    /api/overlay           (EXISTS, live)
      spec holds none)                 /api/derive            (Phase 6 only)
        ▲                             console/agent/     (Phase 5)
        │ x-vercel-oidc-token          ├ grounding-interviewer
        │ aud = studio host            └ drift-watch      (Phase 6)
        │                                mounted by withEve() at /eve/v1/*
        │                                     │
  ══════╪═════════════════════════════════════╪══════════════════════
        │                                     ▼
        │                              NEON  spec.proposal_log
        │                                    spec.evaluation_log
        │                                    (append-only, +drafted_by)
        │                                          │
        │                                          │ promote.yml (Phase 4)
        ▼                                          ▼
  CI — BAZEL (unchanged home of all symbolic checking)
   ├ //rdf:gates.bzl               40 corpus gate targets
   ├ //rdf:authoring_gates.bzl     4 gates + 4 measures  ← Phase 4 repairs
   ├ //conformance:conformance_test   evaluation + overlay + STALL (Phase 2)
   ├ //tools/readmodel:emit           derived stall lands here (Phase 2)
   └ //corpus/studio:proposals_ttl_matches_the_log

  AWS FARGATE — nothing, until §4's trigger condition fires.

What existing files become what. console/lib/overlay.ts and console/lib/evaluated.ts stay the only overlay implementations and gain no third runner. tools/readmodel/emit_readmodel.py gains the derived stall and becomes the corpus-side half of a new conformance fixture. java/BUILD.bazel’s thirteen entry-point-less java_library targets gain exactly one java_binary — //java:gate_cli — invoked by Bazel, not by a server. rdf/lint/authoring/envelope-unrecorded.rq gets rewritten and gains the positive control rdf/lint/authoring/fixtures/BUILD.bazel:71-77 says was skipped. proto/spec/v1/invariant.proto gains one enum value. services/spec/ is not touched: backend.rs indexes a Lean estate that has no meaning here, and build.rs:1-3 generates message types only, so adding gRPC there is new codegen with no caller.

AWS gets nothing in Phases 0–5. The corpus is 220 KB of Turtle across 3,669 lines; the gates are sparql_query_test rules that run hermetically in CI. A Fargate task would be a warm JVM idle 99.9% of the time, and Fargate cannot scale to zero. §4 specifies the service in full and names the condition under which it earns its keep, so nothing blocks on the decision.

---

3. The agents

Two eve agents, both mounted into the existing Next.js project with withEve(nextConfig) — console/package.json is Next ^15.5.0 / React ^19.2.8, which matches vercel/eve’s own apps/frameworks/next example. Same origin, no CORS, no agent credential, no URL env var. The build requires Node ≥ 24, so @types/node moves off ^22.10.0.

Neither agent lands before Phase 5. Both are scoped by one rule: an agent gets a job only where a deterministic script demonstrably loses.

3.0 What the script wins, measured

Of Studio’s 60 surfaces:

class	surfaces	rows	how a script disposes of it
colon-form permission tokens (sponsor:edit, deploy:*, …)	8	38	exact match against Studio’s permission enum
decomposer noise (or, act, rule, not rows, deletion, intersected, at issue time)	6	6	retractTerm — “this is not a term”
identifier-shaped (team_memberships, sponsor_grants.created_by_id, /dev/login, …)	9	9	exact match against the schema catalog
residual — judgement (public, admin, org admins, SAVVI admin, reseller agreement, two-level hierarchy, …)	37	54	somebody has to decide

All 38 colon-form rows come from term_source: "code-span" — the author’s own backticks (tools/import/decompose.py reads terms off markup and nothing else). Exact string matching over an author’s deliberate code span is not a task an LLM improves. It is replayable, fingerprintable, free, and structurally incapable of inventing a count. 23 of 60 surfaces and 53 of 107 rows go to a script, and that fully disposes of 14 of the 46 decomposed requirements — including AUTH-24, whose only two terms are sponsor:edit and deploy:*.

That is the answer to “is an agent the right tool” for the majority of the named work: no, and the script ships first. The script is not an agent in disguise — it emits a reviewable list of proposed ops, one human reads it once, and the batch is POSTed under that human’s session. One judgement covering 38 rows, honestly attributed.

3.1 console/agent/grounding-interviewer/ — Phase 5

Job. The 37 residual surfaces. For public, Studio’s schema plausibly offers organizations.visibility = 'public', sponsor_grants.public = true, and a public_sponsor_permissions column; those are three different populations and choosing between them is a statement about the business. The agent runs the probe, presents the readings with their counts, and parks.

Deterministic alternative considered: a ranked candidate list rendered in the grounding page with no model at all. It loses on exactly one thing — the residual surfaces are the ones where the right question is not obvious from the schema (reseller agreement, two-level hierarchy, Lifecycle management are not columns), and an interview that reads the requirement’s prose and proposes candidate locators is genuinely language work. That is a narrow win over a dropdown, and it is the only win claimed.

Files.

console/agent/grounding-interviewer/
  agent.ts            model; limits.sessionTimeoutMs = 7 days (explicit, not false);
                      limits.maxInputTokensPerSession set; disableTool() on the
                      built-in bash and web_fetch harness; NO sandbox slot.
  instructions.md     the six invariants; the closed 17-op vocabulary; the standing
                      rule that it may not state a number.
  instrumentation.ts  recordInputs: false, recordOutputs: false. Both default TRUE.
  channels/eve.ts     AuthFn reading the console's spec_session cookie →
                      { principalId: "google:<sub>", principalType: "user" };
                      turnPolicy: "queue".
  tools/list_open_surfaces.ts    read /api/overlay, rank by claims waiting
  tools/read_requirement.ts      the predicate text and its named terms
  tools/probe_term.ts            calls /api/ground/probe; STRIPS examples in execute()
  tools/propose_binding.ts       approval: input-dependent policy
  tools/propose_retraction.ts    approval: always()
  skills/reading-a-probe.md
  skills/what-is-not-a-term.md
console/evals/
  evals.config.ts
  probes-before-proposing.eval.ts     t.toolOrder(["probe_term","propose_binding"])
  never-proposes-unmeasured.eval.ts   probe returns 0 → t.notCalledTool("propose_binding")
  parks-before-every-write.eval.ts    t.parked()
  never-types-a-number.eval.ts        t.calledTool("propose_binding", { input: {...} })
                                      asserting the input carries no population field

The model cannot type a number. probe_term writes {locator, count, query_fingerprint} into eve session state keyed by (term, index). propose_binding’s inputSchema is { term: string, probe_index: number, definition: string } — there is no population and no query_fingerprint field. The tool re-reads both from session state and builds the op body server-side. This is the single most important line in this section: Design 1’s fatal defect was a model-typed population flowing into an append-only table that has no DELETE, and every existing refusal tests population > 0, never provenance (console/lib/evaluation.ts:138-153, services/spec/src/evaluation.rs:102-117, tools/proposals/materialize.py:115-117, console/db/migrations/0001_schema.sql:143-145).

Examples never reach the agent. probe_term strips examples inside execute(), not via toModelOutput. toModelOutput projects what the model sees; the durable workflow checkpoints the tool’s actual return value so it can replay a resumed run, so an un-stripped result puts Studio’s customer rows at rest in Vercel Workflow storage — inside spec’s own plane, where //proto/spec/v1:data_boundary_test cannot see them. The browser fetches examples directly from POST /api/ground/probe for rendering. This is the only sound answer to invariant ① under durable execution.

Forbidden. No bindTerm without a probe with count > 0 in the same session — enforced by the approval policy returning {type: "denied", reason: "a binding nobody measured is the shape this system refuses — probe first"}, which the model reads rather than retries. No assertNS, no amendNS, no retractNS, no openConflict, no declarePrecedence: those tools do not exist, and a tool that does not exist is a stronger refusal than one that is denied. No evaluations — record_evaluation is deliberately not an agent tool (§3.3).

Identity in the log. author is the approving human’s google:<sub>, taken from ctx.session.auth.current, which the channel AuthFn derived from the console’s own cookie. surface is "Agent" — accepted since 0001_schema.sql:92 and set by nothing today (console/app/useOverlay.ts:66 hard-codes "Meridian"). The agent is recorded in a new column drafted_by = 'eve/grounding-interviewer@<VERCEL_GIT_COMMIT_SHA>'.

We never construct an agent principal. console/lib/proposal.ts:141-146 rejects any agent op that is not assertNS at R0, before the capability table is consulted; that rule stays enforced and untouched, and no code path in this plan tries to route around it. The agent is an instrument, not an author.

Where a human approves. In the eve pane in the console, and in Slack. The approval request carries the full op body plus the probe’s locator, count and fingerprint — never an opaque handle. There is no mutable staging table: a draft that nobody approves leaves no row anywhere, which is both invariant ② one level up and the fix for an audit trail that was mutable while the outcome was permanent.

3.2 console/agent/drift-watch/ — Phase 6, conditional

Job. Re-probe every bound term’s stored query_fingerprint on a cadence. When a count moves without a corpus change, open a thread asking a named human whether the referent drifted. This is the DRIFT half of the three failures and the only component that produces value on a schedule.

File: console/agent/drift-watch/schedules/nightly.ts using defineSchedule({ cron, run }) — the handler form, not markdown. Markdown/task-mode schedules are fire-and-forget and cannot park for a human, and a drift finding that cannot ask is a drift finding nobody acts on.

Deterministic alternative considered — and it wins for the detection half. A cron job that re-probes and diffs needs no model. The agent earns only the second step: turning “sponsor:edit went 1,412 → 1,398” into a question worth a person’s attention, with the requirement text and the 11 claims that wait on it. So the schedule’s run() does the diff deterministically and only invokes the model when a threshold is crossed. Ship it that way.

Hard prerequisite, non-negotiable. This agent issues aggregate queries against a customer’s production database on a timer, unattended, with retry amplification underneath it (eve steps run up to four attempts; there is no per-tool timeout, only ctx.abortSignal). It does not ship until Studio’s adapter has a statement_timeout, a read replica or equivalent, and this schedule has a per-night probe budget and a circuit breaker. Absent those, the worst realistic incident is that the spec console degrades Studio’s production database at 03:00 UTC and Studio’s on-call is paged for a system they do not operate.

3.3 What has no agent, on purpose

Recording an evaluation. record_evaluation is a console form, not a tool. The human picks the outcome from Examined | Vacuous | CannotBeGrounded; the population and query_fingerprint come from the probe response the form already holds. Two failure modes are closed at once: a model cannot type a count, and the adapter cannot decide the predicate. The proto’s willingness to carry OUTCOME_PASSES over the wire (proto/spec/v1/invariant.proto:131-138) is a defect to route around, not a feature to consume — a wire PASSES or FAILS is logged as a protocol violation and refused, never recorded.

Promotion. promote.yml is a workflow, not an agent. It opens a PR; a human merges.

The 23 undecomposed requirements. 22 of them carry zero author markup. The correct intervention is asking their author to mark up their own sentences — a Slack message, not a pipeline.

---

4. The services

4.1 What changes in proto/spec/v1 — Phase 1, one line

// proto/spec/v1/invariant.proto:131-138
enum Outcome {
  OUTCOME_UNSPECIFIED = 0;
  OUTCOME_PASSES = 1;
  OUTCOME_FAILS = 2;
  OUTCOME_CANNOT_BE_GROUNDED = 3;
  OUTCOME_VACUOUS = 4;
  OUTCOME_EXAMINED = 5;   // ← NEW
}

au:Examined has existed in the ontology since RFC-002 (rdf/ontology/authoring.ttl:454-456), is in OUTCOMES (console/lib/evaluation.ts:54), and is in the table’s CHECK (0001_schema.sql:128). It is not on the wire. Without this line a conforming adapter physically cannot say “I measured 1,412 records and I refuse to decide the implication” — the one honest answer to AUTH-24. DisplayExample stays declared only in grounding_adapter.proto and invariant.proto keeps importing nothing, so //proto/spec/v1:data_boundary_test passes unchanged.

4.2 The adapter — the customer’s service, and it is HTTP

spec.v1.GroundingAdapter.Probe/Evaluate, implemented in studio-nextjs as protobuf-JSON route handlers at POST /api/spec/probe, POST /api/spec/evaluate, GET /api/spec/health. The .proto stays the schema of record; the transport is JSON because console/app/api/ground/[...path]/route.ts:43 already POSTs to exactly ${GROUNDING_ADAPTER_URL}/api/spec/<path>, and services/spec/build.rs:1-3 generates message types only with no proto_library in proto/spec/v1/BUILD.bazel — gRPC here would be new codegen serving no caller.

It runs in Studio’s environment because grounding_adapter.proto:114-116 says so: “Implemented BY THE PROJECT, called by spec … a project can implement this without granting spec any credential.” Hosting it on our Fargate would require Studio’s database credential in our account — invariant ① broken at the infrastructure layer while every line of code still looks correct.

Auth, Vercel → Studio. getVercelOidcToken({ audience: 'https://<studio-host>' }), verified by Studio against the oidc.vercel.com JWKS with aud and environment:production pinned. Not the default-audience token. Vercel’s default OIDC aud is https://vercel.com/<team-slug> and its sub is owner:<team>:project:<project>:environment:<env> — precisely the claims an AWS trust policy pins for sts:AssumeRoleWithWebIdentity. Forwarding the raw token would hand a customer-operated service, on every probe, a credential replayable against STS for any role in our account trusting that project. Audience-scoping is one parameter and it inverts nothing.

Probe is the deliverable. Evaluate may never ship, and that is acceptable. Probe is a count over a schema. Evaluate for AUTH-24 is a decision procedure over Studio’s authorization lattice — 25 of 69 Studio predicates use implication/lattice language and 0 carry a numeric threshold. If Studio ships Probe and stops, every Studio requirement lands on Examined forever. Say that out loud now: no Studio requirement can ever read “Enforced” under this plan. console/lib/evaluated.ts:94,103 gates Enforced on outcome ∈ {Passes, Fails}, and this plan deliberately forbids the adapter from producing either. A stakeholder shown the page will see zero green chips and a column of numbers. That is the honest state and it is enormously better than —, but nobody should be told otherwise before funding it.

4.3 The Fargate service — specified, not scheduled

Trigger condition. Build this when either holds, and not before: (a) the corpus carries ≥ 1 au:Quantity with bounds, so a preflight over the post-admission graph has something to examine — Studio has zero, so envelope_unrecorded would preflight nothing today; or (b) the console needs to answer “what would admitting this proposal do to the gates” interactively for a corpus that has grown past the point where CI’s answer arrives soon enough. services/spec/src/proposal.rs:30-34 names this gap in the code: “that is a GROUP BY … HAVING over the post-admission graph and this plugin has no query engine.”

Surface. A new proto/spec/v1/derivation.proto, importing nothing from grounding_adapter.proto — it carries counts, never rows, so the data-boundary test extends unchanged.

RPC	maps to what exists	Bazel target that computes it today
Derivation.Derive(corpus_version, hypothetical_bindings[]) → DerivedRequirement[]	the Phase 2 stall rule, run online instead of at emit time	//tools/readmodel:emit + //conformance:conformance_test
Gates.RunGates(project, suites[]) → GateReport	the 4 authoring gates + 4 measures	//rdf:authoring_gates.bzl (3 instantiations)
Gates.Preflight(parent_corpus_version, ops[]) → GateDelta[]	nothing — this is the named gap	java/kg/edit/WriteOps.applyAndCheck(edits, kgRoot, apply=false)
Gates.SelfTest() → GateFireResult[]	the adversarial control never wired	//rdf/lint/authoring/fixtures + //grounding:adversarial_gate
Gates.Explain(gate) → {sparql, population_sparql, rationale}	the .rq frontmatter	//rdf:lint filegroup
grpc.health.v1.Health/Check	nothing — services/spec/src/main.rs:108-140 registers only meridian LayoutService	—

GateResult carries status ∈ {PASSED, FAILED, EXAMINED_NOTHING} and an examined count. That idea is the single best thing in any of the three candidate designs and it does not wait for this service — it lands in Bazel in Phase 4 (§5).

Deployment. One ECS Fargate task, 1 vCPU / 2 GB (sized for the JVM’s warm Jena Dataset, not for the data — the corpus is 220 KB), us-east-1, image to the existing private ECR at 042825952740.dkr.ecr.us-east-1.amazonaws.com named in deploy/charts/plugin-spec/values.yaml:4-9. Public subnet, security group admitting only the front door; no NAT gateway (+$32.85/mo for nothing — the task has no outbound need). Deployed by a workflow modeled exactly on migrate.yml:18-21,63: workflow_dispatch and push-to-main only, never pull_request, gated by a compute-production GitHub Environment with a required reviewer, GitHub OIDC to an AWS role. Day-one blocker: the image build needs a GitHub App token for the private fastverk-plugin-crates repo — ci.yml:81-84 records the live 401, and MODULE.bazel:170-173 records that the Bazel OCI image “could not be built by CI and had to be produced by hand.”

Auth from Vercel — a Lambda Function URL, not an ALB. AWS_IAM auth type, SigV4-signed with credentials from sts:AssumeRoleWithWebIdentity against https://oidc.vercel.com/<team>, transcoding JSON to the task. This is the only free, keyless path. ALB has no SigV4 authorizer — its built-in auth is redirect-based OIDC for interactive users — so a gRPC ALB front door means mTLS with a client certificate living in Vercel env, unrevokable without a CRL pipeline nobody will run, and present in every preview deployment. gRPC and Vercel-OIDC meet at no AWS front door except VPC Lattice, which needs Enterprise Secure Compute peering. gRPC is kept between the Rust and JVM containers on loopback, where it is free, and off the internet-facing hop, where it costs the auth story.

Cost. Fargate 1 vCPU / 2 GB = $36.04/mo (0.25 vCPU / 0.5 GB = $9.01 if the JVM is dropped); Lambda + Function URL ≈ $0 at this volume; ECR ~$1; CloudWatch ~$1 if Rust tracing stays at info. ≈ $38/mo, no ALB, no public IPv4, no NAT. Two AZs: ≈ $75/mo. Fargate cannot scale to zero, so that floor is unavoidable — which is exactly why it waits for a trigger condition.

Explicitly refused in this service: health checks gated on SelfTest (a data defect becomes a crash-looping outage with no rollback signal, since the image is fine and every replacement task fails the same deterministic check); reusing SESSION_SECRET as a service credential (console/lib/auth/session.ts:22-33 — “a known secret lets anyone forge a session, and a forged session forges an author”); and colocating the JVM and the front door in one task at one replica.

---

5. The phases

Each phase names a number a SAVVI person can watch move, and the gate that proves it. Phase 0 is measured in hours.

Phase 0 — retract the six noise surfaces. Day 1.

Six retractTerm ops through the already-deployed grounding page, one per noise surface: or, act, intersected, at issue time, rule, not rows, deletion. retractTerm is in the closed vocabulary (console/lib/proposal.ts:52-53), materialize.py:145-146 dispatches it, and console/app/grounding/GroundingClient.tsx:39-45 drops a retracted surface from the hole list entirely.

• Number: the grounding page reads “60 not pinned down · 60 total” → “54 not pinned down · 54 total”. spec.proposal_log goes 0 → 6 rows, the first in the repo’s history.
• Gate: GET /api/overlay returns records: 6; AUTH-23 — the one requirement blocked only by noise — has an empty term queue.
• Cost: zero code, zero dollars, one person, twenty minutes.

Phase 1 — the deterministic binder and the evaluation form. Week 1.

Three things, none of which needs anybody outside this repo.

1. OUTCOME_EXAMINED = 5 in invariant.proto; au:Examined added to vacuous-invariant.rq:24’s refused set, which today filters only au:Passes/au:Fails and is therefore the weakest of the four zero-refusals.
2. tools/import/bind_catalog.py — reads a Studio-supplied catalog of permission tokens and schema identifiers, emits a reviewable JSON list of candidate bindTerm ops for the 8 colon-form and 9 identifier-shaped surfaces, exact match only, no fuzzy matching, no model. A human reads the 17 rows once and POSTs the batch under their own session.
3. An evaluation form in the console — the first caller POST /api/evaluation has ever had. Outcome narrowed to Examined | Vacuous | CannotBeGrounded.

Also in this phase, because Phase 5 depends on it and it is cheap: add locator, query_fingerprint, population to bindTerm’s optional list in both console/lib/proposal.ts:44-45 and services/spec/src/proposal.rs. The vocabulary stays at 17, which is all check_wiring.py:383 asserts. Without this, checkOp’s unknown-field rejection (proposal.ts:105-108) means a binding’s evidence cannot enter the log line, the canonical bytes, or the promoted TTL — and a permanent corpus statement would be forever indistinguishable from a guess.

• Number: open holes 54 → 37. Requirements with zero remaining unbound terms: 0 → 14, AUTH-24 among them.
• Gate: extend check_wiring.py to parse console/lib/proposal.ts’s OPS and assert 17 there too — today it reads only the Rust file despite that file’s own comment at proposal.ts:28-31 claiming otherwise, and the console is the live write door.
• Length: one week.

Phase 2 — derived stall: make binding a term visible on the requirement. Weeks 2–3.

One rule, one definition, two runners — the pattern RFC-003 §3 established for the vacuous refusal and the overlay:

• conformance/stall_cases.json — the fixture, in a language neither runner is written in.
• tools/readmodel/emit_readmodel.py computes blocked_on from the graph (bound terms, retracted terms, retirement, evaluation presence) instead of reading au:stalledOn verbatim.
• console/lib/overlay.ts recomputes it against the pending overlay, so a binding made 30 seconds ago moves the requirement without a redeploy.

The rule does not promote anything to R3. A bound term is not a measurement. When a requirement’s last term is bound, blocked_on becomes "unmeasured: N term(s) bound, no evaluation recorded". au:rung is untouched, so ladder-integrity.rq’s UNNAMED-STALL branch stays satisfied — every claim at R0–R3 still carries an au:stalledOn.

This is the whole point of the phase: it converts “107 unbound terms” into “14 requirements ready to measure and nothing to measure them with”, which is a specific, actionable, embarrassing number that creates the demand signal for Phase 3.

• Number: requirements whose blocked_on string changed: 0 → 14. AUTH-24 goes from "unbound-terms: 2 term(s) named and none confirmed — sponsor:edit, deploy:*" to "unmeasured: 2 term(s) bound, no evaluation recorded".
• Gate: a new zero-row authoring gate, rdf/lint/authoring/stall-drift.rq, firing on any claim whose recorded au:stalledOn differs from the derived one. Two answers with nothing asserting their agreement is DRIFT — the failure this repo exists to prevent — and the gate is what stops us introducing it.
• Length: two weeks.

Phase 3 — Studio’s Probe, and the first population. Weeks 3–6, in parallel with 2.

Ship Studio a runnable reference implementation, not a .proto and a request: the two route handlers stubbed against fixtures, the audience-scoped OIDC verifier, and a conformance suite they can run. Then Studio implements Probe against its permission and role tables. console/app/api/ground/[...path]/route.ts gains the outbound x-vercel-oidc-token header and keeps its 15s timeout and its 503/502 bodies verbatim — the refusal to manufacture {population: {count: 0}} at route.ts:20-38 is the fifth independent refusal of a vacuous zero and stays byte-identical.

• Numbers, in order: GET /api/health reports grounding_adapter: "configured" where it says "unset" today; the grounding page renders three candidate readings with counts instead of “No grounding adapter is answering”; SELECT count(*) FROM spec.evaluation_log goes 0 → 1; AUTH-24 reads “1,412 records, undecided” on the requirements page.
• Gate: an eve-free integration test asserting that a probe returning count: 0 produces outcome: Vacuous and never Examined, and that a 502 from the adapter produces CannotBeGrounded with population: null.
• Length: three weeks of Studio’s time, and it is the only item on the critical path this repo cannot unblock. If no count has arrived six weeks after the reference implementation is handed over, stop and call the bet.

Phase 4 — the promotion loop and the gate plane. Weeks 6–8.

Two independent tracks, both prerequisites for volume.

Promotion. promote.yml — landed (#49): modeled on migrate.yml, workflow_dispatch and a daily schedule, corpus-production Environment with a required reviewer, SELECT-only credential, a pinned export (WHERE seq <= $THROUGH, both pins taken once), materialize.py and emit_readmodel.py via tools/proposals/promote.sh, the gates over the result, then logs/*.jsonl and corpus/*/proposals.ttl and the read model in one commit (or //corpus/studio:proposals_ttl_matches_the_log goes red), opened as a PR. A human merges. Alongside it, materialize.py becomes total over the vocabulary — the else: continue at :139-156 becomes a hard failure naming the unhandled kind — and stops erasing attribution: it must emit one au:Proposal node per log record rather than the single shared st:authoring node at :174-180, carry surface from the record instead of hard-coding au:surface au:Meridian at :177, and emit au:authoredBy st:principal-<sub>, declared at rdf/ontology/authoring.ttl:359-364 and used nowhere. Budget a full day for the one-node-per-record change: it alters proposals.ttl’s shape and what ladder-integrity.rq resolves as au:promotedBy.

The gate plane. Rewrite rdf/lint/authoring/envelope-unrecorded.rq:25-26,34 out of the BIND(IF(?kind = au:LowerBound, ?v, ?unbound)) + HAVING(MAX(?lo) > MIN(?hi)) form that empty-envelope.rq:11-32 documents as returning zero rows under ARQ — the gate authoring_gates.bzl:21-26 calls “the load-bearing gate” is written in the exact form known to detect nothing. Wire the positive control fixtures/BUILD.bazel:71-77 says was deliberately skipped. Add //java:gate_cli, the first java_binary over the thirteen entry-point-less java_library targets, so the fixtures can be run adversarially. And add GateStatus.EXAMINED_NOTHING to the Bazel gate output with an examined count — envelope_unrecorded’s candidate set is ?quantity a au:Quantity (envelope-unrecorded.rq:16) and Studio’s corpus has zero such nodes, so the load-bearing gate is green having examined nothing, right now, today.

One caution the plan carries openly: an independently-authored <gate>.population.rq can overcount, turning a gate that examines nothing into a green gate wearing the number 69 — strictly worse than today’s silence. So examined is derived from the gate’s own WHERE clause with the HAVING stripped, mechanically, not hand-written beside it.

• Numbers: wc -l logs/*.jsonl non-zero in git for the first time. Gates reporting EXAMINED_NOTHING for Studio: named and counted rather than reported as passes.
• Gate: //conformance:conformance_test — which reads ci.yml as a source and asserts every gate-holding package is named in its explicit lists (BUILD.bazel:9-19) — must be updated for any new package, or CI fails.
• Length: two weeks, two people in parallel.

Phase 5 — grounding-interviewer. Weeks 8–11.

The eve agent of §3.1, scoped to the 37 residual surfaces, with its eval suite in CI as eve eval --strict --junit .eve/junit.xml. eve is pinned; every eve-facing call goes through console/lib/agentwrite.ts so a breaking minor — 0.32.0 alone renamed the approval response wire value from deny to cancel — reaches ten small tool files and never checkProposal or appendEvaluation.

• Number: open holes falling from 37 toward 0 — and, critically, the A/B: run the deterministic matcher over the same 37 surfaces and diff. If the agent does not beat exact matching plus a ranked dropdown, it does not touch those surfaces again. Nobody has proposed measuring an agent against the null hypothesis; this plan does, and it is the one experiment that justifies the token bill.
• Gate: the four evals above, as deterministic CI gates. t.parked() and t.notCalledTool are how “the agent stopped for a human” and “the agent refused after a zero-population probe” become facts rather than prompt hopes.
• Length: three weeks.

Phase 6 — drift-watch, and the Fargate service if its trigger fires. Conditional.

Neither is scheduled. drift-watch unblocks when Studio’s adapter has a statement timeout, a read replica, and a probe budget. The Fargate service unblocks on §4.3’s trigger condition. Both are fully specified so that saying “yes” later costs a sprint, not a design.

---

6. The invariant ledger

#	invariant	what threatens it in this plan	what enforces it	where that lives
①	spec never holds project data	eve checkpoints every tool result into durable Workflow storage for the session’s life; OTel recordInputs/recordOutputs default TRUE	probe_term strips examples inside execute(); its outputSchema has no field that could hold one; the browser fetches examples from the proxy for rendering; instrumentation.ts sets both record flags false	console/agent/grounding-interviewer/tools/probe_term.ts, .../instrumentation.ts, console/app/api/ground/[...path]/route.ts; the type boundary at proto/spec/v1/grounding_adapter.proto:18-27, asserted by //proto/spec/v1:data_boundary_test
①	(residual)	a human copy-pastes an example row back into the chat	nothing. Stated, not enforced.	—
②	a proposal is not the corpus	a live derived blocked_on could be computed from log presence rather than difference	Pending.applyTerms compares against the corpus value before marking pending (overlay.ts); the Phase 2 stall rule takes the overlay-applied rows as input and never reads the log directly; no third overlay implementation is created	console/lib/overlay.ts, conformance/overlay_cases.json, conformance/stall_cases.json
③	zero is an exception, never a pass	agent volume; a model-typed population	six independent refusals: the door (console/lib/evaluation.ts:138-153, services/spec/src/evaluation.rs:102-117); promotion (materialize.py:115-117); the SPARQL gate (vacuous-invariant.rq:13-38, gaining au:Examined in Phase 1); the table CHECK (0001_schema.sql:143-145); the proxy’s refusal to manufacture a zero (ground/route.ts:20-38); and the approval policy denying a bindTerm with no probe	as cited
③	(provenance, not magnitude)	all six refusals above test population > 0; none tests where the number came from	the number is never a tool input: propose_binding’s inputSchema has no population field, and the tool re-reads it from session state; record_evaluation is a form, not a tool	console/agent/grounding-interviewer/tools/propose_binding.ts; the eval never-types-a-number.eval.ts
③	(in the gate plane)	a correct gate over an empty candidate set still returns zero rows and reads as PASS	EXAMINED_NOTHING as a distinct status with an examined count derived from the gate’s own WHERE clause; the wired adversarial control	Phase 4: rdf/authoring_gates.bzl, rdf/lint/authoring/fixtures/BUILD.bazel, //java:gate_cli
④	Examined ≠ Passes	the adapter’s Outcome enum can carry OUTCOME_PASSES; a model will summarize “Examined 1,412” as “passing”	the outcome is chosen by the approving human from a form narrowed to Examined | Vacuous | CannotBeGrounded; a wire PASSES/FAILS is a logged protocol violation and is refused, never recorded; the display layer gates Enforced on Passes|Fails independently	the Phase 1 evaluation form; console/lib/evaluation.ts:54,61; console/lib/evaluated.ts:94,103
⑤	nothing is attributed to nobody	an agent has no credential and cannot get one honestly	the author is always the approving human’s google:<sub> from ctx.session.auth.current, never the model; the agent principal is never constructed, so proposal.ts:141-146 stays enforced rather than dead; drafted_by is a new NOT-NULL-when-Agent column with a CHECK; au:authoredBy reaches the corpus in Phase 4	console/agent/*/channels/eve.ts; migration 0004; materialize.py
⑤	(in the corpus)	nothing in the current gate suite would fail if agent- and human-authored claims were indistinguishable — ladder-integrity.rq:17 checks only that au:promotedBy exists	a new zero-row gate agent-unattested.rq: any au:Proposal with au:surface au:Agent and no au:authoredBy resolving to an au:Principal	Phase 4, rdf/lint/authoring/
⑤	(in the evaluation log)	spec.evaluation_log has no surface column (0001_schema.sql:98-146) and stores the email, not the sub	drafted_by added to both logs, with the decomposition_matches_the_line CHECK extended to cover it	migration 0004
⑥	the corpus is generated	agent-scale volume against a five-command manual promotion; retried eve steps double-appending to a log with no DELETE	promote.yml writes both halves in one commit or //corpus/studio:proposals_ttl_matches_the_log goes red; every agent write carries an idempotency key sha256(session_id ‖ canonical) behind a partial unique index — meta.id explicitly does not cover retried steps	Phase 4; migration 0004
⑥	(residual)	the idempotency key would also collapse a legitimate identical re-approval in the same session; the schema deliberately has no unique constraint on line because “binding a term to the same reading twice is a fact, not a duplicate”	partially enforced. The key is scoped per session and the collapse is accepted as the lesser error. Named, not solved.	—

Three rows in that table say nothing or partially. Those are the honest residuals; everything else names a file.

---

7. What this plan refuses to do

No agent authors a proposal alone, and no agent principal is ever constructed. console/lib/proposal.ts:141-146 rejects every agent op that is not assertNS at R0, before the capability table. A design that mints author = 'agent:eve.<name>' and then submits bindTerm gets E_OP_REJECTED 422 with nothing appended (proposal/op/route.ts:45-54). Rather than amend that rule to make an agent plan work, this plan leaves it enforced and routes around it by never needing an agent principal.

No mutable staging table. A spec.review_queue with the append-only triggers deliberately omitted inverts the audit trail — the record of what an agent drafted and a human rejected would be deletable while the record of what got through is permanent — and requires granting UPDATE/DELETE inside the spec schema to spec_app, the role 0003_grants.sql exists to hold to INSERT+SELECT. It is also invisible: console/app/api/overlay/route.ts:39-40 reads proposalRecords() and evaluationRecords() and nothing else, so a staged draft changes no number on any page. The approval request carries the full op body instead.

No toModelOutput as a data-boundary control. It projects what the model sees; the durable workflow checkpoints the real return value. Redaction happens in execute() or it does not happen.

No population, outcome, or fingerprint as a model-typed tool input. Every existing refusal tests magnitude, never provenance, and checkEvaluation is pure by design — “no database, no clock, no environment” (evaluation.ts:85-90) — so it structurally cannot verify a count even in principle.

No SESSION_SECRET shared with any service. No mTLS client certificate in Vercel env. No raw default-audience x-vercel-oidc-token forwarded to a customer-operated service.

No grpc.health.v1.Health gated on a gate self-test. A data defect that fails identically on every replacement task is an outage with no rollback signal.

No gRPC on the internet-facing hop. It costs the free keyless auth path and buys nothing the console needs; @grpc/grpc-js from a Vercel Function is also unproven — the string grpc has zero hits across the entire vercel/eve tree.

No AWS in Phases 0–5. The trigger condition is written down; the service is specified; it waits.

No retirement of emit_readmodel.py in favour of a live service. That would remove the CI check at ci.yml:231-237 which proves the eight payloads parse and agree on one corpus_version, and trade a verified batch artifact for an unverified live one in a repo whose purpose is preventing drift. (The rdflib/ARQ divergence is real and worth fixing — emit_readmodel.py:23-29 denies in writing a divergence visible in the committed envelopes.json — but it is fixed by retiring the rdflib query, not by adding a third engine.)

No claim that any Studio requirement will read “Enforced.” It cannot, by construction, and saying so after funding rather than before is the kind of quiet overclaim this whole repo exists to refuse.

---

8. Open questions, each with a default so nothing blocks

1. Will Studio staff a Probe endpoint, and by when? Default: hand over the reference implementation and fixtures in Phase 1 and set a six-week clock from that date. If no count has arrived, stop after Phase 2 and report that the pipeline is complete and unfed. This is the only question that can invalidate the plan.

2. Who reviews the Phase 1 binding batch? 17 exact-match bindings need one named person’s judgement, once. Default: mmarshall@savvifi.com, since SPEC_KERNEL_SUBS is already his problem.

3. Approval throughput. Phase 5 will generate roughly 37 approvals. At three minutes of genuine judgement each that is ~2 hours of senior attention, and if the reviewer spends less, human approval is not a safety property — it is a click. This cost appears in no budget anywhere and it decides whether the agent is safe. Default: batch by surface, not by row (one decision covers sponsor:edit across all 11 claims it blocks), cap the agent at 5 surfaces per session, and measure approval dwell time as a CI-adjacent metric. If median dwell falls under 30 seconds, turn the agent off.

4. Which Vercel plan is the team on? Secure Compute / VPC peering is Enterprise-only; Static IPs are $100/mo/project. Default: assume Pro. The plan is designed to need neither — audience-scoped OIDC to Studio, SigV4 to a Lambda Function URL, no private connectivity.

5. eve model and token budget. vercel.com/docs/eve/pricing was unreachable from every research session and is not vendored in the OSS repo, so the dominant line item in the eve budget is a guess. The only cost controls expressible in code are limits.maxInputTokensPerSession (default 40,000,000) and limits.sessionTimeoutMs. Default: set both explicitly before the first session — 2,000,000 input tokens and 7 days — and read the pricing page from an unblocked network before Phase 5 starts.

6. Does the Fargate trigger condition ever fire? Studio has zero au:Quantity nodes and zero conflicts, and its actual conflict class (25 of 69 predicates use implication/lattice language; 0 byte-equal predicate pairs) has no detector at all. Default: no. Revisit when a second customer corpus with numeric thresholds lands, or when someone writes an IMPLICATION_LATTICE detector — which is a .rq file and a Bazel target, not a service.

7. Kill switch. Nothing in the console today can stop an agent without a redeploy, and spec_app is shared between the agent and the console. Default: SPEC_AGENT_ENABLED read per request in console/lib/agentwrite.ts, defaulting to false, plus a documented POST /eve/v1/session/:id/cancel sweep. Ship it in Phase 5 before the first agent write, not after.

8. Who is paged? For the adapter, for a wedged eve session, and (later) for a Fargate task. Default: the adapter is Studio’s; a wedged session is whoever merged Phase 5; there is no Fargate task to page for, which is one more argument for §4.3’s trigger condition.

from docs/rfc-004a-the-cheapest-population.md

RFC-004a — the cheapest path to a real population

Status: proposed; §4 (the machine credential) and §5 (the job) landed in #48. A narrowing of RFC-004 §5 Phase 3, written because the adapter is the only item on the critical path this repo cannot unblock, and the question “how much of our model do we have to adopt to use this?” deserves a smaller answer than “implement a gRPC service”.

---

1. The short answer

Almost none of it, and you can skip the adapter entirely for the first numbers.

POST /api/evaluation is deployed, authenticated and correct — it has been since #29 — and it has never had a caller. A CI job in the project that runs one SELECT count(*) and posts the result gets a requirement a real population with no proto, no service, no ontology and no spec vocabulary. That is the whole integration:

studio-nextjs CI  ──POST /api/evaluation──▶  console  ──▶  spec.evaluation_log
   one SQL count                                            (append-only)

AUTH-24 stops reading — / NOT-EVALUATED and starts reading “1,412 records, undecided”, which is the sentence this repo was built to make possible.

2. What actually crosses the boundary

The two RPCs in proto/spec/v1/grounding_adapter.proto cost very differently, and conflating them is what makes the adapter look expensive.

	what it asks of the project	how much of spec’s model it carries
Probe	”given these strings you wrote, how many records does each match?“	none — invariant_id and term_id are opaque and echoed back, and the proto says outright: “The project decides what a locator means; spec never parses one”
Evaluate	”resolve this Grounding, run this Check, and decide the predicate”	a lot — both types come from invariant.proto

So the shoehorning risk is real and it lives entirely in Evaluate. RFC-004 §4.2 already declines it: 25 of Studio’s 69 predicates use implication or lattice language and none carries a numeric threshold, so Evaluate for AUTH-24 is a decision procedure over Studio’s authorization lattice — a research project, not an endpoint.

Ship Probe, never ship Evaluate. Everything then lands on Examined: measured, undecided. That is the honest state, it is what OUTCOME_EXAMINED exists for, and its price is stated in RFC-004 §4.2 — no Studio requirement can ever read “Enforced”. A column of real numbers beats a column of em dashes.

And the direction of travel is worth naming: a locator is written by your engineer in your vocabulary during binding. The model that crosses the wire is yours, moving outward. Nothing of spec’s moves in.

3. The evaluation POST, exactly

Verified against console/lib/evaluation.ts and console/app/api/evaluation/route.ts.

POST /api/evaluation
{
  "claim":             "auth-24",         // REQUIRED — an evaluation of nothing is not a measurement
  "implementation":    "studio-nextjs",   // REQUIRED — the same claim can pass in one product and be
                                          //            ungroundable in another; an unattributed count
                                          //            cannot tell you which
  "outcome":           "Examined",        // Passes | Fails | Examined | Vacuous | CannotBeGrounded
  "population":        1412,              // integer; REQUIRED for Passes/Fails/Examined
  "project":           "studio",          // optional
  "query_fingerprint": "sha256:9f2c1a…",  // optional, and the thing that makes a count reproducible
  "detail":            ""                 // optional, failure case only — not evidence
}
→ 202 { "recorded": true, "log_seq": 1, … }

Three refusals you will meet, and each is deliberate:

• Examined with population: 0 → 422. Zero is an exception, never a result. Report Vacuous, which is what it is. This is the entire point of the system and it is enforced in six independent places.
• A positive outcome with no population → 422. A result nobody can audit.
• No principal → 401. See §4.

Report Examined, not Passes. A count is a measurement; a pass is a judgement. The adapter measures a population and refuses to decide the predicate, and a CI job posting Passes would be making a claim its SELECT count(*) did not check.

4. The machine credential

POST /api/evaluation authenticates with the console’s session cookie — principal() resolves a signed-in human, or SPEC_AUTHOR in local development — or with a machine credential, which is the thing this section used to say did not exist. It is deliberately NOT a general-purpose API key:

• Accepted only by POST /api/evaluation. /api/proposal/op never consults it — that route calls principal(), which can only ever produce a google: or dev: sub — so a machine cannot reach the op door by construction, and checkOp refuses the machine: prefix as a second lock. A machine may report what it measured and may not author, amend or withdraw a requirement: the same boundary proposal.ts draws for agents, one door over.
• A named principal. The token’s sub is machine:<implementation>, and that string is the author on the row. Invariant ⑤ is that nothing is attributed to nobody, and “a machine did it” is nobody.
• Held in the project’s CI secrets, rotatable, and useless for anything except appending counts. An HS256 JWT signed with SPEC_MACHINE_TOKEN_SECRET — a secret of its own, required to differ from SESSION_SECRET — carrying aud spec-console:evaluation, typ spec-machine+jwt, a required exp (90 days by default, a year at most) and a jti, so one leaked token can be revoked by name (SPEC_MACHINE_TOKEN_REVOKED) without rotating the secret out from under every consumer. Rotating the secret kills every token at once; re-mint and redistribute.

Two rules ride on it, both enforced before anything is appended:

• A machine reports, never judges. Passes and Fails from a machine: author are refused (422). A count says how many records a check would examine; whether the claim holds over them is a judgment, and a SELECT count(*) did not make one. The rule lives in the shared conformance cases (conformance/evaluation_cases.json), so the Rust door says the same.
• A credential reports for the implementation it names, and no other. A token issued for studio-nextjs posting against implementation: "ampere" is a 403, not a rewrite.

And a presented credential is judged, never ignored: an Authorization header that does not verify is a 401 here and now, never a fall-back to a cookie or SPEC_AUTHOR. The refusals, by code: E_MACHINE_TOKEN_REJECTED (not this console’s, expired, or revoked), E_MACHINE_TOKENS_UNCONFIGURED (the deployment has no machine secret), E_IMPLEMENTATION_MISMATCH.

Minting is an operator’s laptop, not a route — console/tools/mint-machine-token.mjs, walked through in console/DEPLOY.md → “Machine credentials”. The verifier is console/lib/auth/machine.ts; the tests that matter are console/test/routes.test.ts, written as the attack.

5. The job

tools/evaluation/post_evaluation.mjs is the job: one dependency-free file a project copies into its CI. It runs wherever the project’s database is reachable — which is the point: spec never sees the database, only the number.

## Your SQL, your pool, your credentials. Only the count leaves.
POP=$(psql "$DATABASE_URL" -X -A -t -c "$(cat checks/auth-24.sql)")

SPEC_CONSOLE_URL=https://spec.example.com SPEC_EVALUATION_TOKEN=… \
node post_evaluation.mjs --claim auth-24 --implementation studio-nextjs \
    --project studio --population "$POP" --sql-file checks/auth-24.sql

What it sends is §3’s body: the claim, the implementation, the count, and sha256: + the first 16 hex of the SHA-256 of the query text — so the count can be reproduced later without storing what was counted. The outcome is a function of the count, Vacuous at zero and Examined otherwise; the script has no way to say Passes. --dry-run prints the body without reading the token. tools/evaluation/README.md has the GitHub Actions and GitLab CI shapes and the refusals the job will meet.

Note what is absent: no .proto, no generated client, no ontology import, no term ids, no rungs. A list of (claim, SQL) pairs and one POST.

6. What this does not get you

• No candidate readings. The “three fields could mean a sponsor they brought, and they disagree by 47 sponsors” conversation needs Probe, because it needs counts for readings nobody has committed to yet. This job only counts a reading already chosen.
• No examples. DisplayExample is transit-only and exists for that same conversation. Nothing here renders a row.
• Nothing reads “Enforced”. By construction, as in §2.
• Drift is not watched. A count posted once is a count from that day. Running the job on a schedule is what turns it into a tripwire, and RFC-004 §3.2’s drift-watch is the same idea with a model attached.

7. Where this leaves RFC-004

Phase 3 splits in two, and only the first half is on the critical path:

3a	the CI job in §5, plus the machine credential in §4	shipped on the console side (#48). What remains is the consumer’s CI running it — days, and not this repo’s days
3b	Probe, for the grounding conversation	weeks, and worth it once terms are being bound at volume

The six-week clock RFC-004 §8 puts on Phase 3 should be started against 3a — from the day the first credential is handed over. If a count has not arrived in that window, the blocker was never the protocol.

from docs/rfc-005-one-engine-of-record.md

RFC-005 — one engine of record, before the gates answer anybody live

Status: proposed. Prerequisite for RFC-004 §4.3. Written because the estate runs three SPARQL engines over two disjoint gate suites on two Jena versions, one file asserts in prose that it runs one, and none of that is survivable once a gate verdict is something an agent can ask for.

---

1. What is actually true today

path	engine	Jena	what it runs
kg.GateHarness / kg.edit.WriteOps	in-process ARQ, QueryExecutionFactory.create	5.0.0 (@spec_maven, MODULE.bazel:62)	7 gates — contradictions, four resource-bundled framework gates, query_smoke, SHACL
sparql_query_test / rdf_validate_test	ARQ as a subprocess — //jena/sparql:jena_sparql, stdin → TSV, --fail-on-nonempty, exit code	5.2.0 (@jena_maven, in rules_jena)	47 + 8 = 55 targets over rdf/queries/consistency/ and rdf/lint/authoring/
tools/readmodel/emit_readmodel.py	rdflib	—	the 8 read-model routes the console renders

Counted, not estimated: spec_corpus_gates is instantiated 8 times × (4 sparql_query_test + 1 rdf_validate_test); spec_authoring_gates 3 times × 4 gates; plus 3 hand-written sparql_query_test. 32 + 12 + 3 = 47, and 8 SHACL.

And tools/readmodel/emit_readmodel.py:26-27 says:

There is exactly ONE SPARQL implementation of record. No drift risk between a Rust query path and the Jena gates.

Four lines above from rdflib import Graph. The sentence is true about the Rust path, which does not exist. It is false about the estate, and it is the reason nobody has been looking.

2. Why this is load-bearing now and was not before

While the gates only ever ran in CI, divergence cost a confusing afternoon. The moment a gate verdict is an RPC an agent can call, divergence becomes a model reporting a requirement as formally validated on the strength of a suite that is not the one which gates the merge.

WriteOps.applyAndCheck — the one function that already computes a proposed-graph verdict, and the natural body of Gates.Preflight — preflights against GateHarness’s seven. Those seven are not a subset of the 55. So “preflight: PASSED” does not entail “CI will pass”, and nothing anywhere says so.

This is not hypothetical. rdf/lint/authoring/envelope-unrecorded.rq carries, in its own body:

⛔ THIS GATE RETURNED ZERO ROWS FOR EVERY INPUT, AND READ AS PASSING.

because of how ARQ specifically evaluates HAVING(MAX(?lo) > MIN(?hi)) over BIND(IF(...)). That is an engine-semantics divergence inside one engine family. emit_readmodel.py re-implements similar aggregations under rdflib and nothing compares the two.

3. The decision

The Bazel sparql_query_test path is the engine of record. It is the one that gates the merge, the one that caught the defect above, and the one whose verdict is already a hard pass/fail rather than a rendered number.

Three consequences, in the order they bind:

① Anything that answers “what do the gates say” RUNS the engine of record, rather than reimplementing it. //java:gate_cli executes @rules_jena//jena/sparql:jena_sparql — the same binary sparql_query_test invokes, with the same flags — and reads its exit code and rows. It is not asserted to agree with the gate targets; on the verdict it IS them.

This is strictly better than the conformance-fixture pattern used elsewhere in this repo. A fixture proves two implementations agree on the cases someone thought of. Running the same binary removes the question.

⚠ The in-process version is not available at the pinned version, and finding that out cost a build. rules_jena’s main has a result_emit java_library whose comment states the purpose — “Keeping the formatter calls in one library guarantees the two paths emit byte-identical results” — but 0.3.0, which is what MODULE.bazel resolves, ships only JenaSparql.java with the execution inline. A sibling working copy at fastverk/fastverk/repos/rules_jena is ahead of the release; reading it and assuming it matched is the mistake. Until rules_jena is bumped, every gate costs a subprocess — fine for CI, and the thing to fix before an agent hits this in a loop.

② A gate runner links the engine’s Jena, never spec’s. @spec_maven is on Jena 5.0.0 and rules_jena on 5.2.0. A java_binary depending on both puts two Jena versions on one classpath, and which one answers is a function of classpath order. gate_cli uses in-process Jena only to merge the corpus and derive the examined count — never to decide a gate — and must not depend on //java:loader or anything else carrying @spec_maven’s Jena.

⚠ The obvious spelling, load("@rules_jena//jena:defs.bzl", "JENA_DEPS"), does not work: those labels live in rules_jena’s own @jena_maven, which Bzlmod does not make visible outside the module that declared it (use_repo is module-scoped). The build fails with “No repository visible as @jena_maven”. So the version is restated in a second install, @spec_gate_maven, pinned to 5.2.0 in spec_gate_maven_install.json. That restatement is a drift risk with no gate on it — if rules_jena bumps Jena, nothing here notices. Naming it is the only mitigation this RFC offers.

⚠ Pinning that install needs an ambient JDK, because Coursier runs as a repository rule outside Bazel’s Java toolchain. That is issue #19 exactly, and why every install here is pinned. bazel run --repo_env=JAVA_HOME=<jdk> @unpinned_spec_gate_maven//:pin.

The real cost: gate_cli cannot reuse Loader.loadDataset and loads its own. The alternative — moving all 14 java_library targets to 5.2.0 — is the better end state and is deliberately not attempted here, because it touches maven_install.json and every consumer of those libraries in Aion.

③ The rdflib path is retired, not reconciled. RFC-004 §7 already says the fix is “retiring the rdflib query, not adding a third engine.” Nothing in this RFC changes emit_readmodel.py; it removes its claim to be the only implementation and puts it behind a dated note. It is the read model, not a gate, and it is not on the path an agent asks about.

⚠ What happened when the read model was finally run under the engine of record

The last sentence above was the reasonable call and it was load-bearing in the wrong direction. “It is the read model, not a gate” is true and it is exactly why nobody looked — and spec#52 made it matter anyway, because a CONSUMER’s console is built from these payloads, so “not a gate” became “not checked, and shown to people”.

rdf/readmodel/ now holds the same eight questions as .rq files, and spec_readmodel runs them under ARQ. The first time they were put to the engine of record, one answered differently:

route	rdflib	ARQ
envelopes over corpus/ampere	2 rows	0 rows

The read-model copy was written in the flat form this repository has already documented twice as broken — empty-envelope.rq’s header explains it at length, and envelope-unrecorded.rq’s opens with ”⛔ THIS GATE RETURNED ZERO ROWS FOR EVERY INPUT, AND READ AS PASSING”:

BIND(IF(?kind = au:LowerBound, ?v, ?unbound) AS ?lo)
...
HAVING (MAX(?lo) > MIN(?hi))

The third instance of a defect found twice, surviving in the one place that ran a different engine. Both gates were fixed; the read model was not, because rdflib evaluates the unbound sentinel as “leave it unbound” and the query works there. It is now the gate’s own three-subselect form, so the console panel and the gate measure are the same question asked the same way rather than two formulations that happened to agree under one engine.

//tools/readmodel:engine_agreement_test compares both engines row for row over spec’s two corpora — same .rq files, same shapers, so a difference is the engine and nothing else. They now agree on every comparable pair. Two more disagreements surfaced getting there and neither was an engine’s fault: ARQ writes booleans BARE in TSV (false, not "false"^^xsd:boolean), so a decoder that drops to str yields bool("false") == True; and GROUP_CONCAT’s order is unspecified in SPARQL 1.1, so the payload now sorts it rather than inheriting whichever engine ran.

⚠ The rdflib path still exists and still emits what is committed under services/spec/readmodel/. What changed is that it is no longer the only implementation and no longer unchecked. Switching spec’s own payloads to the ARQ path is the next step and is deliberately not taken in the same change as the finding.

4. EXAMINED_NOTHING, and why the count is derived rather than written

A zero-row gate over an empty candidate set returns zero rows and reads as PASS. envelope_unrecorded’s candidate set is ?quantity a au:Quantity; Studio’s corpus has zero such nodes. That gate is green today having examined nothing.

A human skims past that. A model reports it as validation. So GateStatus is three-valued — PASSED | FAILED | EXAMINED_NOTHING — with an examined count beside it.

RFC-004 §5 proposes an independently authored <gate>.population.rq and then names its own defect: it can overcount, “turning a gate that examines nothing into a green gate wearing the number 69 — strictly worse than today’s silence.” That convention does not exist in the repo (0 files) and this RFC declines to create it.

Instead the count is derived from the gate’s own parsed query, mechanically, through ARQ’s AST: clear HAVING, project SELECT *, count solutions. The argument was that a transform of the parsed query cannot describe a WHERE clause the gate does not have, while a hand-written sibling can.

That was implemented, run against Studio’s corpus, and is wrong for most gates here. It is recorded rather than quietly deleted, because the failure is the useful part.

Stripping HAVING separates candidates from judgement only when the judgement is in the HAVING. Most gates in rdf/lint/authoring/ are not written that way. ladder-integrity.rq is a UNION of blocks shaped like:

?claim a rfc:NormativeStatement ; au:rung ?rung .
FILTER(?rung IN (au:R0, au:R1, au:R2, au:R3))
FILTER NOT EXISTS { ?claim au:stalledOn ?s }

The judgement is the FILTER NOT EXISTS, and it is INSIDE the WHERE. The pattern matches violations and nothing else, so on a healthy corpus it matches nothing. The derived count came back 0 for a gate that had just read 133 claims, and all four authoring gates reported EXAMINED_NOTHING over a corpus CI calls green. A blind-gate detector that fires on every healthy gate is worse than no detector: it teaches the reader to ignore it.

So the derivation is claimed only where it is sound, which is mechanically decidable — Query.getHavingExprs().isEmpty(). No HAVING, no separable candidate set, and examined is -1, meaning UNKNOWN. -1 never reads as EXAMINED_NOTHING: a gate whose blindness cannot be determined reports PASSED with the count withheld, which is the honest state.

This vindicates RFC-004 §5’s <gate>.population.rq more than it refutes it. An authored candidate set is not avoidable, only relocatable — and RFC-004’s own objection, that an independently authored population can overcount so a gate examining nothing wears a flattering number, is real and unchanged.

The recommendation is therefore the middle position neither RFC took: declare the candidate pattern in the gate’s own frontmatter, in the same file, reviewed in the same diff — not in a sibling file that can drift, and not in a transform that cannot see the judgement. That is an open decision, not a conclusion.

⚠ Residual even where sound: for a grouped gate this counts solutions, not groups, so examined reads “candidate rows the gate looked at”, not “things it judged”. It is not a denominator and nothing should divide by it.

5. What this does not decide

• It does not merge the two gate suites. GateHarness’s seven include SHACL and a query-smoke walk that the Bazel suite expresses as separate rules; the overlap is partial and reconciling it is its own piece of work. This RFC says only which one answers when they disagree, and forbids the new surface from adding a third opinion.
• It does not retire GateHarness. It is reachable from Aion, which is outside this repo’s control.
• It does not move spec to Jena 5.2.0. Named in ②, deliberately deferred.

6. The check that keeps this true

//java:gate_cli is exercised by CI over the same corpus as the sparql_query_test targets, and a test asserts that for every gate in the authoring suite, gate_cli’s verdict matches the corresponding Bazel target’s. The assertion is cheap precisely because ① makes it near-tautological — and it is worth having anyway, because the day it fails is the day someone has reintroduced a second implementation without noticing.

from docs/rfc-006-the-gate-plane-deployed.md

RFC-006 — the gate plane, deployed

Status: proposed. Follows RFC-005 (which engine answers) and RFC-004 §4.3 (what the service should offer). This one is about where it runs and what it costs, and it is much cheaper than RFC-004 assumed because most of it already exists.

---

1. What is already running

Verified against the fastverk EKS cluster in account 491117466965, not inferred:

plugin-spec	running 1/1, image 491117466965.dkr.ecr.us-east-1.amazonaws.com/spec:ee840289f3b2, ports http/8080 + grpc/50056, ClusterIP
the fleet	16 plugins, every one http/8080 + a named grpc port. gRPC is already the east-west idiom here
/mcp	already served — services/spec/src/http.rs:96-98 mounts crate::mcp::router(...)
images	pushed per commit; newest ef7ddbb9d1d9 (2026-08-11). The pod is simply behind
the front door	ALB group fastverk-public, internet-facing, HTTPS:443, target-type: ip

RFC-004 §4.3 budgets ≈$38/mo for a new Fargate task and says “AWS gets nothing in Phases 0–5.” AWS already has something, it is already paid for, and the marginal cost of adding RPCs to a pod that exists is zero. That section should be read as superseded on cost, not on design.

Two corrections, both recorded because I got them wrong in sequence.

ci.yml:75-90 reads like a live 401 against the private fastverk-plugin-crates repo, and MODULE.bazel says the OCI image “could not be built by CI and had to be produced by hand.” Both describe problems that were fixed — the block documents the App-token mint, and ECR shows a fresh image per commit.

⛔ But that does not mean a NEW image is cheap, and I then over-generalized it into “the image path is not a risk.” It is not: nothing in this repository builds or pushes an image at all. ci.yml has exactly two jobs, gate and console, and neither touches ECR — a grep suggesting otherwise was matching “s-ecr-ets”. The spec:<sha> tags are pushed by the platform build-runner, per the Dockerfile’s own note that “the platform’s canonical build is the bazel rules_fastverk_plugin macro / //services/spec:spec-image; this Dockerfile is the pragmatic cross-arch path until the build-runner bakes the bazel image on a linux worker.”

So §3’s sidecar needs a JVM image, and producing one is work in fastverk/build, not here. The three options, none free: teach the build-runner a second image; add an image build to spec’s CI, duplicating a pipeline the platform deliberately centralised; or bundle a JRE into the existing spec-server image, which is distroless today and would grow by ~180 MB for a process most deployments will never call. This is the open question gating deployment, and it is not answerable from inside this repo.

2. The front door shares an ALB, and that is the whole cost story

No new load balancer. The AWS Load Balancer Controller merges every Ingress carrying the same alb.ingress.kubernetes.io/group.name onto one ALB, and fastverk-public has room:

rules      6 / 100
certs      4 / 25
hosts      app · hooks · mcp · mirror .fastverk.com

A second ALB would be ~$16–22/mo of base charge before a byte moves, for nothing that the existing one cannot do. So:

alb.ingress.kubernetes.io/group.name: fastverk-public   # ⛔ share, do not create
alb.ingress.kubernetes.io/listen-ports: '[{"HTTPS":443}]'
alb.ingress.kubernetes.io/target-type: ip
alb.ingress.kubernetes.io/backend-protocol-version: GRPC
alb.ingress.kubernetes.io/certificate-arn: <new cert for spec.fastverk.com>

backend-protocol-version is a per-target-group setting, so a gRPC backend coexists with the four HTTP/1.1 backends already on that ALB. Sharing costs nothing in capability.

DNS. One public fastverk.com zone in this account (Z01797023FIJ030ZIGZEA, 60 records), live and delegated — app.fastverk.com resolves. spec.fastverk.com is free. external-dns is running in the fastverk namespace with --domain-filter=fastverk.com --provider=aws --aws-zone-type=public, so the record follows the Ingress with no manual step.

⚠ It runs --policy=upsert-only, which means it never deletes. Removing the Ingress later leaves spec.fastverk.com resolving at an ALB that no longer routes it — a name that answers and a service that is gone are harder to debug than a name that does not resolve. Deleting the record is a manual step, and nothing will remind anyone.

⚠ The existing ACM cert covers app.fastverk.com with a single SAN and no wildcard, so a new hostname needs its own cert. Certs are immutable; four are already attached to that listener, which is the established pattern.

⚠ A gRPC target group’s health check cannot be a plain GET /healthz — it needs healthcheck-protocol-version: GRPC with a gRPC health service, or an HTTP check with success-codes: 0-99 (gRPC status codes, not HTTP). Getting this wrong produces a target group that never goes healthy while every container is fine.

Total marginal infrastructure cost: one ACM certificate ($0) and one Route 53 record set (~$0).

3. Where the JVM runs

A second container in the pod that already exists, not a new Deployment. plugin-spec already runs exactly two containers — spec-server and git-sync (verified on the live Deployment) — so multi-container is established here and the chart has a place to put a third.

The Rust process keeps the front door and reaches the JVM on loopback. That is RFC-004 §4.3’s own instinct — “gRPC is kept between the Rust and JVM containers on loopback, where it is free, and off the internet-facing hop, where it costs the auth story” — and it survives unchanged.

What that buys over a separate Deployment: no second Service, no second ArgoCD-managed workload, no cross-pod hop, and the JVM’s lifecycle is the plugin’s. What it costs: the two scale together. At one replica that is not a trade-off yet.

⚠ Sizing is unmeasured. The corpus is 220 KB of Turtle and gate_cli runs four gates in 0.52s on a laptop, but no one has measured the JVM’s resident set under a warm Jena Model. Set a request, watch it, and do not copy RFC-004 §4.3’s “1 vCPU / 2 GB” — that number was sized for a Fargate task nobody is now building.

4. Auth: verified in the service, not at the front door

RFC-004 §4.3 rules out gRPC on the internet-facing hop because “ALB has no SigV4 authorizer” and “gRPC and Vercel-OIDC meet at no AWS front door except VPC Lattice.” That argument is about making the front door do the authenticating, and it dissolves when the service does it.

The console sends getVercelOidcToken({ audience: 'https://spec.fastverk.com' }) in gRPC metadata; the plugin verifies it against the oidc.vercel.com JWKS with aud and environment:production pinned. The ALB routes and terminates TLS and authenticates nothing. No SigV4, no mTLS, no client certificate in Vercel’s environment, no key to rotate.

⛔ Not the default-audience token. Vercel’s default OIDC aud is https://vercel.com/<team-slug> and its sub is owner:<team>:project:<project>:environment:<env> — precisely the claims an AWS trust policy pins for sts:AssumeRoleWithWebIdentity. Forwarding the raw token hands a service, on every call, a credential replayable against STS for any role in the account trusting that project. Audience-scoping is one parameter.

⚠ The fleet’s existing mechanism is a shared bearer token (builds-secrets/plugin-token, validated as require_gateway_token). It would work today with no new code, and it is weaker: one static secret, shared across every plugin, with no per-caller identity. Acceptable as a stopgap; it should not be the answer once a permanent record can be attributed to the caller.

5. What the service may answer, and what it may not

Derivation.RunGates and Derivation.Preflight, per derivation.proto. Both carry counts and never rows, and the proto imports nothing so //proto/spec/v1:data_boundary_test extends unchanged.

An MCP facade for the read plane, and only the read plane. /mcp is already mounted, so preflight and run_gates are handlers to add rather than a service to stand up — and their value is that agents which are not eve get them too.

⛔ No write tool over MCP. propose_requirement parks on an always() approval and takes its author from ctx.session.auth.current — the approving human. MCP has no approval semantics and no session principal, so a write tool there has nobody to attribute to, and “a machine did it” is nobody. That is invariant ⑤, and it is the same boundary RFC-004 §3.3 draws when it makes record_evaluation a console form rather than a tool.

6. Order, and the honest stopping point

1. ✅ //java:gate_binary — a long-lived wrapper over gate_cli’s library, holding a warm Model. Local, no AWS. Done.
2. ✅ UNBLOCKED, and done. This read “BLOCKED on §1’s second correction — the sidecar needs a JVM image and this repo cannot produce one.” It can now: //java:gate_image builds here and ci.yml’s image job pushes it to spec-gate per-sha. The tag nothing populated is populated. The chart’s sidecar is in deploy/charts/plugin-spec, disabled by default.
3. The Ingress above, sharing fastverk-public, plus the cert and record.
4. Vercel OIDC verification in the plugin.
5. The console calls Preflight before submitting a proposal.
6. The agent gets a preflight tool — last, and only with EXAMINED_NOTHING in the response, because a tool that returns “PASSED” over an unexamined population is worse than no tool.

Steps 1–2 are the ones that matter. They make preflight callable at all. 3–4 only make it callable from Vercel, and if that stalls on a certificate or a DNS delegation, everything before it still works from inside the cluster and from CI.

⭐ A step this list never had, now done: the service itself. The numbering above jumps from the sidecar to the Ingress as though Derivation were free — §5 names the two RPCs and nothing was going to serve them. services/spec now does, on the same gRPC port as the nav plane, proxying to the sidecar on loopback. The numbering is left alone so existing references still resolve; read this as 2½, and note what it means for step 3: the Ingress now has something to expose that is not LayoutService.

The service also answers what §5 left implicit — what happens when the plane is asked something it cannot honestly answer. Three refusals, each in place of a confident wrong answer: removals_turtle (the sidecar has no removal channel, so the result would be the proposal minus its deletions), a pinned parent_corpus_version (unverifiable — the sidecar reports no version), and a gate name that is not in the suite (silently dropping it makes a typo read as a gate that passed).

✅ The stale-chart warning that stood here is resolved: deploy/charts/plugin-spec/values.yaml pointed at the aion-dev ECR (042825952740) while the live pod ran from fastverk’s own (491117466965), which would have moved the image backwards on the first sync. It now names fastverk’s, with both image tags supplied by the deploying pipeline and required — an empty tag used to render spec: and fail in the cluster, which is the same class of mistake one layer further out.

from docs/running-locally.md

Running the console and the agent locally

Everything here runs without touching production. The console writes to a local JSONL file unless you deliberately point it at Neon, and the agent has no door to the log except the console you give it.

Prerequisites

	why
Node 22+	the console
Node 24+	the agent — eve’s own engines constraint, and it is enforced
pnpm 10	the console’s lockfile
AWS credentials with bedrock:InvokeModel	only for the agent, and only on the Bedrock route

The two halves need different Node versions, so run them in separate shells with whatever version manager you use.

---

1. The console

cd console
pnpm install

## ⛔ Local development only. `SPEC_AUTHOR` stands in for a signed-in Google
## account so writes have someone to be attributed to — invariant ⑤ is that
## nothing is attributed to nobody, and without this every write is refused
## rather than recorded anonymously.
export SPEC_AUTHOR='you@savvifi.com'

## The append-only log, as a file. Point this at a scratch path, NOT at
## logs/proposals.jsonl — that file is committed and gated, and the promotion
## pipeline reads it.
export SPEC_PROPOSAL_LOG=/tmp/spec-proposals.jsonl
touch "$SPEC_PROPOSAL_LOG"

pnpm dev            # http://127.0.0.1:5175

GET /api/health is the fastest check that it came up correctly:

{
  "log_backend": "jsonl",          // "neon" if DATABASE_URL is set
  "write_enabled": true,
  "principal": "present",          // "absent" ⇒ SPEC_AUTHOR is unset and writes will 401
  "grounding_adapter": "unset",
  "deployment": { "commit": "", "stage": "local" }
}

Against Neon instead — set DATABASE_URL to the spec_app credential, never the owner. spec_app holds INSERT and SELECT and nothing else; the owner can ALTER TABLE … DISABLE TRIGGER, which is the one thing the whole schema exists to prevent. Migrations are CI’s job (.github/workflows/migrate.yml), not a laptop’s.

⚠ Writes to Neon cannot be undone. The log is append-only by trigger and by grant, and the only cleanup for a test record is dropping the schema. Use the JSONL backend to try things.

As a machine — the credential a consumer’s CI would hold (RFC-004a §4):

export SPEC_MACHINE_TOKEN_SECRET=$(openssl rand -hex 32)   # set BEFORE pnpm dev; must differ from SESSION_SECRET
TOKEN=$(node tools/mint-machine-token.mjs --implementation studio-nextjs)
curl -s -X POST localhost:5175/api/evaluation \
  -H "authorization: Bearer $TOKEN" -H 'content-type: application/json' \
  -d '{"claim":"auth-24","implementation":"studio-nextjs","outcome":"Examined","population":1412}'
## 202 {"recorded":true,…,"author":"machine:studio-nextjs"}
tail -1 /tmp/spec-proposals-evaluations.jsonl

The same token against /api/proposal/op is a 401: it is accepted by the evaluation route and nowhere else. SPEC_AUTHOR is not consulted while an Authorization header is present — a presented credential is judged, never ignored. /api/health reports machine_credentials.configured so a deployment that forgot the secret reads as one.

The door — a proposal, and the name it gets:

curl -s -X POST localhost:5175/api/proposal -H 'content-type: application/json' \
  -d '{"parent":"corpus:studio@today","ops":[
        {"op":"bindTerm","term":"session","definition":"a row in auth.sessions","project":"studio"}]}'
## 202 {"verdict":"Admitted","address":"sha256:…","address_pre_image":"{\"author\":…}","log_seq":1}

⛔ Now send the identical op through the flat route with a different surface, and compare the two addresses:

curl -s -X POST localhost:5175/api/proposal/op -H 'content-type: application/json' \
  -d '{"parent":"corpus:studio@today","surface":"Chat","op":"bindTerm",
       "term":"session","definition":"a row in auth.sessions","project":"studio"}'

Same address, different canonical. That is RFC-002 §9.1: one proposal, two provenance records. The name is sha256 over {author, ops, parent} and over nothing else, so the surface and the intent are recorded and do not vote. Then:

python3 tools/proposals/replay.py --log /tmp/spec-proposals.jsonl --list
python3 tools/proposals/replay.py --log /tmp/spec-proposals.jsonl \
    --address sha256:… --project studio --out /tmp/replayed

⚠ The plugin’s POST /proposal answers 410 Gone and names these routes. Two doors are two implementations of the address, and they had already disagreed about one (the plugin coerced a form’s bound_value to a float; the console does not coerce at all).

What to look at

/requirements	the list, with each row’s grounding fraction
/requirements/auth-24	the one to look at. The motivating claim, its two words highlighted by whether they point at anything, and the walkthrough
/requirements/new	write a requirement and watch the decomposition preview as you type
/terms	the same words as entities, ordered by how many claims each unblocks
/terms/studio/sponsor:edit	one word, and the 11 claims waiting on it

A five-minute pass that exercises the whole loop:

1. Open /requirements/auth-24 — “2 of 2 terms not pinned down”, both words amber.
2. Record a reading for deploy:* — say permissions.key = 'deploy:*'.
3. It turns green in the sentence, the bar moves to 1/2, and it leaves the walkthrough.
4. /terms/studio/deploy:* now shows what it reads as, and every claim that waited on it.
5. cat $SPEC_PROPOSAL_LOG — one record, with your author, the parent read point, and canonical bytes.

Nothing there has been adopted. Pending means differs-from-the-corpus, and promotion is tools/proposals/materialize.py plus a human merging a PR.

---

2. The agent

cd agent            # Node 24 shell
npm install

On Bedrock (no Vercel account involved)

export SPEC_AGENT_BEDROCK_MODEL="us.anthropic.claude-sonnet-4-5-20250929-v1:0"
export AWS_REGION=us-east-1
export SPEC_CONSOLE_URL=http://127.0.0.1:5175      # the console from §1

npx eve build

## ⛔ NOT `eve dev` — see "eve dev cannot build this agent" below.
VERCEL=1 VERCEL_ENV=development npx eve start

⛔ SPEC_AGENT_BEDROCK_MODEL must be set for build AND for dev/start. agent.ts is evaluated once at build time to compile the manifest and again at runtime to resolve the model. Set it for only one and they disagree: MODEL_SELECTION_FAILED: Expected the authored agent config … to provide a dynamic model definition.

⛔ eve dev cannot build this agent, and eve start refuses the caller

Both halves of the documented eve build && eve dev path are broken, in different ways, and the workaround above threads between them.

eve dev copies the agent into .eve/dev-runtime/snapshots/<id>/source/agent/ and builds from there. agent/tools/preview_decomposition.ts and propose_requirement.ts import ../../../console/lib/decompose — deliberately, so the rule has one definition — and that path escapes the snapshot, which contains no console/. The build fails with two UNRESOLVED_IMPORT errors before the server starts. eve build is unaffected: it bundles from the real tree, where the import resolves.

So the agent must be run from the production build, eve start — and that rejects every request with 401 unauthorized. agent/channels/eve.ts admits vercelOidc() and localDev(), and localDev() returns a principal only when VERCEL is set and VERCEL_ENV === "development", or when eve is in dev mode. Under eve start neither holds.

Hence VERCEL=1 VERCEL_ENV=development. It is a local shim, and it must never be set in a deployment — it is the switch that makes the agent admit an unauthenticated caller. The real fix is one of: give the agent its own copy of the decomposition rule (losing the single-definition property the conformance fixture exists to protect), make console a resolvable package rather than a relative path, or add a real auth strategy to the channel.

Model access is per-model, per-account, and Anthropic wants a form

Anthropic models on Bedrock additionally require a use-case details form to be submitted for the account, in the Bedrock console. Until it is, every Claude model id returns:

ResourceNotFoundException: Model use case details have not been submitted for
this account. Fill out the Anthropic use case details form before using the
model.

That is a 404, not a 403, and it names a model that bedrock list-foundation-models will happily list — so it reads like a wrong model id rather than an entitlement problem. Both 740659854426 and 491117466965 returned it on 2026-08-12.

To tell entitlement apart from credentials, call a non-Anthropic model with the same credentials — us.amazon.nova-pro-v1:0 succeeded where every us.anthropic.* id failed. If Nova answers, the credential chain, region and signing are all correct and the problem is the form.

⚠ --profile does not reach the provider. @ai-sdk/amazon-bedrock@5 signs with aws4fetch; there is no @aws-sdk/credential-providers in the tree (grep -c @aws-sdk agent/package-lock.json → 0) and agent.ts passes no credentialProvider, so AWS_PROFILE is ignored. Materialize the credentials instead:

eval "$(aws configure export-credentials --profile <profile> --format env)"

On the Vercel AI Gateway instead

export AI_GATEWAY_API_KEY=…        # vercel.com/dashboard/ai/api-keys
npx eve build && npx eve dev

Blocked today with customer_verification_required — the AI Gateway will not service inference until the Vercel team has a card on file. The credential itself authenticates fine (GET /v1/models returns 200).

Driving it without the TUI

SID=$(curl -s -X POST localhost:3000/eve/v1/session \
  -H 'content-type: application/json' \
  -d '{"message":"Which words carry weight in AUTH-24, and why?"}' | jq -r .sessionId)

curl -N "localhost:3000/eve/v1/session/$SID/stream"          # NDJSON events

An approval parks the run at session.waiting; answer it with:

curl -X POST "localhost:3000/eve/v1/session/$SID" \
  -H 'content-type: application/json' \
  -d '{"inputResponses":[{"requestId":"req_…","optionId":"approve"}]}'

What it may do

Three tools. preview_decomposition runs the real rule, read_corpus reads through the console’s overlay, propose_requirement submits assertNS at R0 behind always() approval. There is no bindTerm, no tool that accepts a number, and no agent principal — it writes through the same HTTP route the browser uses, attributed to the human whose approval released it. agent/README.md has the reasoning.

---

3. The gates, without Bazel

Most of the safety machinery runs on stdlib Python:

python3 conformance/check_conformance.py     # 295 checks
python3 tools/readmodel/check_wiring.py      # 194 checks
cd console && pnpm test && pnpm typecheck    # 108 vitest cases

The SPARQL gates need Bazel (bazel test //rdf/...), but they also run under rdflib if you only want to look:

pip install rdflib
python3 - <<'PY'
import re
from rdflib import Graph
g = Graph()
for f in ["rdf/ontology/authoring.ttl", "rdf/lint/authoring/fixtures/envelope-undocumented.ttl"]:
    g.parse(f, format="turtle")
q = re.sub(r"\A# ---.*?\n# ---\n", "", open("rdf/lint/authoring/envelope-unrecorded.rq").read(), flags=re.S)
print(len(list(g.query(q))), "rows — expect 1")
PY

⚠ ARQ is the engine that runs them in CI and it is the authority. rdflib disagrees with ARQ on at least one gate today: conflict-hygiene-strict finds 3 of its 4 planted defects under rdflib because of a date-comparison difference the query’s own comment documents. Do not “fix” a gate against rdflib.