multi-tenant-relay.md

Multi-Tenant Buzz Relay: A Formal Specification

draft

Abstract

This document specifies the data and authorization model that lets one shared Postgres instance, served by N stateless relay processes, host M independent communities without one community observing or acting on another, and gives a formal proof of its safety properties. It proves two families of property: isolation — a community is non-interfering with every other community across the relay's logical interface (query results, authorization decisions, emitted errors, and audit-chain contents) — and authorization soundness — no credential, signature, or forged event lets an actor cross a community boundary.

Today a Buzz relay process is the security boundary: one DATABASE_URL, one relay keypair, one relay-global relay_members table, with channel_id (the h tag) as the only sub-relay locality. The model proven here demotes the relay process to stateless compute and elevates a new community entity to the tenant/security boundary, carried as a community_id on every scoped row. That move collapses a process-level boundary into a row-level one. The contribution of this document is the formal characterization that the collapse loses nothing — proven relative to explicitly stated axioms about Postgres row-level security, Schnorr/NIP-98, a collision-resistant hash, and the relay's own channel_id → community_id resolution.

The architecture is not novel as a pattern: row-level multi-tenancy with a discriminator column and row-level security (RLS) is established practice (see §Prior Art). The contribution is the formal treatment — stating tenant isolation as non-interference encoded as a label-flow invariant (not a WHERE community_id = $1 predicate), mechanizing it (TLA+ for the concurrency/serving model, Tamarin for the authorization protocol under a Dolev-Yao adversary), and gating every invariant on a mutation test so the proof is non-vacuous.

Scope and Non-Goals

This specification proves safety ("nothing bad happens"). It deliberately does not prove:

• Liveness or performance. That a query meets a latency budget, or that a hot partition does not throttle, is empirical — characterized by the perf rig, not by theorem.
• Postgres's internal correctness. RLS enforcement, MVCC snapshot isolation, and ON CONFLICT DO NOTHING semantics are trusted and stated as axioms (§Axioms). We prove our composition on top of them; we do not reprove them.
• Cryptographic primitives. Schnorr signature unforgeability (BIP-340), the NIP-98 request binding, and second-preimage resistance of the event-id hash are the Tamarin model's equational theory, not reproven.
• Physical-resource isolation. Communities share an id space, time partitions, a connection pool, and a CPU. The proof covers the logical interface; bandwidth-limited physical channels are a named, explicit carve-out (§Isolation Boundary, class C1).
• Above-the-interface client leakage. The proof boundary is the relay's observational interface. If a client (a multi-tenant UI, an NIP-19 nevent share, a screenshot, a leaked log) surfaces a user's own event ids from community A while that user is also a member of B, the user then holds an A-id out-of-band and can probe the existence oracle from a B connection. The composite-index closure (A-RLS-5) means the probe still reveals nothing — B's write at that id is a fresh (community_id, id) key — but we name this surface explicitly: closing it for any weaker index shape is above the interface and is the client's obligation, not the relay's.

Stating this boundary is part of the claim. "Provably isolated" without naming the trust boundary does not survive scrutiny; "isolation is machine-checkable relative to these stated axioms, with every shared logical channel either closed in-model or closed by a named axiom" does.

System Model

A community C is the tenant/security boundary. It owns: a set of channels, a membership relation, a signing keypair, a token namespace, workflows, an audit hash chain, and the messages scoped to it. A community is a durable row in a communities table; creating one is an INSERT, never DDL.

The shared store holds three tiers:

• One canonical message log L: an append-only table keyed by (community_id, created_at, id). Every message carries the community_id of the community it belongs to. Append is idempotent (ON CONFLICT (community_id, created_at, id) DO NOTHING).
• A tenant-scoped control plane: relational, ACID tables — channels, channel_members, api_tokens, workflows, audit entries — each carrying community_id, kept relational because authorization needs synchronous current state.
• Disposable projections: mentions, thread metadata, reactions, full-text search — each community_id-keyed, rebuildable from L, never authoritative.

A relay process is stateless compute. It owns no community data; any process can serve any community, and N processes share the store.

A connection is bound to an actor (a pubkey, authenticated via NIP-42 on WebSocket or via a NIP-98-minted bearer token on REST). Every connection operation is evaluated under a TenantContext ⟨community_id, actor⟩. The community_id is resolved by the relay, never read from the client-supplied h tag or claimed community. For a channel-bearing operation it is the community of the channel the operation names (resolve : channel_id → community_id, an indexed lookup the relay owns under the same transaction snapshot as the operation), and the connection's host must agree with it — an A-host presenting a B-channel event is rejected fail-closed, never acted on as B. For a channel-less operation (profiles, DMs, long-form, status, read-state, lists — no h tag) it is the community bound to the connection's host at establishment (resolve_host : host → community_id, lifting today's per-relay URL identity up to the community); an unmapped host binds to no community and the connection is rejected fail-closed. The composed resolver is ResolveTenant(req, event) (see P-RESOLVE-HOST).

Two operation classes act on the store:

• Serve(ctx, q) — a read (REQ / REST GET, including direct ids lookup, #e/#a tag filters, metadata/member discovery, and projection reads). Returns rows and derived results matching q, confined to ctx.community_id.
• Accept(ctx, e) — a write (EVENT / REST POST). Appends e to L (or mutates control-plane state) under ctx.community_id, after an authorization decision over current control-plane state.

A community is either allowlisted or open. An allowlisted community admits actors only via a signed NIP-43 member list (§Authorization, S7); an open community (one with no member-pubkey allowlist) auto-registers any authenticated npub on AUTH — but the registration is stamped to the host-resolved community, never a client-claimed one, so "open" widens who may join, never which community they join. Two further control-plane writes are first-class: channel creation stamps a fresh channel atomically from HostCommunity[host] (the client supplies no community id, and the stamp is immutable thereafter), and no-#h reads — the kinds-only feed read and the #e-only aux read (reactions, edits, deletes, thread metadata) — resolve their community from the connection's host and are gated on host-community admission like every other channel-less operation. These surfaces are modeled, not asserted: see §Isolation (I5) and §Authorization (S5/S8).

The resolved community_id is the sole tenant authority. The h tag on a wire event is a routing hint a client asserts; it is never the commit point of tenancy. This is the confused-deputy hazard (Hardy 1988): the relay holds broad authority over a shared DB, and a client supplies an ambient name; if the relay acts on its broad authority under the client's name, the client escapes its community. The defense is capability discipline — authority is bound to the resolved object (community_id, channel_id, capabilities), never to a caller-supplied tag. The model treats the h tag as adversary-controlled and proves it is not load-bearing (Theorem I2 / S1).

Isolation Boundary

Tenant isolation is stated as non-interference: for any two executions equal on community B's inputs and initial B-visible state, B's observable outputs are equal regardless of community-A-only actions (Goguen–Meseguer 1982; the concurrent variant is observational determinism). A WHERE community_id = $1 row-return invariant is only one projection of this theorem — it implies nothing about timing, errors, uniqueness collisions, projection rebuild, or the auth gate. Two execution traces cannot be expressed directly in TLA+; the standard tractable encoding is a label-flow invariant: every state element (message row, membership, projection cell, in-flight query, emitted error, audit entry) carries the community label it originated from, and the single-run safety invariant is "no high-labeled value ever flows into a low-labeled observation." This encoding forces enumeration of every state element's label, which is what catches the projection-rebuild and error-surface channels that a predicate hides.

Shared channels split into two classes:

(C1) Bandwidth-limited physical channels — declared, out of scope. Buffer cache, autovacuum, planner statistics, partition right-edge throughput, and connection-pool tail latency are shared. A co-tenant can measure these as timing; the channel is bandwidth-bounded and orthogonal to the threat model (cross-tenant data leak, privilege escalation, audit forgery). We declare this class as git-on-s3 declares physical pack pruning: named, with a deferred future bandwidth bound. We do not claim timing non-interference.

(C2) Logical channels — in scope, enumerated, each closed. These are not carve-outs; a B-scoped connection can observe them at the interface, so each must be closed in-model or by a named axiom:

1. Event-id existence oracle. INSERT … ON CONFLICT DO NOTHING on the content-hash id: a B-writer observing zero rows affected learns some tenant wrote that id. Closed by A-RLS-5 (§Axioms): the uniqueness constraint is composite over (community_id, …, id), so a B-scoped write at an id A already holds gets a fresh key, not a conflict — B's rows-affected count is a function of B's own state alone, never A's. A_HASH is the supporting axiom: it additionally rules out the adversarial-search variant (B cannot find a fresh event hashing to a chosen id). Note the residual: A_HASH says nothing about ids B already knows out-of-band (NIP-19 nevent shares, multi-tenant client UIs that surface a user's own ids across communities) — that exposure is closed by the composite index, not the hash, and any above-the-interface client surface that leaks a user's A-ids while they are also in B is a named residual in §Scope and Non-Goals, not a relay-closed channel.
2. Constraint-violation error surface. Postgres errors can leak constraint names, conflicting tuples, and columns. Closed by a fixed sanitized error alphabet and the structural obligation that the relay emits only errors from that alphabet (an implementation code-fence, proven relative to it).
3. Projection rebuild path. A rebuild touches every community's events by construction. Closed by the invariant that rebuild writes server-side projection tables only and never serves rows to a tenant-scoped connection; a tenant query concurrent with a rebuild sees its own rows or none.
4. Unauthenticated global surface. The NIP-11 relay information document at / is unauthenticated and tenant-unscoped by construction; no B-scoped connection, no c.scope, no label exists, so the labeling invariant does not reach it. Closed by a typed-input code-fence: the doc-build function consumes only relay-static configuration types — no database handle, no tenant context, no audit service. Today RelayInfo::build (crates/buzz-relay/src/nip11.rs:122) takes only static inputs and nip11_facts (:176) reads only state.config/state.relay_keypair, so the surface is clean — but by current code, not by the proof; adding a total_events counter is one &PgPool argument away and the labeling invariant catches none of it. This is the same enforcement class as the Σ_err alphabet (C2.2) — a typed constraint at a seam, lintable over build's signature — but disjoint: Σ_err governs what symbols leave on authenticated paths, C2.4 governs what state populates unauthenticated paths. Any future unauthenticated relay-level endpoint (NIP-66 monitoring, health probes that expose counters) lives under C2.4 by default.

The numeric COUNT (NIP-45) and EOSE cardinality channels are deliberately not on this list: they are closed by the same label propagation as event rows (a count is |{B-labeled rows matching the filter}|), so they belong in the typed interface, not as distinct C2 mechanisms. The C2 list is the index of distinct closure mechanisms — A_HASH, the Σ_err alphabet, the rebuild behavioral invariant, and the C2.4 typed-input fence — not the index of channels.

(C3) Historical writes after revocation — declared, out of scope. The admission fence (I5, Inv_AdmissionFence) governs current capability: it proves that no membership or channel-less read capability survives for an actor not currently admitted to that community. Revocation (RevokeMember) removes the current admittedMembers row and therefore the capability, but it does not relabel or delete rows the actor wrote while admitted — those historical writes retain their original community label and remain present. This is sound and intended: the property we mechanize is "current membership and read capability track current admission," not "writes are retroactively un-admitted." We declare this as C1 declares physical timing: named, with retroactive-write redaction left to an operator data-lifecycle surface outside the isolation model. We do not claim historical writes are revoked when a member is revoked.

The typed observational interface

The non-interference theorem is stated over an interface: the exclusive set of observations a B-scoped connection (one whose resolved community is B) can make. Enumerating this set is load-bearing — a WHERE community_id = $1 invariant silently omits cardinality, error, status-code, and global-document channels. Any observation not in this set is either C1 (declared) or a model violation. There is no third category. Each entry below names its code seam so the TLA+ model, the Tamarin model, and the red-team audit reference the same surface.

O.WS — WebSocket transport (crates/buzz-relay/src/protocol.rs:180-215). The relay emits exactly these client-bound messages:

• O.WS.EVENT(sub_id, event) — a delivered Nostr event. Its content is high-labeled at the row's community; e/p/q tag references inherit the row's label (they may name globally-existing ids, but the row reaches B only if B-labeled).
• O.WS.EOSE(sub_id) — end-of-stored-events. The count of preceding events is the cardinality of B-visible rows matching the filter; it must be a function only of B-labeled state.
• O.WS.OK(event_id, accepted, message) — write ack. event_id echoes the submission (benign); accepted is a function of (validity, signature, resolved scope, dedup) over B-labeled state only; message is drawn from the sanitized alphabet Σ_err (the C2.2 seam — the current String type admits any value).
• O.WS.NOTICE / O.WS.CLOSED — out-of-band and sub-termination strings; same Σ_err constraint (connection.rs:307,326).
• O.WS.AUTH(challenge) — NIP-42 challenge; a fresh nonce, function of relay randomness only, never of any tenant's writes.
• O.WS.COUNT(sub_id, n) — NIP-45 count (protocol.rs:213). n is a numeric channel: even under row confinement, a count touching non-B rows leaks A's cardinality. The rule: n is the count of B-labeled rows matching the filter, full stop.

O.REST — HTTP API surface.

• O.REST.BODY — JSON response: row content, projection results, and audit entries (crates/buzz-audit/src/service.rs:get_entries) must all be B-labeled.
• O.REST.META — status code, headers, structured error envelope. The status code is itself observable: IngestError::{Rejected,AuthFailed,Internal} → 400/401|403/500 (handlers/ingest.rs:138-146) must be a function of {request, B-labeled state}, never of A's state.

O.AUTH — auth verdict. The Boolean "did this pass the gate," observable via O.WS.OK.accepted and O.REST.META.status. It is a function of (submitted credentials, server-side resolution channel_id → community, B-labeled membership/token/policy state). The claimed community never appears in this function — only the resolved one. (Theorem S1.)

O.AUDIT — audit chain. get_entries(scope=B) returns only B-chain entries; verify_chain(scope=B) is decidable from B-labeled entries alone; compromise of A's chain key does not affect B's. (Theorem S4.)

O.NIP11 — relay info document (/). Global and unauthenticated, so by construction it cannot be tenant-labeled — therefore its content must be a function of relay-static configuration only. supported_nips is fine; total_events would be a cross-tenant leak.

Everything outside this set is C1 (wall-clock latency, buffer-cache hit rate, planner choice, autovacuum, partition right-edge throughput, pool saturation, memory/fd/scheduler effects — declared, bandwidth-bounded) or closed by axiom (the INSERT … ON CONFLICT DO NOTHING id-existence oracle at event.rs:151, closed by A_HASH).

Label-propagation rules

The labeling discipline that makes non-interference a single-run safety invariant (every state element carries a community label; the invariant is "no high-labeled value flows into a low observation"):

• L1 — Source label. Every event row carries community_id, set by the server-side resolver at insert time via ResolveTenant. For a channel-bearing event the label is resolve(channel_id); for a channel-less event (kind:0 profiles, 1059 DMs, 30023/30174/30315/30078, lists — channel_id = NULL) the label is the connection's host-bound community resolve_host(connection.host), with the token stamp required to agree (never to supply it). The h tag is not the label source, and neither is the client-claimed community. (Resolution is a fence — see P-RESOLVE and P-RESOLVE-HOST.)
• L2 — Projection inheritance. Each projection row (event_mentions, thread_metadata, reactions, FTS) inherits its source event's label; rebuild = replay of labeled source rows, so rebuilds preserve labels by construction.
• L3 — Audit partitioning. N independent chains, one per community label; community-scoped writers only; no cross-chain reference, no global "latest" head.
• L4 — Auth-verdict label. The allow/deny verdict carries the resolved community label, never the claimed one.
• L5 — Token stamp. A NIP-98 token has exactly one community stamp, assigned at mint from the resolved channel set; a mint resolving to >1 community is rejected fail-closed (S2). The token's label is its stamp.
• L6 — Connection scope. A connection has exactly one resolved community at a time, bound from its host (resolve_host(connection.host)) at establishment before any handler runs; re-scoping requires a new connection to a different host; all its observations inherit that scope. An unmapped host binds to no community and is rejected fail-closed (P-RESOLVE-HOST), never defaulted.
• L7 — Error label. A finite, statically-declared alphabet Σ_err governs the authenticated, tenant-scoped WS error surface: every O.WS.OK.message, O.WS.NOTICE, and O.WS.CLOSED is drawn from it (the 9 NIP-01-reachable prefixes — auth-required, restricted, invalid, duplicate, pow, rate-limited, blocked, error, frame-too-large). Emitting a non-Σ_err string is a structural code violation (the C2.2 code-fence — a lint, not a model property). Today RelayError::Database(#[from] buzz_db::DbError) (error.rs:11) is the seam. The unauthenticated/REST error surface (not-found, bad-request) is a distinct fence — C2.4's typed-input constraint, not Σ_err — because it has no tenant scope and no label, so it sits outside the labeling invariant entirely. One Rust enum may back both for ergonomics, but the model treats them as two alphabets closed by two mechanisms.
• L8 — No injection. Per L7, A-labeled state cannot influence which Σ_err symbol B observes.

In one line: for every reachable state s, every B-scoped connection c, and every observation o ∈ O.* ∪ Σ_err emitted to c, o is a deterministic function of (B-labeled state in s, c's request history, relay-static config); no A-labeled element is an input to o. This is what the TLA+ model encodes — strictly stronger than row-equality, because it forces enumeration of every observation channel above.

Axioms

The proof holds relative to the following. Each is a documented property of Postgres / the crypto primitives, and a testable assumption admitted per deployment (§Conformance).

Row-level security (the fail-closed backstop)

Postgres RLS is fail-closed only under specific configuration (PostgreSQL manual, "Row Security Policies"). We state the configuration as obligations:

• (A-RLS-1) Every queryable tenant-bearing table has RLS enabled with a restrictive policy community_id = current_setting('app.community_id')::uuid, and no permissive policy that admits cross-tenant rows.
• (A-RLS-2) The relay's request role is non-superuser, NOBYPASSRLS, and not the table owner unless FORCE ROW LEVEL SECURITY is set (owners and BYPASSRLS roles bypass policies).
• (A-RLS-3) app.community_id is set transaction-locally (SET LOCAL) before any query and cleared at transaction end. Pooled connections must not retain or combine tenant context across requests.
• (A-RLS-4) SECURITY DEFINER and leakproof/user-defined functions in the request path are audited as part of the trusted boundary: a leakproof function may be evaluated ahead of the RLS check, and a SECURITY DEFINER function can read data unavailable to the caller.
• (A-RLS-5) Uniqueness and foreign-key constraints include community_id, so a conflict outcome or a dangling reference cannot reveal or reach another community.

A query that fails to set app.community_id matches the policy predicate over NULL → no rows, never all rows. This is what makes a missed application predicate fail closed rather than leak (Theorem I4).

Concurrency, crypto, and resolution

• (P-APPEND) INSERT … ON CONFLICT (community_id, created_at, id) DO NOTHING commits a row iff no row with that key exists; concurrent appends are serializable under MVCC; a committed row is never silently overwritten; a read sees a consistent snapshot.
• (P-SIG) An actor cannot produce a valid Schnorr signature (BIP-340) for a pubkey whose secret key it does not hold. A NIP-98 event's u/method/ payload tags bind it to exactly one HTTP request and are non-transferable to a different request.
• (P-RESOLVE) resolve : channel_id → community_id is a total function over existing channels, computed from control-plane state under the operation's transaction snapshot. A channel belongs to exactly one community (channels.community_id NOT NULL); resolution never returns a community a channel does not belong to. A channel's community is set at creation and never reassigned: channels.community_id is immutable after insert. Both mechanized models encode this — Tamarin as the persistent !ChannelCommunity fact (MultiTenantAuth.spthy:51, once-true-always-true), TLA+ as the ChannelCommunity CONSTANT function (MultiTenantRelay.tla:107). Any future re-tenanting would be a separate axiomatic admission with its own audit discipline and re-verification of S1/S2 (and I1–I5).
• (P-RESOLVE-HOST) resolve_host : host → community_id ∪ {⊥} is the upstream binding for every connection, lifting today's per-relay URL identity one level up to the community. A connection's community is resolve_host(host), fixed at establishment; the URL the client connects to is the selector, exactly as a relay URL is today. ResolveTenant(req, event) composes the two: if the event has an h tag, require resolve(h) = resolve_host(host) (the host/channel agreement fence — an A-host presenting a B-channel event is a confused deputy on the host axis and is rejected fail-closed, never acted on as B) and store that community; if it has none, store community_id = resolve_host(host), channel_id = NULL. Two fences hold for both paths. Fail-closed: a host/channel disagreement (incl. an unmapped host resolving to ⊥, which can never equal a real channel community) is rejected generically (auth-required/restricted), never bound to a default tenant — resolve_host is partial and the absence/disagreement of a binding is a reject, not a fallback. Host wins: a NIP-98 token's community stamp (L5) must agree with the host-derived community; a token that disagrees is rejected, so the confused-deputy fence (I2) is intact with authority binding to the host-resolved object. Tamarin encodes this as the persistent !HostCommunity fact (MultiTenantAuth.spthy): the channel-less use rule fires only when token stamp and host community coincide (witness ChannelLessResolved, lemma channelless_use_confined_to_host_community), and the channel-bearing use rule fires only when the channel mapping and the host community coincide (witness ChannelBearingResolved(tok, used_comm, host, host_comm), lemma channelbearing_use_agrees_with_host asserting used_comm = host_comm). TLA+ encodes it as the HostCommunity resolver (with a ⊥ sentinel for unmapped hosts) and an Inv_HostBindingFence invariant quantifying over every accepted write — channel-bearing and channel-less — and every observable duplicate/no-op outcome, that its stored community equals its originating host's mapping. The duplicate/no-op path carries the same obligation because it is client-observable write surface (the Duplicate result exposes the scoped existence/conflict rows): an A-host presenting a B-channel id is fenced before any conflict lookup, so it cannot learn whether that id exists in B. At N = 1 this is byte-identical to today: one host → the one community, every connection lands there, nothing client-observable changes.
• (A_HASH) The event id sha256(canonical event) is second-preimage resistant: an actor cannot find a distinct event hashing to a chosen id. (NIP-01 already relies on this; we cite it the way git-on-s3 cites its CAS axiom.)
• (P3) NIP-98 mint freshness. A NIP-98 mint event (kind:27235) is accepted at most once. The implementation enforces this with two checks: a created_at within ±60s of server time (buzz-auth/src/nip98.rs:77-83, TIMESTAMP_TOLERANCE_SECS = 60) and a seen-set keyed on event id (buzz-relay/src/api/bridge.rs::check_nip98_replay), whose cache TTL (120s, state.rs:407) is 2× the window so a mint valid at either edge stays tracked for the full window. The Tamarin model abstracts the window as a fresh nonce on ~time (MultiTenantAuth.spthy:91), which over-approximates the implementation by treating every mint as structurally unique; the spthy comment at :84-86 references this obligation as "P3."

P-RESOLVE is the load-bearing application assumption for channel-bearing events and P-RESOLVE-HOST is its channel-less counterpart — together the fence the h-tag and claimed-community adversary cannot circumvent. A-RLS-1..5 are the load-bearing backstop.

Safety Theorems

Isolation (mechanized in TLA+)

• NI (Non-interference, master). For every reachable state and every B-scoped observation, the observed value is a function only of B-labeled state — no high-labeled value flows into a low-labeled observation. I1–I5 are the specific flows it rules out, each independently mutation-tested non-vacuous.
• I1 (Read confinement). Every row a Serve returns — including direct-id and #e/#a lookups — is ctx.community-labeled.
• I2 (Resolution fence). ctx.community = resolve(channel_id) for channel-bearing events and resolve_host(host) for channel-less ones, never the h tag, the claimed community, or the token stamp; an adversary h = C' ≠ resolve = C cannot widen what is served or accepted. The host axis is fenced on both paths: a channel-less write over host A cannot land in community B, and a channel-bearing op over host A on a B-channel is rejected rather than acted on as B — including the duplicate/no-op outcome, so an A-host cannot use a B-channel id-conflict result as a cross-tenant existence oracle (Inv_HostBindingFence quantifies over accepted writes and recorded duplicates, making "default to C", "A-host drives a B-channel insert", and "A-host probes a B-channel duplicate" caught mutations, not invisible ones).
• I3 (Write non-loss & no cross-contamination). Every accepted append commits under the resolved label and no other; no committed message is lost or overwritten; two communities appending the same event id land as two rows under distinct labels (cross-community id collision is not a write conflict).
• I4 (Fail-closed backstop). A dropped application predicate yields ∅ under A-RLS, and NI still holds; removing the RLS guard makes the dropped predicate produce a cross-label row — proving RLS load-bearing, not decorative.
• I5 (Admission fence). Channel membership and channel-less read capability exist only for actors admitted to that community. The NIP-43 allowlist is the admittedMembers relation keyed on (community, actor); AddMembership and every channel-less read are gated on IsAdmitted(c, a), and Inv_AdmissionFence quantifies over every membership and every recorded channel-less read, requiring same-community admission on both — the channel-less branch additionally binding HostCommunity[host] = community, so the host axis is fenced here too. The same gate covers the open-community and no-#h-read surfaces: an open community auto-registers an authenticated npub into the host-resolved community (AuthenticateOpenCommunity recording an authRegistration), and the kinds-only feed read (ReadHostFeedRows) and #e-only aux read (ReadHostAuxRows) each record a witness only when the actor is IsAdmitted to the host community — Inv_AdmissionFence quantifies over those witness sets too, so an actor admitted only in B can neither open-register into A nor read A's no-#h feed/aux. Channel creation (CreateChannel) stamps a fresh channel from HostCommunity[host] and Inv_ChannelCommunityImmutable proves that stamp is never re-labeled — creation is an in-relay analog of S2's resolve-then-immutable discipline. The fence is about current capability: it is mutation-tested non-vacuous by M9 (re-keying the membership/read gate to any-community admission), which goes red on both a membership trace and a channel-less-read trace, and by M10–M13 (the open-AUTH, channel-create, feed-read, and aux-read stamp/gate mutations), each confirmed red — proving an admit-into-A then act-in-B escape is caught rather than invisible on every one of these surfaces. (See C3 for the explicit historical-write carve-out.)

Authorization soundness (mechanized in Tamarin, Dolev-Yao adversary)

• S1 (Token confinement). A token accepted for a B-resolved operation was minted with stamped community B; a token stamped A never authorizes in B. A leaked token authorizes within its own community (blast radius is not zero and we do not pretend otherwise) but never another — containment, proven.
• S2 (Mint integrity). A token exists only as the output of a NIP-98 mint by the holder of owner_pubkey's key (P-SIG); it carries exactly one stamped community; a mint whose channel set spans two communities yields no token. S2's trace-level mint-rejection closure relies on P-RESOLVE's totality, single-valuedness, and immutability: the Tamarin model encodes immutability via persistent-fact semantics (!ChannelCommunity), without which a retag-then-replay — reject a cross-community req, retag a channel, replay the original mint bytes (same req hash) — would mint a token for a request S2 declares unmintable. This is the structural analog of A-RLS-5's UNIQUE (community_id, id) clause for I1: both turn stable scope into the disjointness witness.
• S3 (Signing-key non-confusion + containment). A community-B-signed system event (NIP-29 39000/39001/39002) is never accepted as an authentic community-A event, even when group ids collide; compromise of B's signing key does not let the adversary forge A's events.
• S4 (Audit-chain unforgeability + containment). No splice, reorder, or forge in community A's hash chain; compromise of B's chain does not break A's — N independent chains, N independent guarantees.
• S5 (Channel-less host confinement). A channel-less authorization (profiles, DMs, long-form, lists — no h tag) is confined to the community bound to the connection's host, not the token's stamp: host wins. The token must agree with the host community or the request is rejected; a B-stamped token presented over an A-host never authorizes for B. This is I2's host counterpart, mechanized as channelless_use_confined_to_host_community, channelless_token_agrees_with_host, and host_token_mismatch_not_authorized.
• S6 (Channel-bearing host/channel agreement). A channel-bearing authorization is confined to the community bound to the connection's host: the host and the channel mapping must agree. An A-host presenting a B-channel event never authorizes as B — the host axis of the confused-deputy fence, which the prior model proved only on the channel axis (claimed-community ignored). This closes the cross-tenant escape over a wildcard host route where the channel mapping alone would have been authoritative. Mechanized as channelbearing_use_agrees_with_host (the single-witness ChannelBearingResolved fact asserting used_comm = host_comm).
• S7 (NIP-43 admission confinement). A community's member-list (NIP-43) admission is confined to the community whose signing key signed it: B's signing key can never admit a pubkey into A. Modeled as a parallel rule pair — Community_Signs_NIP43_MemberList mints the signed list and Relay_Accepts_NIP43_MemberList re-verifies the signature against !CommunitySigningKey(comm, sk), so comm is bound by unification to the resolved community (the same confused-deputy discipline as the S5/S6 host fence), emitting persistent !Admitted(pk, comm). nip43_admission_confined_to_signing_community proves the confinement; the commented MUTATION_Admit_Ignore_Community (the dual of S6's MUTATION_Use_Token_Ignore_Host) falsifies it, confirming the green is non-vacuous. This is the authorization-world half of the same admission property TLA+'s I5 proves in the in-relay world: !Admitted(pk, comm) / MemberAdmitted(pk, comm) ⇔ admittedMembers/IsAdmitted(c, a) — one property, two worlds (Tamarin proves the admission event per-community unforgeable, TLA+ proves the resulting capability in-relay scoped).
• S8 (Open-community AUTH confinement). When a community carries no NIP-43 member-pubkey allowlist it is open: any authenticated npub auto-registers on AUTH. The registration is still confined to the host-resolved community — Authenticate_To_Open_Community stamps the registration from the connection's host binding, never a client-supplied selector, so "open" relaxes the gate on membership without relaxing the boundary it lands in. Mechanized as open_auth_registration_confined_to_host_community (a host-bound npub registers only into its host's community), with the exists-trace witness executable_open_auth_registration proving a legitimate open registration is producible so the confinement lemma is non-vacuous. This is S5/S6's host-binding discipline applied to the admission event: the same confused-deputy fence that stops a B-stamped token authorizing over an A-host stops a B-host AUTH registering into A. Its in-relay counterpart is I5's open-community branch (AuthenticateOpenCommunity, mutation M10).

Each Tamarin lemma is paired with an exists-trace sanity lemma (the honest protocol can run), the Tamarin analog of the mutation test.

Verification status. S1–S8 are machine-verified green on Tamarin 1.12.0 / Maude 3.5.1 — the full selected run verifies all 32 lemmas in ~12s with zero analyzed failures. S1/S2: token_confinement, cross_community_use_attempts_are_not_authorized, the two minted_*_channels_match_stamp lemmas, token_stamp_matches_mint, cross_community_mint_yields_no_token_for_that_request, and the leaked_token_blast_radius_contained / leaked_token_can_authorize_within_its_community containment pair, with MUTATION_Use_Token_Claimed_Community confirmed red (falsified — found trace). S3: system_event_acceptance_requires_same_community_key_or_compromise (21 steps) and other_community_key_compromise_does_not_authorize (147 steps). S4: audit_append_advances_same_community_head (2 steps) and cross_community_audit_splice_attempt_is_not_append (1 step). S5 (channel-less host confinement): channelless_use_confined_to_host_community (2 steps), channelless_token_agrees_with_host (3 steps), and host_token_mismatch_not_authorized (6 steps), each paired with an exists-trace probe (executable_host_bound, executable_channelless_use, executable_host_token_mismatch_attempt). The S5 mutation MUTATION_Use_Token_ChannelLess_Ignore_Host (the relay reading the token's stamp and ignoring the host binding — the B-token-on-A-host confused deputy) is confirmed red: it falsifies channelless_use_confined_to_host_community in 3.3s with a 13-step trace. Each safety lemma is paired with a verified exists-trace sanity lemma, and the S3/S4 mutations are confirmed red: the bad-accept-with-other-community-key mutation falsifies both S3 lemmas (5 / 16 steps) and the splice-as-append mutation falsifies the S4 splice lemma (8 steps). S6 (channel-bearing host/channel agreement): channelbearing_use_agrees_with_host (2 steps), with the MUTATION_Use_Token_Ignore_Host mutation (the relay resolving a channel-bearing op from the channel mapping while ignoring the host binding — the A-host-on-a- B-channel confused deputy) confirmed red: it falsifies channelbearing_use_agrees_with_host in 2.6s with a 14-step trace. S7 (NIP-43 admission confinement): nip43_admission_confined_to_signing_community (19 steps) and other_community_key_compromise_does_not_admit (79 steps), with the exists-trace probe executable_member_admitted (7 steps) proving a legitimate admission is producible — so the confinement lemma is non-vacuous, not trivially true over an unreachable premise. The S7 mutation MUTATION_Admit_Ignore_Community (the relay minting !Admitted for a community other than the one whose key signed — the admission-side confused deputy, the dual of S6's MUTATION_Use_Token_Ignore_Host) is confirmed red: it falsifies nip43_admission_confined_to_signing_community in 1.57s with a 7-step trace. S8 (open-community AUTH confinement): open_auth_registration_confined_to_host_community (2 steps), paired with the exists-trace witness executable_open_auth_registration (5 steps) proving a legitimate open-community registration is producible, so the confinement lemma is non-vacuous; its in-relay counterpart is the M10 open-AUTH stamp mutation, confirmed red in TLA+ (a 2-state Inv_AdmissionFence violation).

The S5 confinement lemma was deliberately framed to keep its mutation cheaply refutable. An earlier framing joined two action facts (ChannelLessAuthorized ⋈ HostBoundFor) on a shared host; the proof verified, but the mutation refutation did not terminate — Tamarin chased which HostBoundFor instance applied for a given host across both the real and mutated rules. The fix emits a single combined witness ChannelLessResolved(tok, used_comm, host, host_comm) from the authorizing rule (in the real rule both communities are the same variable), so the confinement lemma is a single-fact assertion used_comm = host_comm and the mutation that breaks it is a one-rule-instance counterexample. The proof dropped to 2 steps and the mutation falsifies in 3.3s — the same "make the bad case structurally cheap to exhibit" discipline as the S1 claimed-community mutation.

The S3/S4 round corrected one vacuity bug in the committed 1e7fb042…aceaacf24 artifact: other_community_key_compromise_does_not_authorize bound Neq(commA, commB) to the same timepoint as CommunityKeyCompromised(commB), but no rule emits Neq at the compromise point, so that premise was unsatisfiable — the lemma verified vacuously and asserted nothing. (Independently confirmed: an exists-trace probe of the old premise returns no trace found.) The fix decouples the inequality onto a separate witness timepoint #k; a new exists-trace lemma executable_other_key_compromise_plus_system_accept (16 steps, verified) proves the corrected premise is satisfiable, so the 147-step proof is non-vacuous. This is the same hygiene class as F1/F3/F4 — an artifact relying on a fact the model never makes reachable — but caught inside a safety lemma's premise rather than a comment. That fix predates this milestone's host-binding additions and is carried forward unchanged in the current .spthy.

Conformance

Each axiom is admitted per deployment, not assumed universally:

• A-RLS-1..5 are admitted by a startup/CI assertion suite: enumerate every tenant-bearing table and assert RLS enabled + restrictive policy present; assert the request role is NOBYPASSRLS and non-owner-or-FORCE; assert no SECURITY DEFINER function in the request path reads tenant tables without re-establishing context; assert every unique/FK constraint includes community_id. A failing assertion rejects the deployment.

• P-RESOLVE is admitted by the channels.community_id NOT NULL constraint plus a test that resolve is read under the operation's snapshot, plus a migration lint asserting channels.community_id is never mutated after insert (no UPDATE/ALTER/drop-recreate). A failing lint rejects the deployment.

• P-SIG / A_HASH are the standard Nostr crypto assumptions; admitted by using the audited libraries the rest of Buzz uses.

• P3 is admitted by the NIP-98 handler enforcing both timestamp-range validation and the seen-event-id check (check_nip98_replay) before any mint. Two structural gates make the seen-set sound, and both are conformance checks because the implementation is silent if either is violated:

  1. Capacity vs. rate. The seen-set is bounded (capacity 10,000, TTL 120 s = 2× the ±60 s window). It must satisfy capacity ≥ peak NIP-98 RPS × 120 s (≈ 83 RPS sustained at the current capacity); above that, LRU eviction can release an entry while its signed created_at is still inside the window, and a replay slips through.
  2. Per-pod scope. The seen-set is Arc<AppState>-scoped, not cross-pod, so the same replayed event reaching two pods succeeds once on each. P3 therefore requires either NIP-98 mints be pod-sticky on event_id or the seen-set be shared across pods (e.g. Redis with the same atomic insert-if-absent semantics and TTL ≥ 120 s). The chart default (replicaCount: 1) satisfies this gate today; the shipped HA examples (replicaCount: 3 in deploy/charts/buzz/examples/argocd-app.yaml:27 and deploy/charts/buzz/examples/flux-helmrelease.yaml:35) are P3-non-conforming as shipped unless the operator adds one of:
     • (a) an ingress annotation hashing upstream selection on a header stable across replays — nginx.ingress.kubernetes.io/upstream-hash-by: "$http_authorization" works for today's NIP-98 HTTP path, since the signed event rides in Authorization: Nostr <base64> (bridge.rs:34-46) and is bit-identical across replays. Two caveats keep this from being the recommended fix: it couples replay-stickiness to literal-byte-identity of the auth header (any future header normalization — whitespace, casing, base64 padding — silently breaks it), and it does not extend to any mint path that moves off HTTP (a WS mint has no Authorization header to hash on).
     • (b) a shared seen-set backed by a store with atomic insert-if-absent and TTL ≥ 120 s (e.g. Redis, already present in the HA chart for git-pubsub). This is the recommended path — no new infra surface and none of (a)'s fragility.

  A regression test asserts a replayed mint within the window yields a single token under the deployment's routing/storage shape (and that the seen-set TTL covers the full ±60 s window). A failing test or an unmet gate rejects the deployment.

Prior Art

The pattern (discriminator column + RLS) is established; the formal treatment as label-flow non-interference is, to our knowledge, new for a Nostr relay.

• Goguen & Meseguer, "Security Policies and Security Models" (IEEE S&P 1982) — the origin of non-interference; the theorem shape ("A's actions do not affect B's observations"), with "community" for "security domain."
• Sabelfeld & Myers, "Language-Based Information-Flow Security" (IEEE JSAC 2003) — the canonical label-based IFC survey; its declassification discipline is the model for our named C1 carve-out.
• Jean Yang et al., "Precise, Dynamic Information Flow for Database-Backed Applications" (arXiv:1507.03513, Jacqueline) and Parker, Vazou, Hicks, "LWeb" (arXiv:1901.07665) — the closest formal analogs: label-based per-row policy over a real relational store with a mechanized non-interference proof. They justify "RLS is a backstop axiom; the theorem is the composition."
• Hardy, "The Confused Deputy" (ACM SIGOPS OSR 1988) and Miller et al., "Capability Myths Demolished" (HPL-2003-222) — the resolution-as-capability framing: bind authority to the resolved object, not the caller-supplied name.
• NIP-29 (relay-based groups) — confirms the relay is authoritative and group ids are not globally unique security domains; supports per-community signing keys and per-community audit chains, and motivates S3's "non-confusable even when group ids collide."
• fiatjaf/relay29 — empirical prior art: isolation logic lives across read filters, direct-id lookups, metadata generation, in-memory state rebuilds, and previous-tag validation, not just insert/select predicates. The reason Serve must model the full observable surface, not just channel reads.
• PostgREST / PostGraphile — converge on the transaction-local-context fence (A-RLS-3); real systems install request-local identity into the DB transaction and let policies authorize. (See RESEARCH/MULTITENANT_ISOLATION_PRIOR_ART.md for citations and local checkout line references.)

Mechanized Verification

• docs/spec/MultiTenantRelay.tla + .cfg — the TLA+ isolation model. Run: java -cp tla2tools.jar tlc2.TLC -config MultiTenantRelay.cfg MultiTenantRelay.tla. On the core finite harness (2 communities × 4 channels, 2 message ids, 1 actor, 1 worker, 2 audit values, bounded observation set, symmetry over the permutable model-value sets) TLC completes exhaustively: Model checking completed. No error has been found. — 472,530,528 states generated, 16,226,016 distinct, 0 left on queue, depth 13 (8 workers, ~5m). The distinct-state count grew from the pre-host-binding baseline (4,350,464 → 5,091,328 with channel-less host binding → 5,621,760 with channel-bearing host/channel agreement → 9,232,992 with the admittedMembers allowlist, channelLessReads capability rows, and the AdmitMember/RevokeMember actions → 16,226,016 with the open-community AUTH auto-registration, server-stamped channel creation, and the no-#h host feed/aux read paths) precisely because the channel-less write path, the fail-closed unmapped-host path, the channel-bearing host/channel-agreement (and its fail-closed disagreement) path, the admit/revoke/gated-membership/gated-read paths, and now the open-AUTH/channel-create/feed-read/aux-read paths are genuinely reachable — new behavior, not dead code. Threading the host through the duplicate/no-op path adds reachable fail-closed transitions without new distinct states: only the agreeing host can produce a recorded duplicate, so the host on that path is fully determined; layering the admission gate, then the open-AUTH/channel-create/feed/aux surfaces on top, is the growth to the figures above (admit-then-act, revoke-then-act-fails, gated reads/joins, open-community auto-registration, server-stamped creation, and the two host-fenced no-#h read shapes multiply the reachable space). That each new surface is reachable rather than dead is pinned by four intentionally-false reachability probes (Probe_OpenAuthRegistration_Unreachable, Probe_CreatedChannel_Unreachable, Probe_HostFeedRead_Unreachable, Probe_HostAuxRead_Unreachable): each asserts the corresponding witness set stays empty, so each must go red if its action fires — and all four do (open AUTH and channel-create at 2 states; host feed and host aux at 3 states, via open AUTH then read). A vacuously-passing new conjunct over an unfireable action is therefore ruled out, not assumed. Non-vacuity of the invariants themselves is shown by thirteen mutations (M1–M13), each confirmed to produce a counterexample: substituting the unscoped direct-by-id lookup (UnscopedDirectIdRows, the get_accessible_channel_ids landmine) → Safety violated at depth 4; widening the sanitized-error label to all communities (the raw-error leak) → Safety violated at depth 2; the global-id conflict key (M3: WriteDuplicate keyed on id alone via GlobalConflictRows, the missing-community_id-in-the-unique-index footgun) → Safety violated at depth 3, with a B-scoped WriteResult observation carrying labels |-> {commA} (the existence-oracle leak C2.1 closes); the host-default-tenant mutation (a channel-less write from an unmapped host landing in a default community instead of failing closed) → Inv_HostBindingFence violated at depth 2, the counterexample exhibiting hostBad writing into commA; the M8 host/channel-agreement mutation (WriteInsert dropping the agreement fence so an A-host op on a B-channel is accepted) → Inv_HostBindingFence violated by a 2-state trace (Init → WriteInsert); and the M8-duplicate mutation (WriteDuplicate dropping the same fence so an A-host can probe a B-channel id-conflict) → Inv_HostBindingFence violated by a 3-state trace (Init → WriteInsert → WriteDuplicate), the counterexample exhibiting a foreign-host duplicate record whose stored community ≠ its host's mapping (the existence oracle the duplicate path would otherwise reopen); and the M9 global-allowlist mutation (re-keying the admission gate from same-community IsAdmitted(c, a) to any-community AdmittedInAnyCommunity(a)) → Inv_AdmissionFence violated in two surfaces: a 5-state membership trace (Init → WriteInsert → WriteInsert → AdmitMember(commA, alice) → AddMembership(commB/chanB1, alice)) where alice, admitted to A, joins B's channel through the global hole; and a 4-state channel-less-read trace (Init → WriteInsert → AdmitMember(commB, alice) → ReadMessageRows(commA, NoChannel, hostA)). The two M9 variants prove both the AddMembership gate and the channel-less-read gate are independently load-bearing, not just one. The four newest surfaces — open-community AUTH auto-registration, server-stamped channel creation, and the two no-#h host read shapes (kinds-only feed, #e-only aux) — are each held by their own confirmed-red mutation: the M10 open-AUTH stamp mutation (the relay stamping an open-community auto-registration into a default/claimed community instead of HostCommunity[host]) → Inv_AdmissionFence violated by a 2-state trace (Init → AuthenticateOpenCommunity(hostB stamps commA)), catching an authRegistration whose host maps elsewhere; the M11 channel-create stamp mutation (a fresh channel stamped into a default/claimed community rather than the host's) → Inv_HostBindingFence/Inv_ChannelCommunityImmutable violated by a 2-state trace (Init → CreateChannel(hostB stamps commA)); the M12 feed global-admission mutation (re-keying the ReadHostFeedRows admission guard from same-community IsAdmitted(c, a) to relay-global GloballyAdmitted(a)) → Inv_AdmissionFence violated by a 3-state trace (Init → AdmitMember(commB, alice) → ReadHostFeedRows(hostA)), so an actor admitted only in B cannot read A's no-#h feed; and the M13 aux global-admission mutation (the same guard re-key on ReadHostAuxRows) → Inv_AdmissionFence violated by a 3-state trace (Init → AdmitMember(commB, alice) → ReadHostAuxRows(hostA)). M10–M13 confirm the open-AUTH/create/feed/aux fences are load-bearing, not decorative — the same "every new conjunct earns a confirmed red" contract as M1–M9. (To reproduce M12/M13, the substitution that trips Inv_AdmissionFence is the action's admission guard (IsAdmitted(c, a) → GloballyAdmitted(a) in ReadHostFeedRows/ReadHostAuxRows), not the row-set helper alone, since the invariant quantifies over the recorded feedReads/auxReads witnesses rather than the returned row set — the .tla helper comments call this out.) The host-fence and new-surface figures above are counterexample trace lengths (the error-trace state count), which unlike TLC's run-dependent "depth of complete graph search" total are reproducible from the printed error trace. The h-tag mutation is the same shape (I2). The config is deliberately a fast non-vacuity harness, not the full deployment scale — widening workers, actors, and ids explodes the space; symmetry + bounded observations keep the core isolation surface exhaustively checkable.

• docs/spec/MultiTenantAuth.spthy — the Tamarin authorization model. Run: tamarin-prover --prove docs/spec/MultiTenantAuth.spthy. All 32 lemmas (S1–S8) verify green (Tamarin 1.12.0 / Maude 3.5.1, ~12 s) — each safety lemma paired with a verified exists-trace sanity lemma, and the documented mutations (MUTATION_Use_Token_Claimed_Community for S1, the S3 bad-accept and S4 splice-as-append mutations, MUTATION_Use_Token_ChannelLess_Ignore_Host for S5's host fence, MUTATION_Use_Token_Ignore_Host for S6's channel-bearing host/channel-agreement fence, and MUTATION_Admit_Ignore_Community for S7's NIP-43 admission confinement) confirmed red. The 32 lemmas include the open-community AUTH pair added with the host-scoped-open-auth surfaces: open_auth_registration_confined_to_host_community (2 steps) proves an open-community auto-registration commits to the host-resolved community and never a client-claimed one, and its exists-trace witness executable_open_auth_registration (5 steps) proves a legitimate open-community registration is producible, so the confinement lemma is non-vacuous. See §Authorization soundness for the full lemma list, the S5/S6 single-witness framing, and the corrected other_community_key_compromise_does_not_authorize vacuity fix.

  Machine-check hygiene. S1–S8 lemmas close by two distinct shapes. Rule-shape closure means the lemma's conclusion follows by unification on a single rule's action multiset: token_confinement, audit_append_advances_same_community_head, channelless_use_confined_to_host_community (the S5 single-witness fact), channelbearing_use_agrees_with_host (the S6 single-witness fact), and the S2 supporting set (minted_token_channels_match_stamp, minted_request_channels_match_stamp, token_stamp_matches_mint). These are well-formedness guards on the model's action labels; the substantive security claim is carried by the corresponding rule design and mutation (for example, MUTATION_Use_Token_Claimed_Community falsifies token_confinement when authorization is rewritten to use a claimed community, MUTATION_Use_Token_ChannelLess_Ignore_Host falsifies channelless_use_confined_to_host_community when the relay reads the token stamp instead of the host binding, and MUTATION_Use_Token_Ignore_Host falsifies channelbearing_use_agrees_with_host when the relay resolves a channel-bearing op from the channel mapping while ignoring the host). Substantive closure requires cross-rule reasoning over persistent-fact invariance (cross_community_mint_yields_no_token_for_that_request, leaked_token_blast_radius_contained, cross_community_use_attempts_are_not_authorized), linear-fact lifecycle (cross_community_audit_splice_attempt_is_not_append), or signed-preimage unification (system_event_acceptance_requires_same_community_key_or_compromise). Tamarin proves both kinds identically; the distinction is for reviewer hygiene, not a weakened theorem claim. This paragraph is prose-only to preserve the .spthy byte hash above.

Implementation Correspondence

The model's obligations map to concrete code seams:

• P-RESOLVE / I2 — resolve(channel_id) must be the only source of ctx.community_id; the h tag is never written into tenancy. Today there is no community layer; channel_id is the only locality.
• P-RESOLVE (immutability) / S2 — channels.community_id must be immutable after insert. No migration may UPDATE channels SET community_id = …, ALTER TABLE channels … community_id …, or drop-and-recreate the column without an explicit re-admission of P-RESOLVE and re-verification of S1/S2. This is the load-bearing assumption behind S2's trace-level mint-rejection (a retag-then- replay breaks it) and behind the TLA ChannelCommunity CONSTANT; it is invisible to both the labeling invariant and the Tamarin lemmas (the proofs would silently weaken, not fail), so it is enforced by a migration lint — the same gate-on-the-migration class as the C2.1 composite-index and C2.4 RelayInfo::build signature lints.
• I1 / I4 — every DB entry point takes TenantContext and SET LOCAL app.community_id; the unscoped get_accessible_channel_ids() (crates/buzz-db/src/channel.rs:545-560, which unions every open channel in the DB) must not exist in any tenant-scoped path. RLS is the backstop.
• C2.1 / A-RLS-5 — the message-uniqueness constraint must be composite over (community_id, …, id), never UNIQUE (id) alone. This is the closure for the existence-oracle (M3 goes red at depth 3 under a global key). It is one bad migration away from breaking and is invisible to the labeling invariant, so it is enforced by the conformance schema assertion (§Conformance: "every unique/FK constraint includes community_id") — the same gate-on-the-migration class as the C2.4 RelayInfo::build signature lint.
• S3 / S4 — the relay keypair becomes a per-community signing key (communities.signing_key), distinct from relay-instance identity; the single global audit chain (crates/buzz-audit/src/service.rs) becomes N per-community chains AuditEntry(community, seq, prev, hash).
• P3 / S2 — the NIP-98 mint freshness obligation the Tamarin model abstracts as a fresh ~time nonce is carried by two code seams: the ±60s window in crates/buzz-auth/src/nip98.rs:77-83 and the event-id seen-set check_nip98_replay in crates/buzz-relay/src/api/bridge.rs:76-94, called before every mint (bridge.rs:181, :254, :514). The seen-set (state.nip98_seen, state.rs:249/:407) is the structural analog of the model's nonce: it makes a replayed mint within the window non-fresh, so the implementation matches the "every mint is structurally unique" world the model proves S2 in. This correspondence is deployment-conditional: today's in-process moka cache carries P3 for the chart default (replicaCount: 1) and for any deployment that routes all mints for the same event id to the same pod, but the shipped HA examples (replicaCount: 3) do not carry P3 as shipped because there is no sticky routing and no shared seen-set. HA conformance requires a Redis/shared-store seen-set with atomic insert-if-absent and TTL ≥ 120 s (recommended), or a header-stable sticky-routing layer — see §Conformance (P3) for the two operator options and the caveats on the routing workaround.
• C2.2 — the client-facing error path must map all DB errors to a fixed sanitized alphabet; no sqlx::Error::to_string() reaches a tenant connection.
• C2.4 — the NIP-11 builder RelayInfo::build (crates/buzz-relay/src/nip11.rs:122) must keep its relay-static-only signature (no &PgPool, no tenant context, no audit service); a signature lint enforces the typed-input fence on the unauthenticated / surface.
• P-RESOLVE-HOST / row-zero conformance — every externally reachable relay-global surface consumes the host-derived TenantContext before reading or mutating tenant data. This is the implementation seam for NIP-11/community relay identity, NIP-98/API-token REST calls, media upload/serve, git Smart HTTP, workflow webhooks/schedules/manual triggers, search, presence, and Redis fan-out. Tokens, signed NIP-98 u URLs, webhook ids, workflow ids, repo names, media hashes, and event ids are subordinate names; none may select a community that disagrees with the request host.
• NIP-11 / S3 — tenant-observable relay identity is per-community. Static software/version fields may be operator-global, but self/relay-signed group, membership, audit, and system events use the community signing key. The unauthenticated info path may reveal facts about the addressed host/community only; unknown hosts fail closed generically rather than returning another community's info document.
• API tokens / P3 — api_tokens is a community-scoped namespace. Token hash lookup, channel claims, scopes, revocation, and NIP-98 replay checks are evaluated under (community_id, token_hash/event_id). HA deployments require a shared atomic seen-set keyed by community and NIP-98 event id, or an explicitly admitted sticky/single-replica deployment; otherwise S2's freshness premise is not carried in production.
• Search / C2.1 — the Postgres FTS index (the events.search_tsv generated column, backed by a GIN index) is shared infrastructure, not a shared result space. Searchable rows carry community_id, and every search query filters by community_id so the FTS predicate is BitmapAnd-ed with the community-leading btree filters; a hit never crosses tenants and refetch by hit id is (community_id, event_id). The channel-less scope (ChannelScope::ChannelLessOnly, formerly the __global__ sentinel) means channel-less within one community, never operator-global.
• Redis / subscription refinement — Redis pub/sub keys, presence keys, typing keys, cache invalidation channels, and local-echo dedup labels include community context in any shared multi-tenant deployment. The safe shape is buzz:{community}:channel:{channel_id}, buzz:{community}:presence:{pubkey}, and buzz:{community}:typing:{channel_id}. The current unprefixed keys are admissible only for the degenerate single-community deployment or physically isolated Redis.
• Media / Blossom — raw blob bytes may remain content-addressed and operator-deduplicated, but descriptors, upload authorization, quotas, audit rows, and any future read policy are community-scoped. A media hash collision or pre-existing blob in another community must not become an existence oracle via metadata, status code, quota accounting, or audit output.
• Git / NIP-34 — git Smart HTTP resolves the repository namespace from the host-derived community before consulting owner/repo names, branch protection, NIP-34 repo announcements, manifests, or object-store pointers. Pointer keys include community (for example repos/{community}/{owner}/{repo}/pointer); pack/object CAS may be shared only below community-scoped refs/manifests and authorization metadata.
• Workflows / system events — workflow definitions, runs, approval hashes, webhook/manual trigger routes, cron scheduling, and relay-signed workflow events inherit community_id. A workflow id or approval token hash alone is never a lookup key. Trigger evaluation sees events in the same community only, and schedule coordination must preserve that label across pods.
• Relay membership / pubkey admission — relay membership, pubkey allowlist, and archived identities are community-global admission facts. The portable value is the pubkey; the stored membership/archive fact is (community_id, pubkey, ...). No deployment-global user gate is tenant-observable unless it is modeled as a separate operator surface. This is no longer asserted-only: the (community_id, pubkey) admission key and the absence of a deployment-global gate are both mechanized. TLA+ carries the allowlist as the admittedMembers relation (MultiTenantRelay.tla:149), keyed on [community, actor]; IsAdmitted(c, a) (:317) gates AddMembership and every channel-less read, and Inv_AdmissionFence proves no membership or channel-less read capability survives that is not same-community-admitted (Theorem I5). The deployment-global gate is exactly mutation M9: replacing IsAdmitted(c, a) with the any-community AdmittedInAnyCommunity(a) (:324) makes the model go red — so admit-into-A-then-act-in-B is a caught escape, not an invisible one. On the authorization side, NIP-43 member-list events are signed and accepted per-community in Tamarin (Community_Signs_NIP43_MemberList / Relay_Accepts_NIP43_MemberList, MultiTenantAuth.spthy:403/:413), and nip43_admission_confined_to_signing_community proves B's signing key can never admit a pubkey into A (Theorem S7).

Subscription-pipeline abstraction

The mechanized models abstract one structural seam: the subscription pipeline (REQ → register → match → fan-out → access-filter → EVENT/EOSE). The TLA+ isolation model represents this pipeline as the synchronous Read* actions, indexed by (worker, actor, community, channel); it has no sub_id, no Register, no Match, no FanOut, no EOSE, no filter state. This is sound — the model proves Inv_LabelPropagation over the aggregate row-set delivered to a B-scoped worker, and the prose observational interface (§The typed observational interface) presents the same property over per-sub streams. The refinement from aggregate to per-stream is coarser than the interface, not wrong — but it is not mechanized, and it is closed here, by code-fence and obligation, against the implementation.

Governing rule. Every observation kind enumerated in §The typed observational interface must either (i) be discharged by a TLA+ invariant or Tamarin lemma, or (ii) appear by name in this subsection with a code-fence and a closure obligation. New observation kinds added to §The typed observational interface require a new entry here in the same commit. This rule is what surfaced F1 (A_HASH closure mis-attribution) and F2 (the subscription-pipeline abstraction itself).

G1 — establishment (crates/buzz-relay/src/handlers/req.rs:79-204)

A REQ from a connection authenticated under pubkey p and token t registers a subscription only after:

1. accessible_channels ← get_accessible_channel_ids_cached(p) (:79) — the DB-derived UUID set the connection's pubkey is a member of.
2. If t carries a channel_ids claim, intersect with it (:88-90). This is the one-token-one-community enforcement at the WS surface.
3. extract_channel_id_from_filters(filters) (:92, body at :795-822) returns Some(uuid) only if every filter pins the same #h=<uuid>; any mixed-#h or missing-#h filter yields None, routing the subscription to the global indexes (tests at :1045-1083).
4. Channel-scoped path: if the returned ch_id ∉ accessible_channels, re-confirm via is_member against the DB (:112); on Ok(false) or Err(_) emit CLOSED "restricted: …" (:127-132).
5. Global path (channel_id = None): per-filter p/engram/author gates must hold against p (:144-167); otherwise CLOSED.
6. Only then is sub_registry.register_scoped(...) called. Direct register calls are confined to test setup; production subscription registration goes through the community-scoped API in req.rs.

G2 — delivery (crates/buzz-relay/src/handlers/event.rs:59-113)

Every candidate from sub_registry.fan_out passes through filter_fanout_by_access before any send_to. The function (:59) and its doc comment (:117-124) state the invariant: a registered subscription is never sufficient for delivery — delivery always revalidates access on the sending pod. Three checks, in order:

• Author-only kinds (:70-83) — filter to recipients whose pubkey_for_conn equals the event author.
• Channel visibility (:85-97) — channel_visibility_cached(channel_id). Non-private → pass through; "private" → continue. Lookup error → return Vec::new() (:91-96): visibility short-circuit, fail-closed for the whole fan-out. The cache discipline at state.rs:560-568 caches only "private", so a stale entry can only over-restrict (≤10s), never leak.
• Membership (:99-111) — is_member_cached(channel_id, pubkey) per recipient; Ok(false) or Err(_) drops that recipient.

Non-mechanized obligations

The following obligations close the per-sub stream properties the TLA+ Inv_LabelPropagation does not reach. Each names its code-fence and the gates (G1, G2) that carry the closure.

1. EOSE cardinality. The count of events preceding O.WS.EOSE(sub_id) must equal |{m ∈ messages : matches(m, F) ∧ m ∈ ResolvedScope(conn)}|, where F is the sub's declared filter set. Delivery: req.rs:281 (per-event EVENT send); EOSE emission: req.rs:292. Closure: G1 admits the subscription only with a ResolvedScope(conn)-consistent filter set, and G2 drops any candidate not in ResolvedScope(conn) at delivery; the EOSE count is therefore the sum of events that passed both gates.
2. EOSE → late-EVENT temporal pairing. No O.WS.EVENT(sub_id, …) delivered after the sub's EOSE may reveal state withheld by G2 during the historical dump. Closure: G2 re-validates visibility and membership on every live fan-out, against the same ResolvedScope(conn) predicate used at EOSE time. The primary closure is the visibility short-circuit at event.rs:91-96 — a transient DB error during the late-EVENT window returns an empty fan-out for the whole event, not a relaxed predicate; the per-recipient membership branch at event.rs:107-110 is the secondary backstop.
3. sub_id reuse and collisions. The sub_id namespace is per-connection, not global. Cross-connection collisions are structurally impossible: SubRegistry.subs is keyed entry(conn_id).or_default().insert(sub_id, …) (subscription.rs:66-69) and every index entry stores (conn_id, sub_id). Same-connection reuse (REQ with sub_id="x" superseding a prior sub_id="x") is closed by subscription.rs::register calling remove_subscription(conn_id, &sub_id) at :64 before re-insert, and by the new subscription re-running G1 against the connection's current ResolvedScope(conn).

Summary

One shared Postgres, one canonical community_id-keyed message log, stateless relay workers, a relational tenant-scoped control plane, and disposable tenant-scoped projections — with isolation stated as label-flow non-interference (TLA+), authorization soundness stated as trace lemmas under a Dolev-Yao adversary (Tamarin), every shared logical channel enumerated and closed, and every invariant mutation-tested. Safety is machine-checkable relative to the RLS, crypto, and resolution axioms, each admitted per deployment by a conformance gate.