{
  "title": "The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.",
  "content": "### Gateway exposure and open gateway misconfiguration\n\n**Claim:** binding beyond loopback without auth can make remote compromise possible / increases exposure; token/password blocks unauth attackers (per the model assumptions).\n\n* Green runs:\n  * `make gateway-exposure-v2`\n  * `make gateway-exposure-v2-protected`\n* Red (expected):\n  * `make gateway-exposure-v2-negative`\n\nSee also: `docs/gateway-exposure-matrix.md` in the models repo.\n\n### Nodes.run pipeline (highest-risk capability)\n\n**Claim:** `nodes.run` requires (a) node command allowlist plus declared commands and (b) live approval when configured; approvals are tokenized to prevent replay (in the model).\n\n* Green runs:\n  * `make nodes-pipeline`\n  * `make approvals-token`\n* Red (expected):\n  * `make nodes-pipeline-negative`\n  * `make approvals-token-negative`\n\n### Pairing store (DM gating)\n\n**Claim:** pairing requests respect TTL and pending-request caps.\n\n* Green runs:\n  * `make pairing`\n  * `make pairing-cap`\n* Red (expected):\n  * `make pairing-negative`\n  * `make pairing-cap-negative`\n\n### Ingress gating (mentions + control-command bypass)\n\n**Claim:** in group contexts requiring mention, an unauthorized “control command” cannot bypass mention gating.\n\n* Green:\n  * `make ingress-gating`\n* Red (expected):\n  * `make ingress-gating-negative`\n\n### Routing/session-key isolation\n\n**Claim:** DMs from distinct peers do not collapse into the same session unless explicitly linked/configured.\n\n* Green:\n  * `make routing-isolation`\n* Red (expected):\n  * `make routing-isolation-negative`\n\n## v1++: additional bounded models (concurrency, retries, trace correctness)\n\nThese are follow-on models that tighten fidelity around real-world failure modes (non-atomic updates, retries, and message fan-out).\n\n### Pairing store concurrency / idempotency\n\n**Claim:** a pairing store should enforce `MaxPending` and idempotency even under interleavings (i.e., “check-then-write” must be atomic / locked; refresh shouldn’t create duplicates).\n\n* Under concurrent requests, you can’t exceed `MaxPending` for a channel.\n\n* Repeated requests/refreshes for the same `(channel, sender)` should not create duplicate live pending rows.\n\n* Green runs:\n  * `make pairing-race` (atomic/locked cap check)\n  * `make pairing-idempotency`\n  * `make pairing-refresh`\n  * `make pairing-refresh-race`\n\n* Red (expected):\n  * `make pairing-race-negative` (non-atomic begin/commit cap race)\n  * `make pairing-idempotency-negative`\n  * `make pairing-refresh-negative`\n  * `make pairing-refresh-race-negative`\n\n### Ingress trace correlation / idempotency\n\n**Claim:** ingestion should preserve trace correlation across fan-out and be idempotent under provider retries.\n\n* When one external event becomes multiple internal messages, every part keeps the same trace/event identity.\n\n* Retries do not result in double-processing.\n\n* If provider event IDs are missing, dedupe falls back to a safe key (e.g., trace ID) to avoid dropping distinct events.\n\n* Green:\n  * `make ingress-trace`\n  * `make ingress-trace2`\n  * `make ingress-idempotency`\n  * `make ingress-dedupe-fallback`\n\n* Red (expected):\n  * `make ingress-trace-negative`\n  * `make ingress-trace2-negative`\n  * `make ingress-idempotency-negative`\n  * `make ingress-dedupe-fallback-negative`\n\n### Routing dmScope precedence + identityLinks\n\n**Claim:** routing must keep DM sessions isolated by default, and only collapse sessions when explicitly configured (channel precedence + identity links).\n\n* Channel-specific dmScope overrides must win over global defaults.\n\n* identityLinks should collapse only within explicit linked groups, not across unrelated peers.\n\n* Green:\n  * `make routing-precedence`\n  * `make routing-identitylinks`\n\n* Red (expected):\n  * `make routing-precedence-negative`\n  * `make routing-identitylinks-negative`",
  "code_samples": [],
  "headings": [
    {
      "level": "h3",
      "text": "Gateway exposure and open gateway misconfiguration",
      "id": "gateway-exposure-and-open-gateway-misconfiguration"
    },
    {
      "level": "h3",
      "text": "Nodes.run pipeline (highest-risk capability)",
      "id": "nodes.run-pipeline-(highest-risk-capability)"
    },
    {
      "level": "h3",
      "text": "Pairing store (DM gating)",
      "id": "pairing-store-(dm-gating)"
    },
    {
      "level": "h3",
      "text": "Ingress gating (mentions + control-command bypass)",
      "id": "ingress-gating-(mentions-+-control-command-bypass)"
    },
    {
      "level": "h3",
      "text": "Routing/session-key isolation",
      "id": "routing/session-key-isolation"
    },
    {
      "level": "h2",
      "text": "v1++: additional bounded models (concurrency, retries, trace correctness)",
      "id": "v1++:-additional-bounded-models-(concurrency,-retries,-trace-correctness)"
    },
    {
      "level": "h3",
      "text": "Pairing store concurrency / idempotency",
      "id": "pairing-store-concurrency-/-idempotency"
    },
    {
      "level": "h3",
      "text": "Ingress trace correlation / idempotency",
      "id": "ingress-trace-correlation-/-idempotency"
    },
    {
      "level": "h3",
      "text": "Routing dmScope precedence + identityLinks",
      "id": "routing-dmscope-precedence-+-identitylinks"
    }
  ],
  "url": "llms-txt#the-repo-vendors-a-pinned-`tla2tools.jar`-(tla+-tools)-and-provides-`bin/tlc`-+-make-targets.",
  "links": []
}