refactor(spec): clean prose patterns across all modules

Remove filler/redundant patterns: 钉死/钉, 本模块, likec4 画不出/画得出,
臆造, 散文, 分歧点测试, 纯 plumbing, 恰好, 留白, 宪法第N条, 刻意.
No code definitions changed, only doc comments.

.gitignore

@@ -11,6 +11,9 @@
 # regenerable, not for VCS. The embedded engine mounts cph-render directly.
 render/vendor/local-packages/
 
+# Environment
+.env
+
 # Node (hub/ TS workspace and any future JS package)
 node_modules/
 

docs/para-26071100-feishu-setup.md

@@ -99,7 +99,7 @@ https://example-school.educraft.paradigm-edu.net/auth/feishu/callback
 
 必须使用 Educraft 部署人员最终确认的 slug；不要直接照抄示例。该 URL 用于 OAuth 返回并创建应用作用域下的飞书用户身份，不代表当前已经开放组织管理台。
 
-身份登录和组织成员资格是两件事：OAuth 登录只建立用户身份；当前 Alpha 阶段，Educraft 部署人员还需要通过受控管理命令把该用户加入组织。首位 OWNER 在 bootstrap 时由部署人员完成，其他试点成员按需人工加入。
+组织专属 OAuth 同时完成身份建立和入组：首次成功登录的用户会自动成为当前 Organization 的 `MEMBER`，回到群聊即可使用。`OWNER` 和 `ADMIN` 仍只能由部署人员或管理员显式授予；曾被移除的成员重新登录不会自动恢复资格。
 
 ## 6. 发布并安装应用
 
@@ -203,7 +203,7 @@ Educraft 部署人员收到信息后，会回传最终 organization slug、访
 1. OWNER 在试点群中 @机器人发送一条纯文本消息。
 2. 如果群尚未绑定项目，确认机器人返回项目创建/绑定卡片。
 3. 创建项目后再次 @机器人，确认出现处理状态、流式卡片和最终回答。
-4. 选择一位非 OWNER 试点成员完成 OAuth 登录，并由部署人员加入组织。
+4. 选择一位非 OWNER 试点成员完成 OAuth 登录，确认其自动以 MEMBER 身份加入组织。
 5. 该成员在同一群中 @机器人，确认能够进入已绑定项目。
 6. 测试一个小文件附件、一次运行中断，以及一个需要生成文档的任务。
 
@@ -215,5 +215,5 @@ Educraft 部署人员收到信息后，会回传最终 organization slug、访
 - 组织的 role、system prompt、tools 和 skills 是运行时配置，不需要跟随版本发布。
 - 同一项目同一时间只执行一个任务，避免并发修改同一个 workspace；组织级并发上限由部署配置决定。
 - 当前由 Educraft 人工创建组织、OWNER、Provider Connection 和初始 Team，并通过服务器上的受控管理命令运维；组织管理台尚未开放。
-- 非 OWNER 试点成员需要先完成飞书 OAuth 身份建立，再由 Educraft 部署人员人工加入组织；当前没有自助入组织入口。
+- 非 OWNER 试点成员通过组织专属 OAuth 首次登录后自动成为 MEMBER；OWNER/ADMIN 提权和被移除成员的恢复仍需人工操作。
 - Alpha 不提供开放注册、自助密钥管理或跨组织资源共享。

hub/deploy/NEW_SILO_RUNBOOK.md

@@ -0,0 +1,133 @@
+# New Alpha Silo runbook
+
+Use this runbook for a new Organization. A Silo is not merely another row in
+the existing database: it has an independent PostgreSQL role/database, Linux
+service identity, systemd unit, secret directory/keyring, workspace, skill
+store, loopback port, domain, Feishu app and provider credential.
+
+The repeatable entry point is:
+
+```sh
+bash hub/deploy/new_silo.sh
+```
+
+After collecting the Organization inputs, the wizard shows the assigned
+resources and asks once before applying them directly over SSH. The generated
+bundle is only a root-secret-safe retry and audit checkpoint; the operator does
+not execute it manually during the normal path.
+
+It gathers values and writes a private deployment bundle below
+`~/.cph-silo-plans/<instance-id>/`. The directory and all generated files are
+mode `0700`/`0600`. Never commit, paste into chat, or copy that directory into
+an immutable release. Run the wizard once per Organization; do not edit a copy
+from another Organization.
+
+## Inputs to collect
+
+The wizard derives the instance/Organization id from the slug, uses the current
+release and managed Alpha defaults, connects to the managed host (currently
+`39.107.254.4`), derives
+`https://<organization-slug>.educraft.paradigm-edu.net` from the wildcard DNS,
+and allocates an unused loopback port plus short workspace path by inspecting
+existing Silo environments, listening sockets and workspace paths over
+read-only SSH. The Organization administrator supplies:
+
+- Organization display name and slug;
+- Feishu App ID and App Secret (the wizard resolves the bot Open ID);
+- the first OWNER's Open ID and display name;
+- an Organization-exclusive OpenRouter token.
+
+Everything else is platform-managed or derived: instance/Organization id,
+server, SSH settings, release, resource ceilings, database coordinates and
+generated password, domain, port, workspace, provider/base URL, model/role,
+curated skills, concurrency, request/file limits and the managed Mihomo proxy
+environment. `NODE_USE_ENV_PROXY=1` is required on Node.js 24 so Hub's built-in
+`fetch` actually uses that proxy; merely setting `HTTP_PROXY`/`HTTPS_PROXY` is
+not sufficient.
+
+The Feishu app is scoped to this Silo. OAuth users authenticated by that app are
+automatically admitted to this Organization; OWNER remains the initial
+privileged membership used for controlled administration and bootstrap. An
+empty initial team list does not block the Alpha.
+
+To target a replacement platform-managed host, the platform operator may set
+`CPH_ALPHA_HOST`, `CPH_ALPHA_DEPLOY_USER`, `CPH_ALPHA_SSH_PORT` and
+`CPH_ALPHA_BASE_DOMAIN` before running the wizard. These are fleet controls,
+not Organization setup questions.
+
+Obtain a person's Open ID from the Feishu user-get documentation page by
+clicking the `user_id` value picker and selecting the person. Configure the
+redirect URL shown by the generated `OPERATE.md`; it is required for first-time
+OAuth admission.
+
+## Host prerequisites
+
+Before the first Silo on a host, install Node.js 24+, npm, rsync, PostgreSQL
+server/client, `pg_isready`, systemd, bubblewrap, socat, `runuser`, `setpriv`,
+`pg_dump`, tar, sha256sum, Nginx, Certbot, Typst and a compatible `cph` binary.
+Configure outbound proxying independently at host/service level and verify both
+GitHub and the selected model provider through it. The wizard does not install
+or select proxy nodes.
+
+Use a deployment account with only the required passwordless sudo operations.
+The application itself always runs as the installer-created non-root
+`cph-<instance-id>` user. PostgreSQL must have a separate login role and logical
+database per Silo even when all Silo databases share one PostgreSQL server.
+
+## Execute a generated bundle
+
+Open the bundle's `OPERATE.md` and perform its numbered gates in order:
+
+1. DNS, Feishu redirect URL, permissions and event subscription.
+2. Dedicated PostgreSQL role and database.
+3. Immutable release publication. Exit 78 is expected only when the first
+   installer call seeds this instance's keyring and environment template.
+4. Root-owned secret installation and off-host keyring recovery copy.
+5. Prisma migration, stopped service installation and idempotent bootstrap.
+6. Explicit runtime role/skill installation.
+7. Nginx/TLS, service start, internal/external health and Feishu acceptance.
+8. First off-host backup.
+
+Every command must fail fast. Do not add `|| true` around install, migration,
+bootstrap, Nginx validation, health, or backup checks. If a check fails, retain
+the unit logs and the exact failed stage before changing configuration.
+
+## Default runtime role and skills
+
+Roles and skills are dynamic Silo state, not release contents. The release
+contains only the management CLI. Stage approved skill directories on the host
+and install them with `agent_config.sh`; PostgreSQL records role definitions and
+skill selections while the versioned skill content lives in the Silo state
+directory and is included in backups.
+
+For the current Alpha, upsert the default role with the agreed education
+assistant system prompt, model selection, tools policy and approved skill list.
+Keep the prompt in a root-controlled staging file, pass it via
+`--system-prompt-file`, then verify with `agent_config.sh list`. Do not sync an
+operator's entire personal skill directory: each enabled skill must be reviewed
+and named explicitly. Typst being installed on the host and the Typst skill
+being enabled are separate gates.
+
+## Acceptance gate
+
+A Silo is ready only when all of the following pass:
+
+- its systemd service is active and both loopback and TLS health endpoints pass;
+- startup preflight sees exactly the configured Organization plus active Feishu
+  and provider connections;
+- OWNER completes OAuth and can interact with the bot;
+- a non-OWNER completes OAuth and can interact with the same app/Organization;
+- two Feishu groups bind distinct projects/sessions;
+- a restart preserves persisted session cursor behavior;
+- the configured provider/model succeeds through the host proxy;
+- every enabled skill is listed, and a Typst task succeeds if Typst is enabled;
+- the first business backup and separate recovery backup are stored off-host.
+
+## Rollback boundary
+
+For a failed code release, point only this instance back to the previous
+immutable release and rerun its installer with the same instance parameters.
+Do not roll back a database after migrations unless that release's documented
+database compatibility permits it. Preserve the environment, keyring, database,
+workspace and skill store. For destructive recovery, stop traffic and use the
+separate restore procedure; never substitute another Silo's state.

hub/deploy/README.md

@@ -1,5 +1,16 @@
 # Alpha Silo service installation
 
+For a brand-new Organization, start with the repeatable wizard and end-to-end
+operator runbook:
+
+```sh
+bash hub/deploy/new_silo.sh
+```
+
+See [NEW_SILO_RUNBOOK.md](NEW_SILO_RUNBOOK.md). The remainder of this document
+describes the individual installer and maintenance primitives used by the
+generated bundle.
+
 The supervised alpha runs one Organization per named Silo. The supported host
 has systemd, PostgreSQL, Node.js 24+, `pg_isready`, `runuser`, `setpriv`,
 bubblewrap, `socat`, `pg_dump`, `tar`, `sha256sum`, and a compatible `cph`.

hub/deploy/apply_new_silo.sh

@@ -0,0 +1,73 @@
+#!/usr/bin/env bash
+# Apply a bundle produced by new_silo.sh to the managed Alpha host.
+set -euo pipefail
+
+BUNDLE="${1:?usage: apply_new_silo.sh BUNDLE_DIR}"
+ANSWERS="$BUNDLE/answers.env"
+[ -f "$ANSWERS" ] || { echo "missing $ANSWERS" >&2; exit 1; }
+
+value() { sed -n "s/^$1=//p" "$ANSWERS" | tail -n1; }
+INSTANCE_ID="$(value INSTANCE_ID)"
+ORG_ID="$(value ORGANIZATION_ID)"
+HOST="$(value DEPLOY_HOST)"
+SSH_USER="$(value DEPLOY_USER)"
+SSH_PORT="$(value DEPLOY_SSH_PORT)"
+SSH_KEY="$(value DEPLOY_SSH_KEY)"
+BASE="$(value DEPLOY_BASE)"
+RELEASE="$(value RELEASE_ID)"
+HUB_PORT="$(value HUB_PORT)"
+WORKSPACE="$(value WORKSPACE_ROOT)"
+MEMORY="$(value MEMORY_MAX)"
+CPU="$(value CPU_QUOTA)"
+TASKS="$(value TASKS_MAX)"
+DB_NAME="$(value DATABASE_NAME)"
+DB_USER="$(value DATABASE_USER)"
+DB_PASSWORD="$(value DATABASE_PASSWORD)"
+PUBLIC_URL="$(value PUBLIC_BASE_URL)"
+DOMAIN="${PUBLIC_URL#https://}"
+HUB_DIR="$BASE/releases/$RELEASE/hub"
+ENV_PATH="$BASE/.secrets/$INSTANCE_ID/platform.env"
+KEYRING_PATH="$BASE/.secrets/$INSTANCE_ID/secret-keyring.json"
+UNIT="cph-hub-$INSTANCE_ID.service"
+SSH=(ssh -i "$SSH_KEY" -p "$SSH_PORT" -o BatchMode=yes "$SSH_USER@$HOST")
+SCP=(scp -i "$SSH_KEY" -P "$SSH_PORT")
+
+for file in platform.env bootstrap.json default-role-prompt.md; do
+  [ -f "$BUNDLE/$file" ] || { echo "missing bundle file: $file" >&2; exit 1; }
+done
+
+echo "[1/8] Verify immutable release"
+"${SSH[@]}" "test -f '$BASE/releases/$RELEASE/.complete'"
+
+echo "[2/8] Create dedicated database"
+if ! "${SSH[@]}" "sudo -u postgres psql -Atqc \"select 1 from pg_database where datname='$DB_NAME'\"" | grep -qx 1; then
+  printf "CREATE ROLE %s LOGIN PASSWORD '%s';\nCREATE DATABASE %s OWNER %s;\n" \
+    "$DB_USER" "$DB_PASSWORD" "$DB_NAME" "$DB_USER" | "${SSH[@]}" sudo -u postgres psql -v ON_ERROR_STOP=1
+fi
+
+echo "[3/8] Seed instance keyring and service template"
+set +e
+"${SSH[@]}" "BASE='$BASE' HUB_DIR='$HUB_DIR' INSTANCE_ID='$INSTANCE_ID' WORKSPACE_ROOT='$WORKSPACE' PORT='$HUB_PORT' MEMORY_MAX='$MEMORY' CPU_QUOTA='$CPU' TASKS_MAX='$TASKS' bash '$HUB_DIR/deploy/install_service.sh'"
+status=$?
+set -e
+[ "$status" -eq 0 ] || [ "$status" -eq 78 ] || exit "$status"
+
+echo "[4/8] Upload root-only configuration"
+remote_stage="/root/.cph-bootstrap-$INSTANCE_ID"
+"${SSH[@]}" "install -d -o root -g root -m 0700 '$remote_stage'"
+"${SCP[@]}" "$BUNDLE/platform.env" "$BUNDLE/bootstrap.json" "$BUNDLE/default-role-prompt.md" "$SSH_USER@$HOST:$remote_stage/"
+"${SSH[@]}" "install -o root -g root -m 0600 '$remote_stage/platform.env' '$ENV_PATH'; chmod 0600 '$remote_stage/bootstrap.json' '$remote_stage/default-role-prompt.md'"
+
+echo "[5/8] Migrate, install, and bootstrap"
+"${SSH[@]}" "set -euo pipefail; set -a; . '$ENV_PATH'; set +a; node '$HUB_DIR/node_modules/prisma/build/index.js' migrate deploy --schema '$HUB_DIR/prisma/schema.prisma'; BASE='$BASE' HUB_DIR='$HUB_DIR' INSTANCE_ID='$INSTANCE_ID' WORKSPACE_ROOT='$WORKSPACE' PORT='$HUB_PORT' MEMORY_MAX='$MEMORY' CPU_QUOTA='$CPU' TASKS_MAX='$TASKS' bash '$HUB_DIR/deploy/install_service.sh'; node '$HUB_DIR/dist/deployment/bootstrap-silo-cli.js' --config-file '$remote_stage/bootstrap.json' --keyring-file '$KEYRING_PATH'"
+
+echo "[6/8] Copy curated skills and configure default role"
+"${SSH[@]}" "set -euo pipefail; stage='/var/lib/cph-hub/$INSTANCE_ID/state/operator-staging'; install -d -o cph-$INSTANCE_ID -g cph-$INSTANCE_ID -m 0700 \"\$stage/skills\"; install -o cph-$INSTANCE_ID -g cph-$INSTANCE_ID -m 0600 '$remote_stage/default-role-prompt.md' \"\$stage/default-role-prompt.md\"; for source in /var/lib/cph-hub/para-26071100/state/skills/versions/*; do name=\$(sed -n 's/^name: *//p' \"\$source/SKILL.md\" | head -n1); case \"\$name\" in outline|lesson-project|data-processing-spec|typst) cp -a \"\$source\" \"\$stage/skills/\$name\"; chown -R cph-$INSTANCE_ID:cph-$INSTANCE_ID \"\$stage/skills/\$name\";; esac; done; for name in outline lesson-project data-processing-spec typst; do INSTANCE_ID='$INSTANCE_ID' ENV_FILE='$ENV_PATH' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/agent_config.sh' install-skill --organization '$ORG_ID' --source \"\$stage/skills/\$name\" --version 1; done; INSTANCE_ID='$INSTANCE_ID' ENV_FILE='$ENV_PATH' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/agent_config.sh' upsert-role --organization '$ORG_ID' --role draft --label '智能助手' --system-prompt-file \"\$stage/default-role-prompt.md\" --tools-json null; INSTANCE_ID='$INSTANCE_ID' ENV_FILE='$ENV_PATH' HUB_DIR='$HUB_DIR' bash '$HUB_DIR/deploy/agent_config.sh' set-role-skills --organization '$ORG_ID' --role draft --skills outline,lesson-project,data-processing-spec,typst; rm -rf \"\$stage\""
+
+echo "[7/8] Configure Nginx and TLS"
+printf 'server { listen 80; listen [::]:80; server_name %s; client_max_body_size 2m; location / { proxy_pass http://127.0.0.1:%s; proxy_http_version 1.1; proxy_set_header Host $host; proxy_set_header X-Real-IP $remote_addr; proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for; proxy_set_header X-Forwarded-Proto $scheme; proxy_set_header Upgrade $http_upgrade; proxy_set_header Connection $connection_upgrade; proxy_read_timeout 3600s; proxy_send_timeout 3600s; proxy_buffering off; } }\n' "$DOMAIN" "$HUB_PORT" | "${SSH[@]}" "install -o root -g root -m 0644 /dev/stdin '/etc/nginx/sites-available/$INSTANCE_ID'; ln -sfn '/etc/nginx/sites-available/$INSTANCE_ID' '/etc/nginx/sites-enabled/$INSTANCE_ID'; nginx -t; systemctl reload nginx; certbot --nginx --non-interactive --agree-tos --redirect --register-unsafely-without-email -d '$DOMAIN'"
+
+echo "[8/8] Start and verify"
+"${SSH[@]}" "systemctl enable --now '$UNIT'; systemctl is-active --quiet '$UNIT'; curl --fail --silent 'http://127.0.0.1:$HUB_PORT/api/healthz' >/dev/null; rm -f '$remote_stage/bootstrap.json'"
+curl --fail --silent --show-error "$PUBLIC_URL/api/healthz" >/dev/null
+echo "Deployed $INSTANCE_ID at $PUBLIC_URL"

hub/deploy/new_silo.sh

@@ -0,0 +1,412 @@
+#!/usr/bin/env bash
+#
+# A wizard — walks a human through a manual procedure step by step.
+# Generated by the /wizard skill.
+#
+# Everything above the "STAGES" marker is the wizard library: do not hand-edit
+# it. Author the per-step stages below the marker.
+
+set -euo pipefail
+
+# ──────────────────────────────────────────────────────────────────────────
+# Wizard library — delightful, consistent UX. Identical across every wizard.
+# ──────────────────────────────────────────────────────────────────────────
+
+if [[ -t 1 ]] && command -v tput >/dev/null 2>&1 && [[ "$(tput colors 2>/dev/null || echo 0)" -ge 8 ]]; then
+  BOLD=$(tput bold); DIM=$(tput dim); RESET=$(tput sgr0)
+  BLUE=$(tput setaf 4); GREEN=$(tput setaf 2); YELLOW=$(tput setaf 3); RED=$(tput setaf 1)
+else
+  BOLD=""; DIM=""; RESET=""; BLUE=""; GREEN=""; YELLOW=""; RED=""
+fi
+
+# Author sets these two at the top of the stages section.
+TOTAL_STAGES=0
+TOTAL_MINUTES=0
+
+_STAGE_INDEX=0
+_MINUTES_ELAPSED=0
+ENV_FILE="${ENV_FILE:-.env}"
+WRITTEN_ENV=()    # KEYs written to ENV_FILE this run
+WRITTEN_SECRET=() # secret NAMEs set this run
+SKIPPED=()        # things we couldn't do (e.g. gh missing)
+
+# _clear — wipe the terminal so only the current step is on screen. No-op when
+# output isn't a terminal, so piped logs stay readable.
+_clear() {
+  [[ -t 1 ]] || return 0
+  if command -v tput >/dev/null 2>&1; then tput clear; else printf '\033[2J\033[3J\033[H'; fi
+}
+
+# banner "Title" — opening frame: what this wizard does and how long it takes.
+banner() {
+  _clear
+  printf '\n%s%s  %s%s\n' "$BOLD" "$BLUE" "$1" "$RESET"
+  printf '%s  %s stages · about %s minutes%s\n\n' \
+    "$DIM" "$TOTAL_STAGES" "$TOTAL_MINUTES" "$RESET"
+  printf '%s  You drive the browser; this wizard tells you exactly what to do and\n' "$DIM"
+  printf '  captures the values you copy back. Stop any time with Ctrl-C and re-run\n'
+  printf '  later — it remembers values already saved.%s\n' "$RESET"
+  pause "Ready to start?"
+}
+
+# stage "Name" <minutes> — clear the screen, then announce a stage and show
+# progress + time remaining. Clearing keeps only the current step on screen.
+stage() {
+  _clear
+  _STAGE_INDEX=$((_STAGE_INDEX + 1))
+  local remaining=$((TOTAL_MINUTES - _MINUTES_ELAPSED))
+  (( remaining < 0 )) && remaining=0
+  _MINUTES_ELAPSED=$((_MINUTES_ELAPSED + ${2:-0}))
+  printf '\n%s%s▸ Stage %s/%s · %s%s  %s(~%s min left)%s\n' \
+    "$BOLD" "$BLUE" "$_STAGE_INDEX" "$TOTAL_STAGES" "$1" "$RESET" "$DIM" "$remaining" "$RESET"
+}
+
+# say "..." — a plain instruction line.
+say()  { printf '  %s\n' "$1"; }
+# step "..." — a numbered-feeling action the human takes in the browser.
+step() { printf '  %s•%s %s\n' "$BLUE" "$RESET" "$1"; }
+note() { printf '  %s%s%s\n' "$DIM" "$1" "$RESET"; }
+warn() { printf '  %s⚠ %s%s\n' "$YELLOW" "$1" "$RESET"; }
+
+# open_url URL — open in the human's browser, cross-platform incl. WSL.
+open_url() {
+  local url="$1"
+  printf '  %s↗ opening%s %s\n' "$GREEN" "$RESET" "$url"
+  { if   command -v wslview     >/dev/null 2>&1; then wslview "$url"
+    elif command -v explorer.exe >/dev/null 2>&1; then explorer.exe "$url"
+    elif command -v xdg-open    >/dev/null 2>&1; then xdg-open "$url"
+    elif command -v open        >/dev/null 2>&1; then open "$url"
+    else warn "couldn't open a browser — visit it manually: $url"; fi
+  } >/dev/null 2>&1 || warn "couldn't open a browser — visit it manually: $url"
+}
+
+# pause "msg" — wait for the human to confirm they've done the manual part.
+pause() {
+  printf '  %s%s%s ' "$DIM" "${1:-Press Enter to continue}" "$RESET"
+  read -r _ || true
+}
+
+# confirm "question" — y/N gate; returns success on yes.
+confirm() {
+  local reply=""
+  printf '  %s? %s [y/N] ' "$YELLOW" "$1"
+  read -r reply || true
+  [[ "$reply" =~ ^[Yy] ]]
+}
+
+# _existing KEY — current value of KEY in ENV_FILE, if any.
+_existing() {
+  [[ -f "$ENV_FILE" ]] || return 1
+  local line; line=$(grep -E "^${1}=" "$ENV_FILE" | tail -n1) || return 1
+  printf '%s' "${line#*=}"
+}
+
+# ask KEY "Prompt" — read a value into $KEY. Offers the existing .env value as
+# a default on re-runs (Enter keeps it). Visible input (non-secret).
+ask() {
+  local key="$1" prompt="$2" current input
+  current=$(_existing "$key" || true)
+  if [[ -n "$current" ]]; then
+    printf '  %s%s%s %s[Enter keeps current]%s ' "$BOLD" "$prompt" "$RESET" "$DIM" "$RESET"
+  else
+    printf '  %s%s%s ' "$BOLD" "$prompt" "$RESET"
+  fi
+  read -r input || true
+  [[ -z "$input" && -n "$current" ]] && input="$current"
+  printf -v "$key" '%s' "$input"
+}
+
+# ask_secret KEY "Prompt" — like ask, but input is hidden.
+ask_secret() {
+  local key="$1" prompt="$2" current input
+  current=$(_existing "$key" || true)
+  if [[ -n "$current" ]]; then
+    printf '  %s%s%s %s[Enter keeps current]%s ' "$BOLD" "$prompt" "$RESET" "$DIM" "$RESET"
+  else
+    printf '  %s%s%s ' "$BOLD" "$prompt" "$RESET"
+  fi
+  read -rs input || true
+  printf '\n'
+  [[ -z "$input" && -n "$current" ]] && input="$current"
+  printf -v "$key" '%s' "$input"
+}
+
+# write_env KEY VALUE — upsert KEY=VALUE into ENV_FILE (creates it; replaces
+# any existing line). Idempotent.
+write_env() {
+  local key="$1" value="$2" tmp
+  touch "$ENV_FILE"
+  tmp=$(mktemp)
+  grep -vE "^${key}=" "$ENV_FILE" > "$tmp" || true
+  printf '%s=%s\n' "$key" "$value" >> "$tmp"
+  mv "$tmp" "$ENV_FILE"
+  WRITTEN_ENV+=("$key")
+  printf '  %s✓ wrote%s %s → %s\n' "$GREEN" "$RESET" "$key" "$ENV_FILE"
+}
+
+# set_secret NAME VALUE — set a GitHub Actions repo secret via gh. Falls back
+# to a warning (and records it) if gh is unavailable or unauthenticated.
+set_secret() {
+  local name="$1" value="$2"
+  if command -v gh >/dev/null 2>&1 && gh auth status >/dev/null 2>&1; then
+    if printf '%s' "$value" | gh secret set "$name" >/dev/null 2>&1; then
+      WRITTEN_SECRET+=("$name")
+      printf '  %s✓ set%s GitHub secret %s\n' "$GREEN" "$RESET" "$name"
+      return
+    fi
+  fi
+  SKIPPED+=("GitHub secret $name (set it manually: gh secret set $name)")
+  warn "skipped GitHub secret $name — gh not ready; set it later"
+}
+
+# set_var NAME VALUE — set a GitHub Actions repo variable (non-secret).
+set_var() {
+  local name="$1" value="$2"
+  if command -v gh >/dev/null 2>&1 && gh auth status >/dev/null 2>&1; then
+    if gh variable set "$name" --body "$value" >/dev/null 2>&1; then
+      printf '  %s✓ set%s GitHub variable %s\n' "$GREEN" "$RESET" "$name"
+      return
+    fi
+  fi
+  SKIPPED+=("GitHub variable $name")
+  warn "skipped GitHub variable $name — gh not ready; set it later"
+}
+
+# finish — clear, then a closing summary of everything configured.
+finish() {
+  _clear
+  printf '\n%s%s  ✓ Setup complete%s\n' "$BOLD" "$GREEN" "$RESET"
+  (( ${#WRITTEN_ENV[@]} ))    && note "wrote ${#WRITTEN_ENV[@]} value(s) to $ENV_FILE: ${WRITTEN_ENV[*]}"
+  (( ${#WRITTEN_SECRET[@]} )) && note "set ${#WRITTEN_SECRET[@]} GitHub secret(s): ${WRITTEN_SECRET[*]}"
+  if (( ${#SKIPPED[@]} )); then
+    printf '\n'; warn "still to do by hand:"
+    for s in "${SKIPPED[@]}"; do note "  - $s"; done
+  fi
+  printf '\n'
+}
+
+# ──────────────────────────────────────────────────────────────────────────
+# STAGES — author this section. One stage() per step the human takes.
+# Replace the example below. Set the two totals to match the stages you write.
+# ──────────────────────────────────────────────────────────────────────────
+
+TOTAL_STAGES=7
+TOTAL_MINUTES=35
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+REPO_ROOT="$(cd "$SCRIPT_DIR/../.." && pwd)"
+PLAN_ROOT="${CPH_SILO_PLAN_ROOT:-$HOME/.cph-silo-plans}"
+umask 077
+
+require_value() {
+  local key="$1" value="$2"
+  [[ -n "$value" ]] || { warn "$key is required"; exit 1; }
+  [[ "$value" != *$'\n'* && "$value" != *$'\r'* ]] || {
+    warn "$key must be a single line"
+    exit 1
+  }
+}
+
+seed_default() {
+  local key="$1" value="$2"
+  _existing "$key" >/dev/null 2>&1 || write_env "$key" "$value"
+}
+
+capture() {
+  local key="$1" prompt="$2"
+  ask "$key" "$prompt"
+  require_value "$key" "${!key}"
+  write_env "$key" "${!key}"
+}
+
+capture_secret() {
+  local key="$1" prompt="$2"
+  ask_secret "$key" "$prompt"
+  require_value "$key" "${!key}"
+  write_env "$key" "${!key}"
+}
+
+allocate_host_slot() {
+  local allocation local_reserved="" answers_file reserved_port
+  for answers_file in "$PLAN_ROOT"/*/answers.env; do
+    [ -f "$answers_file" ] || continue
+    reserved_port="$(sed -n 's/^HUB_PORT=//p' "$answers_file" | tail -n1)"
+    [[ "$reserved_port" =~ ^[0-9]+$ ]] || continue
+    local_reserved="${local_reserved:+$local_reserved,}$reserved_port"
+  done
+  allocation="$(ssh \
+    -i "$DEPLOY_SSH_KEY" \
+    -p "$DEPLOY_SSH_PORT" \
+    -o BatchMode=yes \
+    -o StrictHostKeyChecking=accept-new \
+    "$DEPLOY_USER@$DEPLOY_HOST" \
+    bash -s -- "$local_reserved" <<'REMOTE'
+      set -euo pipefail
+      local_reserved=",${1:-},"
+      for candidate in $(seq 8788 8999); do
+        reserved=false
+        if [[ "$local_reserved" == *",$candidate,"* ]]; then
+          continue
+        fi
+        for env_file in /srv/curriculum-project-hub/.secrets/*/platform.env; do
+          [ -f "$env_file" ] || continue
+          if [ "$(sed -n "s/^PORT=//p" "$env_file")" = "$candidate" ]; then
+            reserved=true
+            break
+          fi
+        done
+        workspace="/w/$candidate"
+        if [ "$reserved" = false ] && ! ss -H -ltn "sport = :$candidate" | grep -q . && [ ! -e "$workspace" ]; then
+          printf "%s %s\n" "$candidate" "$workspace"
+          exit 0
+        fi
+      done
+      echo "no free Alpha Silo slot in 8788..8999" >&2
+      exit 1
+REMOTE
+  )"
+  read -r HUB_PORT WORKSPACE_ROOT <<<"$allocation"
+  require_value HUB_PORT "$HUB_PORT"
+  require_value WORKSPACE_ROOT "$WORKSPACE_ROOT"
+  write_env HUB_PORT "$HUB_PORT"
+  write_env WORKSPACE_ROOT "$WORKSPACE_ROOT"
+}
+
+banner "New Alpha Silo"
+
+stage "Organization identity and private plan" 3
+say "One run creates one Organization's private deployment bundle."
+ask ORGANIZATION_SLUG "Organization slug (lowercase, max 24 chars; e.g. school-a):"
+require_value ORGANIZATION_SLUG "$ORGANIZATION_SLUG"
+[[ "$ORGANIZATION_SLUG" =~ ^[a-z0-9]([a-z0-9-]{0,22}[a-z0-9])?$ ]] || {
+  warn "invalid Organization slug"
+  exit 1
+}
+INSTANCE_ID="$ORGANIZATION_SLUG"
+ORGANIZATION_ID="$ORGANIZATION_SLUG"
+OUTPUT_DIR="$PLAN_ROOT/$INSTANCE_ID"
+mkdir -p "$OUTPUT_DIR"
+chmod 0700 "$OUTPUT_DIR"
+ENV_FILE="$OUTPUT_DIR/answers.env"
+touch "$ENV_FILE"
+chmod 0600 "$ENV_FILE"
+write_env INSTANCE_ID "$INSTANCE_ID"
+write_env ORGANIZATION_ID "$ORGANIZATION_ID"
+write_env ORGANIZATION_SLUG "$ORGANIZATION_SLUG"
+capture ORGANIZATION_NAME "Organization display name:"
+
+stage "Host, release, and isolation" 5
+say "The Alpha host is platform-managed. Port and short workspace path are allocated from live host state."
+DEPLOY_HOST="${CPH_ALPHA_HOST:-39.107.254.4}"
+DEPLOY_USER="${CPH_ALPHA_DEPLOY_USER:-root}"
+DEPLOY_SSH_PORT="${CPH_ALPHA_SSH_PORT:-22}"
+write_env DEPLOY_HOST "$DEPLOY_HOST"
+write_env DEPLOY_USER "$DEPLOY_USER"
+write_env DEPLOY_SSH_PORT "$DEPLOY_SSH_PORT"
+seed_default DEPLOY_BASE "/srv/curriculum-project-hub"
+seed_default DEPLOY_SSH_KEY "$HOME/.ssh/id_ed25519"
+write_env RELEASE_ID "v$(node -p 'require(process.argv[1]).version' "$REPO_ROOT/hub/package.json")"
+seed_default MEMORY_MAX "16G"
+seed_default CPU_QUOTA "400%"
+seed_default TASKS_MAX "512"
+seed_default CPH_BIN "/usr/local/bin/cph"
+note "Managed Alpha host: $DEPLOY_USER@$DEPLOY_HOST:$DEPLOY_SSH_PORT"
+DEPLOY_SSH_KEY="$(_existing DEPLOY_SSH_KEY)"
+MEMORY_MAX="$(_existing MEMORY_MAX)"
+CPU_QUOTA="$(_existing CPU_QUOTA)"
+TASKS_MAX="$(_existing TASKS_MAX)"
+[ -f "$DEPLOY_SSH_KEY" ] || { warn "managed SSH key is missing: $DEPLOY_SSH_KEY"; exit 1; }
+if [[ "$(_existing HUB_PORT || true)" =~ ^(878[8-9]|87[9][0-9]|8[89][0-9]{2})$ ]] && \
+   [ "$(_existing WORKSPACE_ROOT || true)" = "/w/$(_existing HUB_PORT)" ]; then
+  HUB_PORT="$(_existing HUB_PORT)"
+  WORKSPACE_ROOT="$(_existing WORKSPACE_ROOT)"
+  note "Keeping allocated host slot: port $HUB_PORT, workspace $WORKSPACE_ROOT"
+else
+  say "Checking existing Silo environments, listening sockets, and workspace paths..."
+  allocate_host_slot
+  note "Allocated host slot: port $HUB_PORT, workspace $WORKSPACE_ROOT"
+fi
+note "Platform ceilings: MemoryMax=$MEMORY_MAX, CPUQuota=$CPU_QUOTA, TasksMax=$TASKS_MAX"
+
+stage "Dedicated PostgreSQL database" 4
+say "A PostgreSQL server may be shared, but this Silo gets a distinct login role and database."
+seed_default DATABASE_HOST "127.0.0.1"
+seed_default DATABASE_PORT "5432"
+seed_default DATABASE_NAME "cph_${INSTANCE_ID//-/_}"
+seed_default DATABASE_USER "cph_${INSTANCE_ID//-/_}"
+DATABASE_NAME="$(_existing DATABASE_NAME)"
+if ! _existing DATABASE_PASSWORD >/dev/null 2>&1; then
+  DATABASE_PASSWORD="$(openssl rand -base64 36 | tr -d '\n')"
+  write_env DATABASE_PASSWORD "$DATABASE_PASSWORD"
+fi
+note "The generated OPERATE.md uses an interactive/protected SQL path; the password is never put in a command argument."
+
+stage "Public URL and Feishu app" 9
+open_url "https://open.feishu.cn/app"
+say "Create or open the Organization's own app. Copy credentials from Credentials & Basic Info."
+PUBLIC_BASE_URL="https://${ORGANIZATION_SLUG}.${CPH_ALPHA_BASE_DOMAIN:-educraft.paradigm-edu.net}"
+write_env PUBLIC_BASE_URL "$PUBLIC_BASE_URL"
+note "Platform-assigned public URL: $PUBLIC_BASE_URL"
+capture FEISHU_APP_ID "Feishu App ID:"
+capture_secret FEISHU_APP_SECRET "Feishu App Secret:"
+say "Resolving the bot Open ID from Feishu..."
+FEISHU_BOT_OPEN_ID="$(printf '%s\0%s\0' "$FEISHU_APP_ID" "$FEISHU_APP_SECRET" | node "$SCRIPT_DIR/resolve_feishu_bot.mjs")"
+write_env FEISHU_BOT_OPEN_ID "$FEISHU_BOT_OPEN_ID"
+note "Resolved bot identity: $FEISHU_BOT_OPEN_ID"
+open_url "https://open.feishu.cn/document/server-docs/contact-v3/user/get"
+step "In the user/get page, click the user_id value picker, select the first OWNER, and copy the returned open_id."
+capture OWNER_OPEN_ID "OWNER Open ID (ou_...):"
+capture OWNER_DISPLAY_NAME "OWNER display name:"
+write_env OWNER_UNION_ID ""
+say "The exact redirect URL and acceptance steps will be written to OPERATE.md."
+
+stage "Provider and Alpha limits" 5
+say "Use a provider credential exclusive to this Organization. Host proxy setup is a separate prerequisite."
+seed_default PROVIDER_ID "openrouter"
+seed_default PROVIDER_BASE_URL "https://openrouter.ai/api"
+seed_default DEFAULT_MODEL "anthropic/claude-sonnet-5"
+seed_default DEFAULT_ROLE_ID "draft"
+seed_default DEFAULT_ROLE_LABEL "智能助手"
+seed_default MAX_TURNS "25"
+seed_default MAX_CONCURRENT_RUNS "4"
+seed_default MAX_RUN_SECONDS "900"
+seed_default HTTP_BODY_LIMIT_BYTES "1048576"
+seed_default MAX_FILES_PER_MESSAGE "8"
+seed_default MAX_FILE_BYTES "26214400"
+seed_default HTTP_REQUESTS_PER_MINUTE "120"
+seed_default FEISHU_EVENTS_PER_MINUTE "120"
+capture_secret PROVIDER_AUTH_TOKEN "Provider auth token:"
+for key in PROVIDER_ID PROVIDER_BASE_URL DEFAULT_MODEL DEFAULT_ROLE_ID DEFAULT_ROLE_LABEL \
+  MAX_TURNS MAX_CONCURRENT_RUNS MAX_RUN_SECONDS HTTP_BODY_LIMIT_BYTES \
+  MAX_FILES_PER_MESSAGE MAX_FILE_BYTES HTTP_REQUESTS_PER_MINUTE FEISHU_EVENTS_PER_MINUTE; do
+  printf -v "$key" '%s' "$(_existing "$key")"
+done
+write_env APPROVED_SKILLS "outline,lesson-project,data-processing-spec,typst"
+note "Platform runtime: OpenRouter, concurrency 4, default education role, curated skills."
+if ! _existing HUB_SESSION_SECRET >/dev/null 2>&1; then
+  command -v openssl >/dev/null 2>&1 || { warn "openssl is required"; exit 1; }
+  HUB_SESSION_SECRET="$(openssl rand -hex 32)"
+  write_env HUB_SESSION_SECRET "$HUB_SESSION_SECRET"
+fi
+
+stage "Render the private deployment bundle" 2
+say "This renders platform.env, bootstrap.json, deploy.env, nginx.conf and OPERATE.md."
+command -v node >/dev/null 2>&1 || { warn "Node.js is required to render safely"; exit 1; }
+node "$SCRIPT_DIR/render_new_silo_bundle.mjs" "$ENV_FILE" "$OUTPUT_DIR"
+chmod 0700 "$OUTPUT_DIR"
+chmod 0600 "$OUTPUT_DIR"/*
+say "Bundle: $OUTPUT_DIR"
+warn "It contains database, Feishu, provider and session secrets. Never commit or paste it."
+
+stage "Operator handoff and gates" 7
+say "The deployment package is an internal retry/audit checkpoint; you do not operate it manually."
+step "Target: $PUBLIC_BASE_URL → $DEPLOY_HOST:$HUB_PORT"
+step "Resources: database $DATABASE_NAME, workspace $WORKSPACE_ROOT, service cph-hub-$INSTANCE_ID"
+warn "Confirmation will create server, database, TLS, and runtime state."
+if confirm "Deploy this Organization now?"; then
+  bash "$SCRIPT_DIR/apply_new_silo.sh" "$OUTPUT_DIR"
+else
+  warn "deployment skipped; rerun the wizard later and keep existing answers"
+fi
+
+finish

hub/deploy/render_new_silo_bundle.mjs

@@ -0,0 +1,217 @@
+#!/usr/bin/env node
+
+import { chmod, mkdir, readFile, writeFile } from "node:fs/promises";
+import { resolve } from "node:path";
+
+const [answersPath, outputPath] = process.argv.slice(2);
+if (!answersPath || !outputPath) {
+  throw new Error("usage: render_new_silo_bundle.mjs ANSWERS_ENV OUTPUT_DIR");
+}
+
+function parseAnswers(source) {
+  const values = new Map();
+  for (const [index, line] of source.split("\n").entries()) {
+    if (!line || line.startsWith("#")) continue;
+    const separator = line.indexOf("=");
+    if (separator < 1) throw new Error(`invalid answers line ${index + 1}`);
+    const key = line.slice(0, separator);
+    const value = line.slice(separator + 1);
+    if (!/^[A-Z][A-Z0-9_]*$/.test(key)) {
+      throw new Error(`invalid answers key on line ${index + 1}: ${key}`);
+    }
+    if (value.includes("\r") || value.includes("\n")) {
+      throw new Error(`multiline value is not supported: ${key}`);
+    }
+    values.set(key, value);
+  }
+  return values;
+}
+
+function required(values, key) {
+  const value = values.get(key);
+  if (!value) throw new Error(`missing required answer: ${key}`);
+  return value;
+}
+
+function optional(values, key, fallback = "") {
+  return values.get(key) || fallback;
+}
+
+function assertMatch(label, value, pattern) {
+  if (!pattern.test(value)) throw new Error(`invalid ${label}: ${value}`);
+}
+
+function envLine(key, value) {
+  if (/[\r\n]/.test(value)) throw new Error(`unsafe newline in ${key}`);
+  return `${key}=${value}`;
+}
+
+const answers = parseAnswers(await readFile(resolve(answersPath), "utf8"));
+const instanceId = required(answers, "INSTANCE_ID");
+const orgId = required(answers, "ORGANIZATION_ID");
+const orgSlug = required(answers, "ORGANIZATION_SLUG");
+const port = required(answers, "HUB_PORT");
+const workspaceRoot = required(answers, "WORKSPACE_ROOT");
+const publicBaseUrl = required(answers, "PUBLIC_BASE_URL").replace(/\/$/, "");
+const domain = new URL(publicBaseUrl).hostname;
+const databasePassword = required(answers, "DATABASE_PASSWORD");
+const databaseUrl = `postgresql://${encodeURIComponent(required(answers, "DATABASE_USER"))}:${encodeURIComponent(databasePassword)}@${required(answers, "DATABASE_HOST")}:${required(answers, "DATABASE_PORT")}/${encodeURIComponent(required(answers, "DATABASE_NAME"))}`;
+
+assertMatch("INSTANCE_ID", instanceId, /^[a-z0-9](?:[a-z0-9-]{0,22}[a-z0-9])?$/);
+assertMatch("organization slug", orgSlug, /^[a-z0-9](?:[a-z0-9-]*[a-z0-9])?$/);
+assertMatch("port", port, /^[1-9][0-9]{1,4}$/);
+assertMatch("database name", required(answers, "DATABASE_NAME"), /^[a-z_][a-z0-9_]*$/);
+assertMatch("database user", required(answers, "DATABASE_USER"), /^[a-z_][a-z0-9_]*$/);
+assertMatch("default role id", required(answers, "DEFAULT_ROLE_ID"), /^[a-z][a-z0-9-]*$/);
+assertMatch("release id", required(answers, "RELEASE_ID"), /^[A-Za-z0-9._-]+$/);
+if (!publicBaseUrl.startsWith("https://")) throw new Error("PUBLIC_BASE_URL must use https");
+for (const [label, value] of [
+  ["WORKSPACE_ROOT", workspaceRoot],
+  ["DEPLOY_BASE", required(answers, "DEPLOY_BASE")],
+  ["DEPLOY_SSH_KEY", required(answers, "DEPLOY_SSH_KEY")],
+  ["CPH_BIN", required(answers, "CPH_BIN")],
+]) {
+  if (!value.startsWith("/") || /\s/.test(value)) {
+    throw new Error(`${label} must be an absolute path without whitespace: ${value}`);
+  }
+}
+if (Number(port) > 65535) throw new Error(`invalid port: ${port}`);
+if (Buffer.byteLength(workspaceRoot) > 16) {
+  throw new Error(`WORKSPACE_ROOT exceeds the 16-byte sandbox socket limit: ${workspaceRoot}`);
+}
+
+const outputDir = resolve(outputPath);
+await mkdir(outputDir, { recursive: true, mode: 0o700 });
+await chmod(outputDir, 0o700);
+
+const base = required(answers, "DEPLOY_BASE");
+const release = required(answers, "RELEASE_ID");
+const releaseHub = `${base}/releases/${release}/hub`;
+const secretDir = `${base}/.secrets/${instanceId}`;
+const envPath = `${secretDir}/platform.env`;
+const keyringPath = `${secretDir}/secret-keyring.json`;
+const unit = `cph-hub-${instanceId}.service`;
+
+const platformEnv = [
+  "# Generated by hub/deploy/new_silo.sh. Install root:root mode 0600.",
+  envLine("NODE_ENV", "production"),
+  envLine("DATABASE_URL", databaseUrl),
+  envLine("HUB_SILO_ORGANIZATION_ID", orgId),
+  envLine("HUB_SYSTEMD_UNIT", unit),
+  envLine("CPH_BIN", required(answers, "CPH_BIN")),
+  envLine("HOST", "127.0.0.1"),
+  envLine("PORT", port),
+  envLine("HUB_PROJECT_WORKSPACE_ROOT", workspaceRoot),
+  envLine("HUB_PUBLIC_BASE_URL", publicBaseUrl),
+  envLine("HUB_SESSION_SECRET", required(answers, "HUB_SESSION_SECRET")),
+  envLine("HUB_AGENT_MAX_TURNS", required(answers, "MAX_TURNS")),
+  envLine("HUB_AGENT_MAX_CONCURRENT_RUNS", required(answers, "MAX_CONCURRENT_RUNS")),
+  envLine("HUB_AGENT_MAX_RUN_SECONDS", required(answers, "MAX_RUN_SECONDS")),
+  envLine("HUB_HTTP_BODY_LIMIT_BYTES", required(answers, "HTTP_BODY_LIMIT_BYTES")),
+  envLine("HUB_MAX_FILES_PER_MESSAGE", required(answers, "MAX_FILES_PER_MESSAGE")),
+  envLine("HUB_MAX_FILE_BYTES", required(answers, "MAX_FILE_BYTES")),
+  envLine("HUB_HTTP_REQUESTS_PER_MINUTE", required(answers, "HTTP_REQUESTS_PER_MINUTE")),
+  envLine("HUB_FEISHU_EVENTS_PER_MINUTE", required(answers, "FEISHU_EVENTS_PER_MINUTE")),
+  envLine("HUB_FEISHU_LISTENER_ENABLED", "true"),
+  envLine("HTTP_PROXY", "http://127.0.0.1:7890"),
+  envLine("HTTPS_PROXY", "http://127.0.0.1:7890"),
+  envLine("ALL_PROXY", "socks5h://127.0.0.1:7890"),
+  envLine("NO_PROXY", "127.0.0.1,localhost,::1"),
+  envLine("NODE_USE_ENV_PROXY", "1"),
+  envLine("ANTHROPIC_DEFAULT_SONNET_MODEL", "anthropic/claude-sonnet-5"),
+  envLine("CPH_SANDBOX_EXTRA_DENY_READ", `${envPath}:${keyringPath}`),
+  "",
+].join("\n");
+
+const bootstrap = {
+  organization: {
+    id: orgId,
+    slug: orgSlug,
+    name: required(answers, "ORGANIZATION_NAME"),
+  },
+  owner: {
+    openId: required(answers, "OWNER_OPEN_ID"),
+    displayName: required(answers, "OWNER_DISPLAY_NAME"),
+  },
+  feishu: {
+    appId: required(answers, "FEISHU_APP_ID"),
+    appSecret: required(answers, "FEISHU_APP_SECRET"),
+    botOpenId: required(answers, "FEISHU_BOT_OPEN_ID"),
+  },
+  provider: {
+    providerId: required(answers, "PROVIDER_ID"),
+    baseUrl: required(answers, "PROVIDER_BASE_URL"),
+    authToken: required(answers, "PROVIDER_AUTH_TOKEN"),
+  },
+  teams: [],
+};
+const ownerUnionId = optional(answers, "OWNER_UNION_ID");
+if (ownerUnionId) bootstrap.owner.unionId = ownerUnionId;
+
+const deployEnv = [
+  "# Source this file locally before deploy_platform.sh (contains no app/provider secrets).",
+  envLine("PLATFORM_DEPLOY_HOST", required(answers, "DEPLOY_HOST")),
+  envLine("PLATFORM_DEPLOY_SSH_KEY", required(answers, "DEPLOY_SSH_KEY")),
+  envLine("PLATFORM_DEPLOY_USER", required(answers, "DEPLOY_USER")),
+  envLine("PLATFORM_DEPLOY_PORT", required(answers, "DEPLOY_SSH_PORT")),
+  envLine("PLATFORM_DEPLOY_HUB_PORT", port),
+  envLine("PLATFORM_DEPLOY_BASE", base),
+  envLine("PLATFORM_DEPLOY_RELEASE", release),
+  envLine("PLATFORM_DEPLOY_INSTANCE", instanceId),
+  envLine("PLATFORM_DEPLOY_WORKSPACE_ROOT", workspaceRoot),
+  envLine("PLATFORM_DEPLOY_MEMORY_MAX", required(answers, "MEMORY_MAX")),
+  envLine("PLATFORM_DEPLOY_CPU_QUOTA", required(answers, "CPU_QUOTA")),
+  envLine("PLATFORM_DEPLOY_TASKS_MAX", required(answers, "TASKS_MAX")),
+  envLine("PLATFORM_DEPLOY_HEALTH_URL", `http://127.0.0.1:${port}/api/healthz`),
+  "",
+].join("\n");
+
+const nginx = `# Install as /etc/nginx/conf.d/${instanceId}.conf after obtaining TLS certificates.\nserver {\n  listen 80;\n  server_name ${domain};\n  return 301 https://$host$request_uri;\n}\n\nserver {\n  listen 443 ssl http2;\n  server_name ${domain};\n\n  ssl_certificate /etc/letsencrypt/live/${domain}/fullchain.pem;\n  ssl_certificate_key /etc/letsencrypt/live/${domain}/privkey.pem;\n\n  location / {\n    proxy_pass http://127.0.0.1:${port};\n    proxy_http_version 1.1;\n    proxy_set_header Host $host;\n    proxy_set_header X-Real-IP $remote_addr;\n    proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;\n    proxy_set_header X-Forwarded-Proto https;\n  }\n}\n`;
+
+const defaultRolePrompt = `你是一位教育机构智能助手，服务于学校和教培机构的日常管理与协作。
+## 核心能力
+**教务管理**：熟悉排课调课、班级管理、课时统计、师资调度等常见管理流程。
+**教研支持**：理解课程设计、教案编写、例题/变式题、定理证明、随堂练习、阶段性测验、知识点拆解、大纲对标等教学业务概念。
+**数字化操作**：熟练使用shell命令行进行文件管理、批量处理、脚本编写、文本处理（grep/sed/awk等）、自动化任务；能协助处理Markdown、Typst等文档、表格数据、格式转换等。
+## 行为准则
+- **实事求是**：不确定时明确说明，能力边界外的任务如实告知，不为完成目标而编造信息或勉强输出
+- **简洁优先**：直接给出答案或方案，省略铺垫和客套
+- **按需展开**：仅在问题复杂或用户明确要求时提供详细说明
+- **结构清晰**：多步骤内容使用编号，便于飞书阅读
+- **可操作性**：涉及操作时给出具体命令或步骤
+保持专业、高效，像一位熟悉业务的同事。
+`;
+
+const operate = `# ${instanceId} deployment commands\n\nThis file contains no application/provider secrets. Run commands deliberately; do not source answers.env.\n\n## 1. DNS and Feishu\n\n- Point \`${domain}\` to \`${required(answers, "DEPLOY_HOST")}\`.\n- In the Feishu app, configure redirect URL: \`${publicBaseUrl}/auth/feishu/callback\`.\n- Enable the required bot/message/contact permissions and event subscription described in the customer setup document.\n\n## 2. Database (run as the PostgreSQL administrator)\n\nCreate one role and one database for this Silo. The password is in \`answers.env\`; use an interactive client or a protected SQL file, never a command-line argument.\n\n\`\`\`sql\nCREATE ROLE ${required(answers, "DATABASE_USER")} LOGIN PASSWORD '<copy DATABASE_PASSWORD from answers.env>';\nCREATE DATABASE ${required(answers, "DATABASE_NAME")} OWNER ${required(answers, "DATABASE_USER")};\n\`\`\`\n\n## 3. Publish the immutable release\n\nThe normal deploy script seeds the first-instance secrets and exits 78. That exit is expected only on this first pass.\n\n\`\`\`sh\nset -a; . ./deploy.env; set +a\nbash hub/deploy/deploy_platform.sh\n\`\`\`\n\n## 4. Install the generated secrets\n\nCopy \`platform.env\` and \`bootstrap.json\` to the server through a protected channel. On the server:\n\n\`\`\`sh\ninstall -d -o root -g root -m 0700 '${secretDir}'\ninstall -o root -g root -m 0600 platform.env '${envPath}'\ninstall -o root -g root -m 0600 bootstrap.json '/root/${instanceId}-bootstrap.json'\n# Copy ${keyringPath} to separate off-host recovery storage before continuing.\n\`\`\`\n\n## 5. Migrate, install the stopped service, and bootstrap\n\n\`\`\`sh\nset -a; . '${envPath}'; set +a\nnode '${releaseHub}/node_modules/prisma/build/index.js' migrate deploy --schema '${releaseHub}/prisma/schema.prisma'\nBASE='${base}' HUB_DIR='${releaseHub}' INSTANCE_ID='${instanceId}' WORKSPACE_ROOT='${workspaceRoot}' PORT='${port}' MEMORY_MAX='${required(answers, "MEMORY_MAX")}' CPU_QUOTA='${required(answers, "CPU_QUOTA")}' TASKS_MAX='${required(answers, "TASKS_MAX")}' bash '${releaseHub}/deploy/install_service.sh'\nnode '${releaseHub}/dist/deployment/bootstrap-silo-cli.js' --config-file '/root/${instanceId}-bootstrap.json' --keyring-file '${keyringPath}'\nrm -f '/root/${instanceId}-bootstrap.json'\n\`\`\`\n\n## 6. Runtime role and skills\n\nRuntime role/skill configuration is intentionally separate from the release. Follow NEW_SILO_RUNBOOK.md, staging each approved skill directory outside the immutable release, then use \`agent_config.sh\`. Do not silently copy a local personal skill collection.\n\n## 7. Nginx, start, and acceptance\n\nInstall \`nginx.conf\`, run \`nginx -t\`, reload Nginx, then:\n\n\`\`\`sh\nsystemctl start '${unit}'\nsystemctl is-active '${unit}'\ncurl --fail --silent --show-error 'http://127.0.0.1:${port}/api/healthz'\ncurl --fail --silent --show-error '${publicBaseUrl}/api/healthz'\njournalctl -u '${unit}' --since '-10 min' --no-pager\n\`\`\`\n\nAcceptance requires: Feishu OAuth completes, OWNER and a non-OWNER can @bot, a second group creates a separate project/session, Typst works when that skill is enabled, and restart preserves session cursor. Then take the first off-host backup.\n\n## 8. Later releases\n\nAfter the instance exists, source \`deploy.env\` with the new release id and run \`deploy_platform.sh\`. Never reuse another org's database, secret directory, workspace root, port, service identity, domain, Feishu app, or provider credential.\n`;
+
+const selectedSkills = optional(answers, "APPROVED_SKILLS");
+const roleInstructions = `
+## Appendix: default runtime role
+
+Copy \`default-role-prompt.md\` to \`/root/${instanceId}-default-role-prompt.md\`.
+After installing each reviewed skill with \`agent_config.sh install-skill\`, run:
+
+\`\`\`sh
+INSTANCE_ID=${JSON.stringify(instanceId)} ENV_FILE=${JSON.stringify(envPath)} HUB_DIR=${JSON.stringify(releaseHub)} bash ${JSON.stringify(`${releaseHub}/deploy/agent_config.sh`)} upsert-role --organization ${JSON.stringify(orgId)} --role ${JSON.stringify(required(answers, "DEFAULT_ROLE_ID"))} --label ${JSON.stringify(required(answers, "DEFAULT_ROLE_LABEL"))} --model ${JSON.stringify(required(answers, "DEFAULT_MODEL"))} --system-prompt-file ${JSON.stringify(`/root/${instanceId}-default-role-prompt.md`)} --tools-json null
+${selectedSkills ? `INSTANCE_ID=${JSON.stringify(instanceId)} ENV_FILE=${JSON.stringify(envPath)} HUB_DIR=${JSON.stringify(releaseHub)} bash ${JSON.stringify(`${releaseHub}/deploy/agent_config.sh`)} set-role-skills --organization ${JSON.stringify(orgId)} --role ${JSON.stringify(required(answers, "DEFAULT_ROLE_ID"))} --skills ${JSON.stringify(selectedSkills)}
+` : "# No skills selected in the wizard; set-role-skills remains an explicit operator step.\n"}INSTANCE_ID=${JSON.stringify(instanceId)} ENV_FILE=${JSON.stringify(envPath)} HUB_DIR=${JSON.stringify(releaseHub)} bash ${JSON.stringify(`${releaseHub}/deploy/agent_config.sh`)} list --organization ${JSON.stringify(orgId)}
+\`\`\`
+
+Changing a role's model, system prompt, tools or skill selection archives that
+role's existing sessions by design. Finish this setup before inviting Alpha users.
+`;
+
+async function privateWrite(name, contents) {
+  const path = resolve(outputDir, name);
+  await writeFile(path, contents, { encoding: "utf8", mode: 0o600 });
+  await chmod(path, 0o600);
+}
+
+await privateWrite("platform.env", platformEnv);
+await privateWrite("bootstrap.json", `${JSON.stringify(bootstrap, null, 2)}\n`);
+await privateWrite("deploy.env", deployEnv);
+await privateWrite("nginx.conf", nginx);
+await privateWrite("default-role-prompt.md", defaultRolePrompt);
+await privateWrite("OPERATE.md", `${operate}${roleInstructions}`);
+
+console.log(`Rendered private Silo bundle: ${outputDir}`);

hub/deploy/resolve_feishu_bot.mjs

@@ -0,0 +1,27 @@
+#!/usr/bin/env node
+
+const chunks = [];
+for await (const chunk of process.stdin) chunks.push(chunk);
+const [appId, appSecret] = Buffer.concat(chunks).toString("utf8").split("\0");
+if (!appId || !appSecret) throw new Error("Feishu App ID and App Secret are required on stdin");
+
+const tokenResponse = await fetch("https://open.feishu.cn/open-apis/auth/v3/tenant_access_token/internal", {
+  method: "POST",
+  headers: { "content-type": "application/json; charset=utf-8" },
+  body: JSON.stringify({ app_id: appId, app_secret: appSecret }),
+});
+if (!tokenResponse.ok) throw new Error(`Feishu token request failed: HTTP ${tokenResponse.status}`);
+const tokenPayload = await tokenResponse.json();
+if (tokenPayload.code !== 0 || typeof tokenPayload.tenant_access_token !== "string") {
+  throw new Error(`Feishu token request failed: ${JSON.stringify(tokenPayload)}`);
+}
+
+const botResponse = await fetch("https://open.feishu.cn/open-apis/bot/v3/info", {
+  headers: { authorization: `Bearer ${tokenPayload.tenant_access_token}` },
+});
+if (!botResponse.ok) throw new Error(`Feishu bot info request failed: HTTP ${botResponse.status}`);
+const botPayload = await botResponse.json();
+if (botPayload.code !== 0 || typeof botPayload.bot?.open_id !== "string" || !botPayload.bot.open_id) {
+  throw new Error(`Feishu bot info request failed: ${JSON.stringify(botPayload)}`);
+}
+process.stdout.write(botPayload.bot.open_id);

hub/package-lock.json

@@ -1,12 +1,12 @@
 {
   "name": "@paradigm/hub",
-  "version": "0.0.11",
+  "version": "0.0.20",
   "lockfileVersion": 3,
   "requires": true,
   "packages": {
     "": {
       "name": "@paradigm/hub",
-      "version": "0.0.11",
+      "version": "0.0.20",
       "dependencies": {
         "@anthropic-ai/claude-agent-sdk": "^0.3.202",
         "@fastify/cookie": "^11.0.2",

hub/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@paradigm/hub",
-  "version": "0.0.11",
+  "version": "0.0.20",
   "private": true,
   "type": "module",
   "engines": {

hub/src/admin/routes/authRoutes.ts

@@ -5,7 +5,7 @@ import { randomBytes } from "node:crypto";
 import type { PrismaClient } from "@prisma/client";
 import type { FastifyInstance, FastifyReply, FastifyRequest } from "fastify";
 import { resolveActiveFeishuApplication } from "../../connections/feishuApplicationConnections.js";
-import { upsertScopedFeishuIdentity } from "../../feishu/identityNamespace.js";
+import { upsertScopedFeishuIdentityInTransaction } from "../../feishu/identityNamespace.js";
 import type { LocalSecretEnvelope } from "../../security/secretEnvelope.js";
 import {
   buildAuthorizeUrl,
@@ -164,16 +164,54 @@ export async function registerAuthRoutes(app: FastifyInstance, config: AuthRoute
       const feishuUser = await exchangeCodeForUser(oauthConfig, code);
       let userId: string;
       if (statePayload.connectionId !== undefined && statePayload.organizationId !== undefined) {
-        const identity = await upsertScopedFeishuIdentity(config.prisma, {
-          connectionId: statePayload.connectionId,
-          openId: feishuUser.openId,
-          ...(feishuUser.unionId !== undefined ? { unionId: feishuUser.unionId } : {}),
-          displayName: feishuUser.displayName,
-          ...(feishuUser.avatarUrl !== null ? { avatarUrl: feishuUser.avatarUrl } : {}),
+        const connectionId = statePayload.connectionId;
+        const organizationId = statePayload.organizationId;
+        const identity = await config.prisma.$transaction(async (tx) => {
+          const resolved = await upsertScopedFeishuIdentityInTransaction(tx, {
+            connectionId,
+            expectedOrganizationId: organizationId,
+            openId: feishuUser.openId,
+            ...(feishuUser.unionId !== undefined ? { unionId: feishuUser.unionId } : {}),
+            displayName: feishuUser.displayName,
+            ...(feishuUser.avatarUrl !== null ? { avatarUrl: feishuUser.avatarUrl } : {}),
+          });
+          const activeMembership = await tx.organizationMembership.findFirst({
+            where: {
+              organizationId,
+              userId: resolved.userId,
+              revokedAt: null,
+            },
+            select: { id: true },
+          });
+          if (activeMembership === null) {
+            const revokedMembership = await tx.organizationMembership.findFirst({
+              where: {
+                organizationId,
+                userId: resolved.userId,
+                revokedAt: { not: null },
+              },
+              select: { id: true },
+            });
+            if (revokedMembership === null) {
+              await tx.organizationMembership.create({
+                data: {
+                  organizationId,
+                  userId: resolved.userId,
+                  role: "MEMBER",
+                },
+              });
+              await tx.auditEntry.create({
+                data: {
+                  organizationId,
+                  actorUserId: resolved.userId,
+                  action: "organization_member.oauth_auto_joined",
+                  metadata: { connectionId: resolved.connectionId, role: "MEMBER" },
+                },
+              });
+            }
+          }
+          return resolved;
         });
-        if (identity.organizationId !== statePayload.organizationId) {
-          throw new HttpError(400, "bad_request", "OAuth identity Organization scope mismatch");
-        }
         userId = identity.userId;
         setSessionCookie(reply, config, {
           userId,
@@ -235,6 +273,34 @@ export async function registerAuthRoutes(app: FastifyInstance, config: AuthRoute
     return reply.status(204).send();
   });
 
+  app.get("/auth/feishu/complete", async (request, reply) => {
+    const query = request.query as { org?: string };
+    const organizationName = typeof query.org === "string" && query.org.trim() !== ""
+      ? query.org.trim()
+      : "当前组织";
+    return reply.type("text/html").send(`<!doctype html>
+<html lang="zh-CN">
+<head>
+  <meta charset="utf-8"/>
+  <meta name="viewport" content="width=device-width, initial-scale=1"/>
+  <title>Educraft 登录成功</title>
+  <style>
+    body{font-family:system-ui,sans-serif;display:flex;min-height:100vh;align-items:center;justify-content:center;margin:0;background:#f6f7f9;color:#1a1a1a}
+    .card{background:#fff;padding:2rem 2.5rem;border-radius:12px;box-shadow:0 8px 24px rgba(0,0,0,.08);max-width:25rem;text-align:center}
+    .ok{font-size:3rem;margin:0 0 .5rem}.hint{color:#646a73;line-height:1.6}
+  </style>
+</head>
+<body>
+  <main class="card">
+    <p class="ok">✅</p>
+    <h1>登录并加入组织成功</h1>
+    <p>你已加入 ${escapeHtml(organizationName)}。</p>
+    <p class="hint">现在可以关闭本页面，返回飞书群再次 @机器人继续使用。</p>
+  </main>
+</body>
+</html>`);
+  });
+
   app.get("/api/me", async (request, reply) => {
     try {
       const auth = await requireSession(request, reply, guardDeps);
@@ -363,10 +429,13 @@ async function resolvePostLoginRedirect(
         revokedAt: null,
         organization: { status: "ACTIVE" },
       },
-      select: { organization: { select: { slug: true } } },
+      select: { organization: { select: { slug: true, name: true } } },
     });
     if (intended === null) return "/admin?error=not_an_active_org_member";
     const orgRoot = `/admin/org/${intended.organization.slug}`;
+    if (returnTo === "/admin") {
+      return `/auth/feishu/complete?org=${encodeURIComponent(intended.organization.name)}`;
+    }
     return returnTo === orgRoot || returnTo.startsWith(`${orgRoot}/`) ? returnTo : orgRoot;
   }
   if (returnTo !== "/admin" && returnTo.startsWith("/admin")) {

hub/src/feishu/trigger.ts

@@ -35,7 +35,6 @@ import type { RuntimeSettings } from "../settings/runtime.js";
 import { currentLockRunId, releaseLock } from "../lock.js";
 import { createPermissionAuthorizer, type AuthorizationDecision, type PermissionAuthorizer } from "../permission.js";
 import { writeAudit } from "../audit.js";
-import { formatRunCostLine } from "../agent/cost.js";
 import { createAgentSdkStderrSink } from "../agent/diagnostics.js";
 import { InactiveOrganizationError, lockActiveOrganization } from "../org/status.js";
 import { StreamingAgentCard } from "./card/streaming-card.js";
@@ -550,7 +549,7 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
             : result.status === "failed" && result.error !== undefined
               ? `\u5904\u7406\u5931\u8D25: ${result.error}`
               : result.text;
-        await card.finish(finalText, { interrupted, footerText: formatRunCostLine(result.costUsd) });
+        await card.finish(finalText, { interrupted });
         const metadataPatch = sessionMetadataPatch(result.sdkSessionId);
         if (metadataPatch !== null) {
           await deps.prisma.agentSession.update({
@@ -1160,14 +1159,14 @@ export function makeTriggerHandler(deps: TriggerDeps): TriggerHandler {
       return {
         status: "error",
         reason: "identity_missing",
-        message: `请先通过飞书登录建立身份：${loginUrl}\n登录后仍需由组织管理员将你加入组织。`,
+        message: `请先通过飞书登录并加入组织：${loginUrl}\n完成后返回群聊重试。`,
       };
     }
     if (user.organizationMemberships.length === 0) {
       return {
         status: "error",
         reason: "membership_missing",
-        message: "你已完成飞书登录，但尚未加入该组织。请联系组织管理员为你开通成员权限。",
+        message: "你尚未加入该组织，或成员资格已被移除。请联系组织管理员。",
       };
     }
     const membership = user.organizationMemberships[0]!;

hub/test/integration/admin-auth.test.ts

@@ -267,9 +267,6 @@ describe("admin auth + org API guards", () => {
       openId: "ou_scoped_user",
       displayName: "Invited User",
     });
-    await prisma.organizationMembership.create({
-      data: { organizationId: DEFAULT_ORG_ID, userId: identity.userId, role: "ADMIN" },
-    });
     await seedTestOrganization("org_scoped_other", "scoped-other");
     await prisma.organizationMembership.create({
       data: { organizationId: "org_scoped_other", userId: identity.userId, role: "ADMIN" },
@@ -317,7 +314,7 @@ describe("admin auth + org API guards", () => {
       expect(me.statusCode).toBe(200);
       expect(me.json()).toMatchObject({
         user: { id: identity.userId, displayName: "Scoped User" },
-        organizations: [expect.objectContaining({ slug: "test-default", role: "ADMIN" })],
+        organizations: [expect.objectContaining({ slug: "test-default", role: "MEMBER" })],
       });
       expect((me.json() as { organizations: unknown[] }).organizations).toHaveLength(1);
       const crossOrganization = await app.inject({
@@ -331,6 +328,32 @@ describe("admin auth + org API guards", () => {
         where: { id: identity.identityId },
         select: { unionId: true },
       })).resolves.toEqual({ unionId: "on_scoped_union" });
+      await expect(prisma.auditEntry.count({
+        where: {
+          organizationId: DEFAULT_ORG_ID,
+          actorUserId: identity.userId,
+          action: "organization_member.oauth_auto_joined",
+        },
+      })).resolves.toBe(1);
+
+      const defaultStart = await app.inject({ method: "GET", url: "/auth/feishu/test-default" });
+      const defaultAuthorize = new URL(String(defaultStart.headers.location));
+      const defaultState = defaultAuthorize.searchParams.get("state");
+      expect(defaultState).not.toBeNull();
+      const defaultCallback = await app.inject({
+        method: "GET",
+        url: `/auth/feishu/callback?code=ok&state=${encodeURIComponent(defaultState!)}`,
+        headers: { cookie: cookiePair(defaultStart.headers["set-cookie"], OAUTH_STATE_COOKIE_NAME) },
+      });
+      expect(defaultCallback.statusCode).toBe(302);
+      expect(defaultCallback.headers.location).toBe(
+        "/auth/feishu/complete?org=Test%20Default%20Organization",
+      );
+      const complete = await app.inject({ method: "GET", url: defaultCallback.headers.location! });
+      expect(complete.statusCode).toBe(200);
+      expect(complete.headers["content-type"]).toContain("text/html");
+      expect(complete.body).toContain("登录并加入组织成功");
+      expect(complete.body).toContain("Test Default Organization");
 
       await connections.disable({ organizationId: DEFAULT_ORG_ID, actorUserId: "scoped-owner" });
       const revoked = await app.inject({ method: "GET", url: "/api/me", headers: { cookie: sessionCookie } });
@@ -340,6 +363,65 @@ describe("admin auth + org API guards", () => {
     }
   });
 
+  it("does not restore a revoked Organization membership during scoped OAuth", async () => {
+    await seedUser("revoked-owner", "legacy_revoked_owner", "OWNER");
+    const connections = new FeishuApplicationConnectionService(prisma, testSecretEnvelope, async () => {});
+    const connection = await connections.rotateCustomerApplication({
+      organizationId: DEFAULT_ORG_ID,
+      actorUserId: "revoked-owner",
+      appId: "cli_revoked_oauth",
+      appSecret: "revoked-oauth-secret",
+      botOpenId: "ou_revoked_bot",
+    });
+    const identity = await upsertScopedFeishuIdentity(prisma, {
+      connectionId: connection.id,
+      openId: "ou_revoked_user",
+      displayName: "Revoked User",
+    });
+    await prisma.organizationMembership.create({
+      data: {
+        organizationId: DEFAULT_ORG_ID,
+        userId: identity.userId,
+        role: "MEMBER",
+        revokedAt: new Date(),
+      },
+    });
+    const fetchImpl = vi.fn(async (input: RequestInfo | URL) => {
+      const url = String(input);
+      if (url.includes("/oauth/token")) {
+        return Response.json({ code: 0, access_token: "revoked-user-token" });
+      }
+      if (url.includes("/user_info")) {
+        return Response.json({
+          code: 0,
+          data: { open_id: "ou_revoked_user", name: "Revoked User" },
+        });
+      }
+      throw new Error(`unexpected ${url}`);
+    });
+    const app = await buildApp(fetchImpl as unknown as typeof fetch);
+    try {
+      const start = await app.inject({ method: "GET", url: "/auth/feishu/test-default" });
+      const authorize = new URL(String(start.headers.location));
+      const state = authorize.searchParams.get("state");
+      expect(state).not.toBeNull();
+      const callback = await app.inject({
+        method: "GET",
+        url: `/auth/feishu/callback?code=ok&state=${encodeURIComponent(state!)}`,
+        headers: { cookie: cookiePair(start.headers["set-cookie"], OAUTH_STATE_COOKIE_NAME) },
+      });
+      expect(callback.statusCode).toBe(302);
+      await expect(prisma.organizationMembership.count({
+        where: { organizationId: DEFAULT_ORG_ID, userId: identity.userId, revokedAt: null },
+      })).resolves.toBe(0);
+      await expect(prisma.auditEntry.count({
+        where: { action: "organization_member.oauth_auto_joined", actorUserId: identity.userId },
+      })).resolves.toBe(0);
+    } finally {
+      await app.close();
+    }
+  });
+
   it("unknown org slug returns 404 for admin", async () => {
     await seedUser("u-admin", "ou_admin", "ADMIN");
     const app = await buildApp();

hub/test/integration/trigger.test.ts

@@ -168,7 +168,8 @@ describe("trigger full lifecycle (integration)", () => {
       msgType: "interactive",
       replyInThread: undefined,
     });
-    expect(rt.sentTexts.some((text) => text.includes("mock response") && text.includes("本次成本: $0.0023"))).toBe(true);
+    expect(rt.sentTexts.some((text) => text.includes("mock response"))).toBe(true);
+    expect(rt.sentTexts.some((text) => text.includes("本次成本"))).toBe(false);
     expect(runAgentCalls).toHaveLength(1);
     expect(runAgentCalls[0]?.providerProxyEnv).toMatchObject({
       ANTHROPIC_BASE_URL: "http://127.0.0.1:12345",
@@ -662,8 +663,8 @@ describe("trigger full lifecycle (integration)", () => {
     await trigger(makeEvent("chat-bound-unknown", "@_user_1 写教案", "ou_bound_unknown"), rt);
 
     expect(rt.sentTexts).toContain(
-      "请先通过飞书登录建立身份：https://educraft.example.test/auth/feishu/test-default\n" +
-      "登录后仍需由组织管理员将你加入组织。",
+      "请先通过飞书登录并加入组织：https://educraft.example.test/auth/feishu/test-default\n" +
+      "完成后返回群聊重试。",
     );
     expect(rt.sentTexts).not.toContain("无权限触发。");
     expect(runAgentCalls).toHaveLength(0);
@@ -684,7 +685,7 @@ describe("trigger full lifecycle (integration)", () => {
     await trigger(makeEvent("chat-bound-non-member", "@_user_1 写教案", "ou_bound_non_member"), rt);
 
     expect(rt.sentTexts).toContain(
-      "你已完成飞书登录，但尚未加入该组织。请联系组织管理员为你开通成员权限。",
+      "你尚未加入该组织，或成员资格已被移除。请联系组织管理员。",
     );
     expect(rt.sentTexts).not.toContain("无权限触发。");
     expect(runAgentCalls).toHaveLength(0);
@@ -1011,8 +1012,8 @@ describe("trigger full lifecycle (integration)", () => {
     await trigger(makeEvent("chat-UNKNOWN", "@_user_1 写教案", "ou_unknown_user"), rt);
 
     expect(rt.sentTexts).toContain(
-      "请先通过飞书登录建立身份：https://educraft.example.test/auth/feishu/test-default\n" +
-      "登录后仍需由组织管理员将你加入组织。",
+      "请先通过飞书登录并加入组织：https://educraft.example.test/auth/feishu/test-default\n" +
+      "完成后返回群聊重试。",
     );
     expect(rt.sentCards).toHaveLength(0);
     const runs = await prisma.agentRun.findMany();
@@ -1033,7 +1034,7 @@ describe("trigger full lifecycle (integration)", () => {
     await trigger(makeEvent("chat-unbound", "@_user_1 写教案", "ou_logged_in_not_member"), rt);
 
     expect(rt.sentTexts).toContain(
-      "你已完成飞书登录，但尚未加入该组织。请联系组织管理员为你开通成员权限。",
+      "你尚未加入该组织，或成员资格已被移除。请联系组织管理员。",
     );
     expect(rt.sentTexts.join("\n")).not.toContain("/auth/feishu/");
     await expect(prisma.agentRun.count()).resolves.toBe(0);

spec/README.md

@@ -49,7 +49,7 @@ agent 不得用预训练先验脑补本领域(领域很新,无先验);prose 是
 
 ### 命名
 
-- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Run`、`Spec.Courseware.Validity`。
+- **模块 / 命名空间**:PascalCase,对应分层,如 `Spec.System.Agent.Run`、`Spec.Courseware.Validity`。
 - **类型**:PascalCase。
 - **谓词 / `Prop`**:用意图清晰的命名,如 `Legal…`、`ValidTransition`、`Can…`。
 - **文件粒度**:原则上"一个带独立不变式的概念一个文件"。

spec/Spec/Courseware.lean

@@ -16,6 +16,6 @@ import Spec.Courseware.Open
 - **`Check`** —— checker 语义:`Severity` + 6 类诊断 + **合法 lesson = 无 error 级
   诊断**(模型外设施诊断以抽象谓词 + `Oracle` 表示);检查管线的 5 阶段、序、compile
   门控。
-- **`Open`** —— 留白骨架(核心关系 OPEN,已 surface 不臆造):题库 `QuestionBank`、
+- **`Open`** —— OPEN 骨架(核心关系 OPEN,已 surface):题库 `QuestionBank`、
   课程编排 `Course`。
 -/

spec/Spec/Courseware/Check/Diagnostic.lean

@@ -6,7 +6,7 @@ import Spec.Courseware.Export.Render
 
 产品里"站在 Lean 位置"的 rule-based checker,语义在此沉淀(ADR-0010,经 ADR-0012
 修订)。它对 lesson 提诊断,每条有**分类**(`DiagKind`)与**严重级别**(`Severity`)。
-本模块:钉级别类型(二分);钉 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
+定级别类型(二分);定 7 类诊断各自的含义与级别,并把"**合法 lesson = 无
 error 级诊断**"建成判定(ADR-0005 deferred 的"完整合法判定"的回填);对**模型外设施**
 型诊断(typst 编过否、数据合 schema 否)用**抽象谓词 + `Oracle` 实现边界**表示——契约
 说"存在这条诊断、什么意思、什么级别",真值由实现提供,不在 Lean 内计算(不内嵌 typst
@@ -50,7 +50,7 @@ inductive DiagKind where
 
 /-- 每类诊断的**严重级别**(`PINNED`, ADR-0010)。六类 `error`(阻断);**唯
 `renderIgnored` 为 `warning`**——ADR-0005 种子规则"缺渲染 ⇒ warning,不阻断导出"。
-钉成全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
+全函数使"哪类阻断"成为可引用、可对齐的事实(实现侧 `DiagCode` 级别据此对齐)。 -/
 def DiagKind.severity : DiagKind → Severity
   | .partPathMissing    => .error
   | .unknownKind        => .error

spec/Spec/Courseware/Check/Pipeline.lean

@@ -5,8 +5,8 @@ import Spec.Courseware.Check.Diagnostic
 
 checker 的 `check` 按**固定顺序**跑五个阶段,逐阶段收集诊断;`compile` 阶段有**门控**。
 顺序与门控是契约——它决定用户看到哪些诊断(藏在缺文件背后的语法错,在文件补齐前不
-显示,这是有意的)。每阶段的**算法**不进 Lean(宪法第 5 条深度上限):只钉**阶段、序、
-门控**。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
+显示,这是有意的)。每阶段的**算法**不进 Lean(深度上限:只定**阶段、序、
+门控**)。阶段对应上游模块:`load`←`cph-model`;`structural`←part 路径/未知 kind;
 `schema`←`cph-schema`;`compile`←`cph-typst`(模型外设施);`coverage`←`renderIgnored`。
 -/
 

spec/Spec/Courseware/Export/Artifact.lean

@@ -2,7 +2,7 @@
 # Artifact —— export target 的产物(ADR-0009 / 0011)
 
 ADR-0009:一个 export target 是**一次 build**,产出一个**有类型的产物**。ADR-0011
-钉死:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
+固定:产物是**带字段的 ADT**——"产物到底指什么"(单文件落在哪 / 一棵树产出哪些文件)
 是不好猜的领域语义,必须写进字段 + doc,而非抹成两个空构造子。路径/glob 用 `String`
 承载并由 doc 赋义(它们就是文本),不复刻文件系统类型。
 -/

spec/Spec/Courseware/Export/Render.lean

@@ -4,7 +4,7 @@ import Spec.Courseware.Export.Artifact
 /-!
 # Render —— export target = artifact + 有序 typed steps(ADR-0009 / 0011)
 
-ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 钉死 build
+ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR-0011 固定 build
 的**形状**:一个 target 是 `artifact` + 一串**有序 typed step**。
 
 - `typstCompile template` —— 把**模板文件**(如 `exports/student.typ`)编译成产物。它是
@@ -20,7 +20,7 @@ ADR-0009:export target 是一次 build,产出一个有类型的 `Artifact`。ADR
 
 **shell step 的执行语义(ADR-0013)。** `shell` 不再只是占位:它**会被执行**,语义是把
 `run` 交给平台 shell、以**工程根为工作目录**运行,产物由被调外部工具自己写出(框架不装配
-内容)。三条边界是真分歧点,故钉契约:
+内容)。三条边界是真分歧点,故定为契约:
 1. **opt-in by construction** —— 任意命令执行只在用户**显式** build 一个 shell target 时发生,
    绝不在 `check` 里跑。`check` 只校验结构(lesson 是否合法),不执行外部工具、不验其产物。
 2. **失败归属** —— shell step 退出非零是一次 **build-过程失败**,不是 lesson 的合法性缺陷;
@@ -46,7 +46,7 @@ namespace Spec.Courseware
 variable (P : Primitives)
 
 /-- 一个 build **step**(`PINNED` typed, ADR-0011;可扩展)。MVP 仅一个 `typstCompile`;
-`steps` 是 list 因为 FileTree / 第三方 build 会需多步。刻意不把模板内部、shell 命令的
+`steps` 是 list 因为 FileTree / 第三方 build 会需多步。不把模板内部、shell 命令的
 解析结构写进来(实现细节, ADR-0011 OPEN)。 -/
 inductive Step where
   /-- 编译模板文件 `template`(相对工程根)成产物;框架注入 manifest。typed 的理由:

spec/Spec/Courseware/Model.lean

@@ -7,7 +7,7 @@ import Spec.Courseware.Model.Info
 /-!
 # Courseware.Model —— 工程文件的内容模型
 
-留白基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
+基元(`Primitives`)、富内容锚点(`RichContent`)、原子单位(`Element`)、单节课
 (`Lesson`)、课时元信息(`Info`:canonical author 为列表 vs `RawInfo` 撰写态)。
 决策出处 ADR-0005 / 0006 / 0008。
 -/

spec/Spec/Courseware/Model/Element.lean

@@ -3,7 +3,7 @@ import Spec.Courseware.Model.Primitives
 /-!
 # Element —— 课程内容的原子单位
 
-ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。本模块把它编码成
+ADR-0005:element 实例 = 一个 kind 标签 + 符合该 kind schema 的数据。把它编码成
 依赖结构,使"数据必须匹配其 kind"成为类型层面的事实而非运行时校验。
 -/
 

spec/Spec/Courseware/Model/Info.lean

@@ -5,7 +5,7 @@
 基数**是一个真分歧点:一节课可由多人(教研组)署名,故 canonical 模型里 author 是一个
 **有序列表**,不是单值或可选单值。
 
-另有一条值得钉的模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
+另一条模式:on-disk 的**撰写态**(用户实际填写的形态)是**语法糖**——单作者可写
 `author = "…"`,多作者写 `author = ["…", "…"]`——但这个"字符串或数组"的二态**只活在加载
 边界**:`RawInfo` 经归一化折叠成 canonical `Info`,其后不再出现。canonical 接收端始终是
 `List String`,raw 形式不泄漏进模型其余部分。这正是 `Info`(canonical)与 `RawInfo`
@@ -24,7 +24,7 @@ inductive RawAuthor where
   | many (names : List String)
 
 /-- raw 作者归一化为**有序作者列表**(`PINNED`, ADR-0008)。单作者 ⇒ 单元素列表;数组
-⇒ 原样。这条钉死"canonical 接收端始终是 `List String`"。 -/
+⇒ 原样。canonical 接收端始终是 `List String`。 -/
 def RawAuthor.normalize : RawAuthor → List String
   | .one n => [n]
   | .many ns => ns

spec/Spec/Courseware/Model/Primitives.lean

@@ -1,26 +1,26 @@
 /-!
-# Primitives —— Courseware 契约的留白基元
+# Primitives —— Courseware 契约的基元
 
 课程工程文件模型(ADR-0005)依赖一组基元:element kind 怎么标识、某 kind 的数据
 schema 是什么、export target 怎么标识。收口成载体 `Primitives`,让模型在其上参数化
 ——契约谈得了 element / lesson / 渲染**之间的关系**,而把每个基元的**内部表示**留给
-实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 钉死)与其表示进 Lean
+实现。注意:某基元语义已 PINNED(如 schema 形态由 ADR-0006 固定)与其表示进 Lean
 是两回事——JSON Schema / typst 的内部结构属实现细节,不入 Lean,故基元在此仍以抽象
-类型承载。富内容的 prose 母本见 `Courseware.RichContent`。
+类型承载。富内容的母本见 `Courseware.RichContent`。
 -/
 
 namespace Spec.Courseware
 
 /-- Courseware 契约基元载体(关系 `PINNED`, ADR-0005;各基元表示留给实现, ADR-0006)。 -/
 structure Primitives where
-  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。刻意用抽象
+  /-- element kind 标识(`PINNED` **开放宇宙**, ADR-0005;表示 `OPEN`)。用抽象
       类型而非 `inductive`:ADR-0005 决定 kind 是开放可扩展宇宙(stdlib + 第三方),
       封闭枚举会违背它——此处开放是**已决策的**(区别于 `RunState` 的"尚未封闭")。 -/
   KindId : Type
   /-- 某 kind 的合法数据类型(`PINNED` 依赖关系, ADR-0005;schema 形态 `PINNED`
       ADR-0006,表示仍抽象)。以 kind 为索引:`ElementData k` 即"符合 `k` schema 的
-      数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)是 ADR-0006
-      钉死的,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
+      数据"。schema 形态(声明式 JSON Schema + `content` 叶子 = typst 源)由 ADR-0006
+      固定,但属 JSON/typst 内部结构、实现细节,不进 Lean;契约只锚定"数据符合
       kind schema"这条关系,故此处仍是抽象类型。 -/
   ElementData : KindId → Type
   /-- export target 标识(`PINNED` 角色, ADR-0005;表示 `OPEN`)。一个 target 是一次

spec/Spec/Courseware/Model/RichContent.lean

@@ -1,5 +1,5 @@
 /-!
-# RichContent —— 富内容(ADR-0006 的 prose 母本)
+# RichContent —— 富内容(ADR-0006 的母本)
 
 ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**源文本**,
 按其 **format** 决定语义(ADR-0015)。两种 format:
@@ -13,7 +13,7 @@ ADR-0006:element schema 的"叶子"可以是 `content` 类型,其值是一段**
 的一等文件,坐落在一个**虚拟路径**上;相对 import 限本工程路径结构内 + `@package`(不跨工程)。markdown format
 的富内容不参与 typst 求值,但同样由一个虚拟路径定位(供 markdown 装配 step 按序读取,见 `Export/Render`)。
 
-本模块只立 prose 锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
+只立锚点 + 最小抽象签名:typst 的 `Content`/`Module` 内部结构、JSON Schema 形状、format 的
 具体判别属实现细节,不进 Lean,只承诺"富内容由一个虚拟路径定位"+"叶子带 format"这两条关系。
 -/
 
@@ -33,8 +33,8 @@ inductive ContentFormat where
   | markdown
 
 /-- 对一段富内容的**引用**:它坐落在某个虚拟路径上(`PINNED` 关系, ADR-0006),并带一个
-**format**(`PINNED`, ADR-0015)。刻意**不**建模源文本、不建模求值出的 `Content`(那是实现侧的事);
-只钉"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
+**format**(`PINNED`, ADR-0015)。不建模源文本、不建模求值出的 `Content`(那是实现侧的事);
+"富内容经由一个 `VPath` 定位 + 带 format",作为 `Primitives.ElementData` 里 `content` 叶子的语义锚点。 -/
 structure RichContentRef where
   /-- 该富内容所在的虚拟路径(ADR-0006;落盘后为真实相对路径, ADR-0007)。 -/
   vpath : VPath

spec/Spec/Courseware/Open.lean

@@ -2,8 +2,8 @@ import Spec.Courseware.Open.QuestionBank
 import Spec.Courseware.Open.Course
 
 /-!
-# Courseware.Open —— 留白骨架(核心关系 OPEN)
+# Courseware.Open —— OPEN 骨架(核心关系)
 
 题库与 element 的关系(`QuestionBank`)、课程编排规则(`Course`)。两者均为已 surface
-但未决策的分歧点,按宪法第 2 条不臆造,待专门 ADR 落定。
+但未决策的 OPEN 分歧点,待专门 ADR 落定。
 -/

spec/Spec/Courseware/Open/Course.lean

@@ -5,6 +5,6 @@ ADR-0005:工程文件的粒度是**单节课**;course / 单元**不是**工程
 **编排**。但"编排"的具体规则未决策:有序列表还是带层级(单元 → 课)的树?lesson 被
 引用还是被包含?跨 lesson 有无约束(目标覆盖、前后置)?这些都是 `OPEN`。
 
-按宪法第 2 条本模块**不臆造**编排结构——不建 `Course := List Lesson`(那会偷偷承诺
+此处不替它选解——不建 `Course := List Lesson`(那会偷偷承诺
 "扁平有序、无层级")。只在此 surface:课程编排待专门 ADR。本文件当前不引入任何承诺性声明。
 -/

spec/Spec/Courseware/Open/QuestionBank.lean

@@ -5,6 +5,6 @@
 典型的可复用单元,lesson 会引用它。但**题库与 element 的关系尚未决策**,且用户明确
 指出"纯引用可能不够"——element 内联题目数据 / lesson 持指向题库条目的引用 / 两者并存?
 
-这是一个 `OPEN` 分歧点。按宪法第 2 条本模块**不替它选解**——不建 `QuestionRef` 也不建
+这是一个 `OPEN` 分歧点。此处不替它选解——不建 `QuestionRef` 也不建
 内联结构,只在此 surface。待专门 ADR 落定后再填。本文件当前不引入任何承诺性声明。
 -/

spec/Spec/Prelude.lean

@@ -1,10 +1,10 @@
 /-!
 # Prelude —— System 层共享标识符
 
-平台层反复引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。其内部表示从未被决策
-(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque 载体
-`Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
-**关系**,却不对标识符表示作承诺。
+平台层引用一组标识符(项目、run、session、principal、chat、platform identity/audit)。
+其内部表示从未被决策(UUID / 复合键、principal 子类型学),也非分歧点,故收口成 opaque
+载体 `Identifiers`,System 各模块在其上参数化——契约谈得了"锁 owner 是哪个 run"这类
+关系,却不对标识符表示作承诺。
 -/
 
 namespace Spec.System
@@ -15,23 +15,33 @@ structure Identifiers where
   ProjectId : Type
   /-- SaaS 租户/组织标识(`OPEN` 表示;ADR-0020 tenant root)。 -/
   OrganizationId : Type
+  /-- 租户层用户标识(`OPEN` 表示;独立实体,非飞书身份派生;见 `Hierarchy.User`)。 -/
+  UserId : Type
+  /-- 飞书用户 open_id(`OPEN` 表示;单应用作用域内唯一)。 -/
+  FeishuOpenId : Type
+  /-- 飞书 user_id(`OPEN` 表示;租户内唯一,换 app 不变)。 -/
+  FeishuUserId : Type
+  /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
+  FeishuAppId : Type
+  /-- 飞书 app_secret 信封引用(`OPEN` 表示;ADR-0024)。 -/
+  FeishuAppSecretRef : Type
   /-- Hub teacher team 标识(`OPEN` 表示;ADR-0020 org-scoped team)。 -/
   TeamId : Type
   /-- Project explorer folder 标识(`OPEN` 表示;ADR-0021 透明组织节点,非权限资源)。 -/
   FolderId : Type
   /-- 一次 agent 任务的标识(`OPEN` 表示;锁的 owner、审计主体,`AgentRun`。provider 无关,
-  ADR-0017;`@Claude` 仅为触发品牌,不承诺 provider)。 -/
+  ADR-0017;`@bot` 仅为触发品牌,不承诺 provider)。 -/
   RunId : Type
   /-- 长生命周期 agent 会话标识(`OPEN` 表示;**provider/model 绑定, ADR-0017**——一次
   session 不跨 provider/model;切 model 即新 session,跨 session 连续性由 ADR-0003 项目
   记忆/锚点重建,不由 session 自带。同 provider/model 内可跨多 run 复用, ADR-0002)。 -/
   SessionId : Type
   /-- 权限主体标识(`OPEN` 表示及其子类型学;ADR-0004 的 user/chat/department/…
-      子类型学未定且非本层分歧点,纯 plumbing,故只留 opaque 键)。 -/
+      子类型学未定且非分歧点,故只留 opaque 键)。 -/
   Principal : Type
   /-- 飞书项目群 chat 标识(`OPEN` 表示;ADR-0001 协作空间、ADR-0003 锚点引用、
       ADR-0004 `feishu_chat` principal 三处共用同一实体。独立成载体而非 `Principal` 子
-      类型——principal 子类型学 OPEN 见上,本层不预设"chat 是 principal 的哪种子型")。 -/
+      类型——principal 子类型学 OPEN,这里不预设"chat 是 principal 的哪种子型")。 -/
   ChatId : Type
   /-- 平台管理员身份标识(`OPEN` 表示;ADR-0023,不复用客户 `User` 标识)。 -/
   PlatformIdentityId : Type

spec/Spec/System.lean

@@ -1,41 +1,49 @@
+import Spec.System.Hierarchy
 import Spec.System.ProjectGroup
 import Spec.System.Organization
+import Spec.System.User
+import Spec.System.Connections
 import Spec.System.ProjectWorkspace
 import Spec.System.Capacity
 import Spec.System.PlatformAdministration
-import Spec.System.Run
+import Spec.System.Agent.Run
+import Spec.System.Agent.AgentRole
+import Spec.System.Agent.Memory
+import Spec.System.Agent.AgentSurface
 import Spec.System.Lock
-import Spec.System.Memory
-import Spec.System.AgentSurface
 import Spec.System.Permission
 import Spec.System.PermissionGrant
 import Spec.System.Audit
 /-!
 # System —— Hub 平台层契约
 
-协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。likec4
-(`docs/architecture/likec4/`)已画出这一层的**结构**;本层只补 likec4 画不出的
-**语义分歧点**:
+协作与执行的平台:项目、飞书群、AgentRun、锁、权限、审计、按需上下文。
+likec4 已画出结构;这里补语义:
 
+- `Hierarchy` —— 三层主体:平台 → 组织 → 用户。
+- `User` —— 用户创建路径(管理员直接创建;飞书注册 `OPEN`)。
+- `Connections` —— 外部连接:提供商枚举(当前仅飞书) + 绑定/信息类型。
 - `ProjectGroup` —— project↔飞书群 1:1 长生命周期绑定(ADR-0001);群是协作空间,不持锁。
-- `Organization` —— SaaS tenant root(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
-  connection secret 使用本地主密钥信封与 fail-closed resolver(ADR-0024)。
+- `Organization` —— SaaS 租户(ADR-0020);project/team 单归属,TEAM grant 不跨 org;
+  connection secret 信封与 fail-closed resolver(ADR-0024);
+  owner/admin/member(`OrganizationRole`)及其管理规则(最后所有者保护)。
 - `ProjectWorkspace` —— org 后台 project explorer:folder 是透明组织节点,project 仍是权限边界
   (ADR-0021)。
 - `Capacity` —— platform ceiling 与 org policy 的分层限制、持久 admission request 状态和
   平台紧急工作负载制动(ADR-0022)。
 - `PlatformAdministration` —— 独立平台身份/会话、单一管理员角色、绑定邀请、最后管理员
   保护、fail-closed 平台审计与离线 emergency grant(ADR-0023)。
+- `AgentRole` —— org-scoped agent 角色配置 + 技能(ADR-0017/0018)。
 - `Run` —— AgentRun 状态与终止判定(状态集合完整性 OPEN)。
 - `Lock` —— 锁 owner=run(ADR-0002),及"持锁者必为非终止 run"的核心不变式。
-- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权的不变式。
+- `Memory` —— 按需上下文:锚点类别(ADR-0003)+ MCP 工具按 run/project 上下文授权。
 - `AgentSurface` —— agent 执行面被 run 的工作区所界定(ADR-0018);与 Lock 正交——
   Lock 限定并发,Surface 限定波及面。机制 OPEN。
-- `Permission` —— read⊂edit⊂manage 角色格、能力推导、单调性;force-release 在格外。
-- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)结构
-  (ADR-0004);role-capability 与 settings-policy 的组合规则 OPEN。
-- `Audit` —— customer Project/Run 审计有意从简(内容多为 plumbing,OPEN);Platform
-  Audit 由 `PlatformAdministration` 独立钉死。
+- `Permission` —— read⊂edit⊂manage 角色体系、能力推导、单调性;force-release 在格外。
+- `PermissionGrant` —— grant(resource×principal×role)与 settings(六 policy 旋钮)
+  (ADR-0004);组合规则 OPEN。
+- `Audit` —— customer Project/Run 审计从简(内容 OPEN);Platform Audit 由
+  `PlatformAdministration` 独立承载。
 
 标识符见 `Spec.Prelude`。决策出处:ADR-0001..0004, 0018, 0020..0024。
 -/

spec/Spec/System/Agent/AgentRole.lean

@@ -0,0 +1,60 @@
+import Spec.Prelude
+
+/-!
+# AgentRole —— Agent 角色与技能配置 (ADR-0017, ADR-0018)
+
+AgentRole 是 org-scoped 运行时配置:system prompt、tool allowlist、default model
+和 skill 绑定。通过 CLI 管理,不需重启进程生效。
+
+Role 的执行面(model/prompt/tools/skill 内容)变更时,该 role 的 active sessions
+归档——下次 run 不能在旧指令下创建的 provider context 上恢复。
+仅 label/排序变更不影响会话连续性(ADR-0017)。
+
+Run 时只读加载 role 选中的 skill 不可变版本到 run-scoped 目录,
+run 结束后删除(ADR-0018)。Skill 管理是 org-scoped;存储机制 `OPEN`。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- Agent 角色(`PINNED`, org-scoped, ADR-0017)。 -/
+structure AgentRole where
+  /-- 所属组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 斜杠命令名(`OPEN` 表示;如 /draft)。 -/
+  roleId : String
+  /-- system prompt(`PINNED`)。 -/
+  systemPrompt : String
+  /-- tool allowlist(`PINNED`;tool 标识集合 `OPEN`)。 -/
+  tools : List String
+  /-- 默认 model(`PINNED`;model ID 表示 `OPEN`)。 -/
+  defaultModel : String
+
+/-- Agent 技能(`PINNED`, org-scoped, ADR-0017/0018)。 -/
+structure AgentSkill where
+  /-- 所属组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 名称(`PINNED`)。 -/
+  name : String
+  /-- 版本(`PINNED`)。 -/
+  version : String
+  /-- 内容摘要(`PINNED`;SHA-256 content-addressed)。 -/
+  contentDigest : String
+  /-- 描述(`OPEN`)。 -/
+  description : String
+
+/-- Role-Skill 绑定(`PINNED`, ADR-0017)。一个 role 可绑定零或多个 skill。 -/
+structure AgentRoleSkillBinding where
+  /-- 所属组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 绑定的 role(`PINNED`)。 -/
+  roleId : String
+  /-- skill 名称(`PINNED`)。 -/
+  skillName : String
+  /-- skill 版本(`PINNED`)。 -/
+  skillVersion : String
+  /-- 排序(`PINNED`)。 -/
+  sortOrder : Nat
+
+end Spec.System

spec/Spec/System/Agent/AgentSurface.lean

@@ -0,0 +1,40 @@
+import Spec.Prelude
+import Spec.System.Agent.Run
+
+/-!
+# AgentSurface —— Agent 执行面边界(ADR-0018)
+
+Agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project 的工作区目录内
+(ADR-0007)。逃逸即越权,拒绝。
+
+与 `Lock`(ADR-0002)正交:Lock 限定并发(谁在改),Surface 限定波及面(能改到哪)。
+二者都按 run × project 作用域。
+
+shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论。机制
+——路径校验、OS 级沙箱、SDK 权限钩子,或其组合——`OPEN`(ADR-0018)。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers) (Path : Type)
+
+/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
+指向某路径;是否越权由下方 `Authorized` 约束。 -/
+structure AgentFileOp where
+  /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
+  run : I.RunId
+  /-- 操作目标路径(`PINNED`, ADR-0018)。 -/
+  path : Path
+
+
+/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
+(`PINNED` 安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 由平台提供
+(表示 `OPEN`);本谓词约束"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写
+宿主任意文件。 -/
+def AgentFileOp.Authorized
+    (op : AgentFileOp I Path)
+    (runWorkspace : I.RunId → Option Path)
+    (pathWithin : Path → Path → Prop) : Prop :=
+  ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
+
+end Spec.System

spec/Spec/System/Agent/Memory.lean

@@ -3,13 +3,13 @@ import Spec.Prelude
 /-!
 # Memory —— 按需上下文:锚点与项目记忆(ADR-0003)
 
-ADR-0003:Hub **只存锚点与项目记忆**,不存全量飞书消息历史;Claude 需要更多上下文时经
-飞书 API 按需读取。本模块刻画所存锚点的**类别**(ADR 列定,枚举完整性 OPEN——ADR 是
-"例如"式列举,新增类别不违反契约),并钉死一条 likec4 画不出的安全不变式:**MCP 工具
-按 run/project 上下文授权,Claude 不得传任意 chat id**(ADR-0003 Consequences 末条)。
+ADR-0003:Hub 只存锚点与项目记忆,不存全量飞书消息历史;Claude 需要更多上下文时经
+飞书 API 按需读取。这里刻画所存锚点的类别(ADR 列定,枚举完整性 OPEN),并约束
+一条安全不变式:MCP 工具按 run/project 上下文授权,Claude 不得传任意 chat id
+(ADR-0003 Consequences 末条)。
 
 "chat id 与 project 绑定"这一锚点类别由 `ProjectGroup.GroupBinding`(ADR-0001)权威承载,
-本模块不重复声明,只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
+这里只覆盖其余飞书侧指针(触发消息、状态卡片、回复、线程)。
 -/
 
 namespace Spec.System
@@ -17,9 +17,8 @@ namespace Spec.System
 variable (I : Identifiers)
 variable (MessageId CardId : Type)
 
-/-- 上下文锚点(`PINNED` 类别, ADR-0003 列定;**枚举完整性 `OPEN`**——ADR 是"例如"式
-列举,实现若需新类别须 surface,不得默认本枚举已穷尽)。承载 Hub 保留的飞书侧最小指针,
-而非消息正文。 -/
+/-- 上下文锚点(`PINNED` 类别, ADR-0003;枚举完整性 `OPEN`——ADR 是"例如"式列举,
+实现若需新类别须 surface)。承载 Hub 保留的飞书侧最小指针,而非消息正文。 -/
 inductive Anchor where
   /-- 触发某次 run 的消息(`PINNED` 类别, ADR-0003 "trigger message id")。 -/
   | triggerMessage : MessageId → Anchor
@@ -35,13 +34,11 @@ MCP tools to read … through Feishu APIs")。 -/
 structure McpReadRequest where
   /-- 发起请求的 run(授权上下文主体, ADR-0003)。 -/
   run : I.RunId
-  /-- 请求读取的 chat(是否允许越界由下方 `Authorized` 钉死:不允许)。 -/
+  /-- 请求读取的 chat(授权由下方 `Authorized` 约束:不允许越界)。 -/
   chat : I.ChatId
 
 /-- 请求获授权:其 chat 必须等于该 run 所属 project 的绑定群(`PINNED` 安全不变式,
-ADR-0003 Consequences "MCP tools must authorize by run/project context; Claude cannot
-pass arbitrary chat ids")。`runProject`/`boundChat` 由平台提供(表示 `OPEN`);本谓词只
-钉死"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id 越权读取。 -/
+ADR-0003)。"chat 必须匹配 run 的 project 绑定",杜绝 Claude 传任意 chat id。 -/
 def McpReadRequest.Authorized
     (req : McpReadRequest I)
     (runProject : I.RunId → Option I.ProjectId)

spec/Spec/System/Agent/Run.lean

@@ -1,16 +1,16 @@
 /-!
 # Run —— AgentRun 状态机
 
-一次 `@Claude` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
-合法转移关系在任何 ADR / likec4 散文里都未定下,故本模块只刻画**状态**与**终止
-判定**(后者是 Lock 排他不变式的依赖),不臆造转移边。
+一次 `@bot` 创建一个 `AgentRun`(ADR-0001),它在终止时释放项目锁(ADR-0002)。
+转移关系在任何 ADR 里都未定,这里只刻画状态与终止判定(后者是 Lock 排他不变式的
+依赖),不定义转移边。
 -/
 
 namespace Spec.System
 
-/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022 + likec4;
-**完整性 `OPEN`**——散文从未声明"状态恰好这些";实现若需新状态(如 pending)须
-surface,不得默认本枚举已穷尽)。终止态见 `RunState.Terminal`。 -/
+/-- AgentRun 运行状态(状态名 `PINNED`, ADR-0001..0003, ADR-0022;完整性 `OPEN`
+——ADR 从未声明"状态就是这些";实现若需新状态(如 pending)须 surface)。终止态
+见 `RunState.Terminal`。 -/
 inductive RunState where
   | active
   | waitingForUser

spec/Spec/System/AgentSurface.lean

@@ -1,44 +0,0 @@
-import Spec.Prelude
-import Spec.System.Run
-
-/-!
-# AgentSurface —— Agent 执行面边界(ADR-0018)
-
-ADR-0001/0002/0004 覆盖"协作治理"直到 `triggerAgent`:谁能触发一次 run。但触发之后
-agent 在执行层面能干什么——读哪些文件、跑什么命令——任何 ADR / 散文都未定。ADR-0017
-落地时采用 Claude Code SDK 的 `bypassPermissions` + 全量 Read/Write/Bash/Glob/Grep,
-agent 的文件与 shell 面对宿主**无界**:spec 与 ADR 均未钉死边界。本模块补这一层。
-
-钉死的不变式:agent 在一次 run 内发起的文件操作,其路径必须落在该 run 所属 project
-的工作区目录内(ADR-0007:工程文件是目录树;此 ADR 固定"agent 操作落在该树内")。
-逃逸即越权,拒绝。与 `Lock`(ADR-0002)正交:Lock 限定**并发**(谁在改),Surface
-限定**波及面**(能改到哪)。二者都按 run × project 作用域。
-
-shell 面的边界(命令的文件效果同样不得逃逸工作区)是同一不变式的推论,但**机制**
-——路径校验工具包装、OS 级沙箱(bubblewrap/容器)、SDK 权限钩子,或其组合——`OPEN`
-(ADR-0018)。契约钉死不变式,不钉死机制。
--/
-
-namespace Spec.System
-
-variable (I : Identifiers) (Path : Type)
-
-/-- Agent 在一次 run 内发起的文件操作(`PINNED` 关系, ADR-0018)。由某 run 发起、
-指向某路径;是否越权由下方 `Authorized` 钉死。 -/
-structure AgentFileOp where
-  /-- 发起操作的 run(授权上下文主体, ADR-0018;与 `Lock` 同作用域 run × project)。 -/
-  run : I.RunId
-  /-- 操作目标路径(`PINNED` 字段, ADR-0018)。 -/
-  path : Path
-
-/-- 工作区边界良构:run 的文件操作路径必须落在该 run 所属 project 的工作区目录内
-(`PINNED` 平台核心安全不变式, ADR-0018)。`runWorkspace` 与 `pathWithin` 均由平台提供
-(表示 `OPEN`——路径如何表示、"在内"如何判定是纯 plumbing,非本层分歧点);本谓词只
-钉死"操作路径必须以 run 的工作区为根",杜绝 agent 越权读写宿主任意文件。 -/
-def AgentFileOp.Authorized
-    (op : AgentFileOp I Path)
-    (runWorkspace : I.RunId → Option Path)
-    (pathWithin : Path → Path → Prop) : Prop :=
-  ∃ w, runWorkspace op.run = some w ∧ pathWithin op.path w
-
-end Spec.System

spec/Spec/System/Audit.lean

@@ -1,21 +1,18 @@
 import Spec.Prelude
 
 /-!
-# Audit —— Project/Run 审计日志(有意从简)
+# Audit —— Project/Run 审计日志
 
-likec4 把 `AuditLog` 列为实体(`AgentRun -> AuditLog 'records lifecycle events'`),
-但**审计记录里装什么**(事件 schema、保留策略、可查询维度)在任何 ADR / 散文里都
-未决策,且大多是 plumbing——按分歧点测试不入契约。故本模块刻意几乎为空:只固定
-"审计以 run 为主体记录其生命周期事件"这一条已决策关系,其余 `OPEN`(留白本身是
-契约的一部分:承诺此处尚无答案、勿填)。
+审计记录里装什么(事件 schema、保留策略、可查询维度)在任何 ADR 里都未决策,
+且大多是实现细节。这里只固定"审计以 run 为主体记录其生命周期事件"这一条已决策
+关系,其余 `OPEN`。ADR-0023 的 Platform Audit 是另一个控制面,见
+`Spec.System.PlatformAdministration`,不复用本结构。
 -/
 
 namespace Spec.System
 
 /-- 审计条目的最小骨架(关系 `PINNED` / 内容 `OPEN`, likec4)。只承诺"一条审计记录
-关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`,待真实分歧点出现时由
-对应 ADR 落定。ADR-0023 的 Platform Audit 是另一个 fail-closed 控制面,见
-`Spec.System.PlatformAdministration`,不复用本结构。 -/
+关联到某个 run";事件类型、时间、actor、详情等字段 `OPEN`。 -/
 structure AuditEntry (I : Identifiers) where
   /-- 该审计条目所属的 run(`PINNED` 关系, likec4)。 -/
   run : I.RunId

spec/Spec/System/Capacity.lean

@@ -4,8 +4,8 @@ import Spec.Prelude
 # Capacity —— SaaS capacity admission and abuse controls (ADR-0022)
 
 初始生产服务共享有限的单机资源,但不能让一个 Organization 垄断容量或让无界输入拖垮
-其他租户。ADR-0022 钉死分层限制、持久 admission、显式背压和紧急制动的领域语义;
-具体数值必须由生产式容量测试校准,因此保持 `OPEN`,不得把未经验证的数字冒充契约。
+其他租户。ADR-0022 定义分层限制、持久 admission、显式背压和紧急制动;具体数值由
+生产式容量测试校准,保持 `OPEN`。
 -/
 
 namespace Spec.System

spec/Spec/System/Connections.lean

@@ -0,0 +1,24 @@
+import Spec.System.Connections.Prelude
+import Spec.System.Connections.Feishu
+
+/-!
+# Connections —— 连接绑定与用户信息
+
+组织/用户的外部连接。提供商枚举见 `Connections.Prelude`;
+飞书具体类型见 `Connections.Feishu`。
+-/
+
+namespace Spec.System
+
+
+/-- 组织连接绑定(`PINNED`)。 -/
+inductive ConnectionBinding (I : Identifiers) where
+  /-- 飞书(`PINNED`)。 -/
+  | feishu : FeishuAppBinding I → ConnectionBinding I
+
+/-- 用户连接信息(`PINNED`)。 -/
+inductive ConnectionProfile (I : Identifiers) where
+  /-- 飞书(`PINNED`)。 -/
+  | feishu : FeishuProfile I → ConnectionProfile I
+
+end Spec.System

spec/Spec/System/Connections/Feishu.lean

@@ -0,0 +1,31 @@
+import Spec.Prelude
+
+/-!
+# Feishu —— 飞书连接
+
+组织绑定一个飞书企业应用(1:1)。用户经此应用登录、调飞书 API。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+
+/-- 组织的飞书应用绑定(`PINNED`, 1:1)。 -/
+structure FeishuAppBinding where
+  /-- 飞书企业应用 app_id(`OPEN` 表示)。 -/
+  appId : I.FeishuAppId
+  /-- app_secret 信封引用(`PINNED`, ADR-0024)。 -/
+  appSecretEnvelope : I.FeishuAppSecretRef
+
+/-- 用户的飞书信息(`PINNED`)。 -/
+structure FeishuProfile where
+  /-- 应用内身份(`OPEN`);调 API 的直接句柄,换应用即变。 -/
+  openId : I.FeishuOpenId
+  /-- 租户内身份(`OPEN`);换应用不变,比 open_id 稳定。 -/
+  userId : I.FeishuUserId
+  /-- 显示名(`OPEN`)。 -/
+  name : Option String
+  /-- 头像 URL(`OPEN`)。 -/
+  avatarUrl : Option String
+
+end Spec.System

spec/Spec/System/Connections/Prelude.lean

@@ -0,0 +1,15 @@
+/-!
+# Connections.Prelude —— 连接提供商
+
+用户/组织的外部身份连接。当前仅 IdP 类别(飞书)。
+模型 provider connection 是独立概念,见 `Spec.System.Organization`。
+-/
+
+namespace Spec.System
+
+/-- 连接提供商(`PINNED`;当前仅飞书,未来可扩展钉钉/企微)。 -/
+inductive ConnectionProvider where
+  /-- 飞书(`PINNED`)。 -/
+  | feishu
+
+end Spec.System

spec/Spec/System/Hierarchy.lean

@@ -0,0 +1,46 @@
+import Spec.Prelude
+import Spec.System.Connections
+
+/-!
+# Hierarchy —— 主体层级
+
+整个服务中的主体: 平台 → 组织(租户)→ 用户。
+
+- **平台**(Platform): SaaS 提供方实体
+
+- **组织**(Organization): SaaS 租户
+
+- **用户**(User): 租户内的独立实体
+
+**术语**: "管理员"一词在文档中不单独出现，避免跨层歧义。
+-/
+
+namespace Spec.System
+
+variable (I : Identifiers)
+/-- 平台(`PINNED`, SaaS 提供方)。只有一个,独立于组织。管理面见 `PlatformAdministration`(ADR-0023)。 -/
+structure Platform where
+  /-- 平台自有飞书应用(`PINNED`, ADR-0023)。 -/
+  application : I.PlatformFeishuApplicationId
+/-- 组织(`PINNED`, ADR-0020)。project/team 必须归属且仅归属一个 org。
+外部连接见 `Connections`。角色/tenancy/凭据见 `Spec.System.Organization`。 -/
+structure Organization where
+  /-- 组织标识(`OPEN` 表示)。 -/
+  id : I.OrganizationId
+  /-- 外部连接(`PINNED`)。 -/
+  connections : List (ConnectionBinding I)
+
+/-- 用户(`PINNED`, 租户层独立实体)。必属一个组织。外部连接见 `Connections`。 -/
+structure User where
+  /-- 用户标识(`OPEN` 表示;组织内唯一,不可改;登录用)。 -/
+  id : I.UserId
+  /-- 所属组织(`PINNED`, ADR-0020)。 -/
+  organization : I.OrganizationId
+  /-- 显示名(`PINNED`, 可改)。 -/
+  displayName : String
+  /-- 密码哈希(`OPEN` 表示;id + 密码登录)。 -/
+  passwordHash : String
+  /-- 外部连接(`PINNED`)。 -/
+  connections : List (ConnectionProfile I)
+
+end Spec.System

spec/Spec/System/Lock.lean

@@ -1,35 +1,32 @@
 import Spec.Prelude
-import Spec.System.Run
+import Spec.System.Agent.Run
 
 /-!
 # Lock —— 项目锁与排他不变式
 
-ADR-0002 的核心:防止并发 Claude 同改一个项目,锁的 **owner 是当前 `AgentRun`**
-(不是 teacher / chat / session)。本模块把这条决策编码进类型,并钉死那条
-likec4 画不出的语义不变式——**持锁者必为非终止 run**。
+ADR-0002:防止并发 agent 同改一个项目,锁的 owner 是当前 `AgentRun`(不是
+teacher / chat / session)。持锁者必为非终止 run。
 -/
 
 namespace Spec.System
 
 variable (I : Identifiers)
 
-/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`(非 SessionId/Principal)从类型
-上编码"lock owner = run_id":锁不可能被 session / teacher 持有。 -/
+/-- 项目级锁(`PINNED`, ADR-0002)。`owner : RunId`从类型上编码"lock owner = run_id":
+锁不可能被 session / teacher 持有。 -/
 structure ProjectAgentLock where
-  /-- 作用域:项目级(`PINNED`, ADR-0002 `scope = project_id`)。 -/
+  /-- 作用域:项目级(`PINNED`, ADR-0002)。 -/
   scope : I.ProjectId
-  /-- 持有者:一个 run(`PINNED`, ADR-0002 `owner = run_id`)。 -/
+  /-- 持有者:一个 run(`PINNED`, ADR-0002)。 -/
   owner : I.RunId
 
 /-- 锁表:每项目当前持锁 run(`PINNED` 排他性, ADR-0002)。`ProjectId → Option RunId`
-的结构**本身**即排他——不可能为同一项目登记两个并发 owner。 -/
+的结构本身即排他——不可能为同一项目登记两个并发 owner。 -/
 def LockTable := I.ProjectId → Option I.RunId
 
-/-- 锁表良构:**持锁者必为非终止 run**(`PINNED` 平台核心不变式, ADR-0002)。
+/-- 锁表良构:持锁者必为非终止 run(`PINNED`, ADR-0002)。
 
-"锁在 run 终止时释放"的逻辑等价物:若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。这条
-把 Lock 与 Run 耦合起来——likec4 能画"run owns lock while running",画不出"终止即
-必须释放"这个约束;它正是契约相对结构图的增量。 -/
+若 `p` 的锁被 `r` 持有,则 `r` 不在终止态。锁在 run 终止时释放。 -/
 def LockTable.WellFormed
     (lt : LockTable I) (statusOf : I.RunId → RunState) : Prop :=
   ∀ p r, lt p = some r → ¬ (statusOf r).Terminal

spec/Spec/System/Organization.lean

@@ -1,18 +1,12 @@
 import Spec.Prelude
 
 /-!
-# Organization —— SaaS tenant root (ADR-0020, ADR-0024)
+# Organization —— SaaS 租户 (ADR-0020, ADR-0024)
 
-ADR-0020:Hub 长期按 SaaS 形态演进,`Organization` 是客户侧 tenant root。
-`Project` 与 `Team` 都必须归属且只归属一个 organization;team 对 project 的授权
-必须在同一 organization 内。平台运营控制面(platform staff / break-glass / 账单)
-不复用 project 的 `read/edit/manage` 角色格,而是另一个控制面。
-
-本模块只钉死会造成实现分歧的不变量:tenant root 存在、project/team 单归属、team grant
-不得跨 org,以及 model provider connection 的凭据归属模式。用户身份、外部目录
-provider 细节仍为 `OPEN`;平台控制面身份/角色/审计已由 ADR-0023 与
-`Spec.System.PlatformAdministration` 独立决定。连接凭据的本地主密钥信封、不可变版本、
-writer authority 与 fail-closed resolver 由 ADR-0024 固定。
+组织就是租户。project/team 必须归属且仅归属一个 org;team→project grant 必须同 org。
+组织实体见 `Hierarchy.Organization`;用户见 `Spec.System.User`;平台控制面见
+`PlatformAdministration`(ADR-0023)。凭据信封见 ADR-0024。Agent 角色配置见
+`Spec.System.Agent.AgentRole`。
 -/
 
 namespace Spec.System
@@ -41,19 +35,17 @@ structure TeamProjectGrantScope where
   project : I.ProjectId
   /-- 获得授权的 team principal(`PINNED`, ADR-0020)。 -/
   team : I.TeamId
-
 /-- Team-project grant 是良构的 iff project 与 team 解析到同一 organization
-(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);本谓词钉死
-跨 org team grant 必须被拒绝。 -/
+(`PINNED`, ADR-0020)。`projectOrg`/`teamOrg` 由平台提供(表示 `OPEN`);跨 org
+team grant 必须被拒绝。 -/
 def TeamProjectGrantScope.WellScoped
     (grant : TeamProjectGrantScope I)
     (projectOrg : I.ProjectId → Option I.OrganizationId)
     (teamOrg : I.TeamId → Option I.OrganizationId) : Prop :=
   ∃ o, projectOrg grant.project = some o ∧ teamOrg grant.team = some o
 
-/-- Organization 的 model provider 凭据归属模式(`PINNED`, ADR-0021):BYOK 由 org
-管理员提供和管理;platform-managed 由平台管理员为该 org 单独提供和管理。两种模式
-都不允许无关 org 共用 process-global provider key。模式切换过程仍为 `OPEN`。 -/
+/- BYOK 由组织所有者/管理员管理;platform-managed 由平台管理员管理。两种模式都不允许
+跨 org 共用 process-global key。模式切换 `OPEN`。 -/
 inductive ProviderCredentialMode where
   | byok
   | platformManaged
@@ -78,7 +70,7 @@ inductive OrganizationConnectionStatus where
 
 /-- Organization secret version 的信封绑定上下文(`PINNED`, ADR-0024):认证附加数据必须
 同时绑定 organization、connection、secret version 与 purpose,因此密文不能跨行、跨 org、
-跨 connection 或跨用途替换。各标识符的数据库表示属于 plumbing,这里保持 opaque。 -/
+跨 connection 或跨用途替换。各标识符的数据库表示为实现细节,这里保持 opaque。 -/
 structure OrganizationSecretBinding
     (OrganizationId ConnectionId SecretVersionId Purpose : Type) where
   /-- secret 所属 organization(`PINNED`, ADR-0024)。 -/
@@ -104,4 +96,34 @@ def OrganizationSecretResolvable
   organizationActive && connectionActive &&
     (binding.organization == requestedOrganization) && authenticatedEnvelope
 
+
+/-- 组织成员角色(`PINNED` 封闭三档)。与项目层 `Role`、平台层 `PlatformRole` 互不相交。 -/
+inductive OrganizationRole where
+  /-- 组织所有者(`PINNED`):bootstrap,独家管 owner 群体,受最后所有者保护。 -/
+  | owner
+  /-- 组织管理员(`PINNED`):管成员/policy/BYOK,不能管 owner 群体。 -/
+  | admin
+  /-- 组织成员(`PINNED`):普通成员。 -/
+  | member
+
+/-- 组织成员关系(`PINNED`)。 -/
+structure OrganizationMembership where
+  /-- 成员(`PINNED`;独立实体,见 `Hierarchy.User`)。 -/
+  user : I.UserId
+  /-- 组织(`PINNED`)。 -/
+  organization : I.OrganizationId
+  /-- 角色(`PINNED`)。 -/
+  role : OrganizationRole
+
+/-- 只有组织所有者能管 owner 群体(`PINNED`)。 -/
+def CanManageOwnerGroup (actorRole : OrganizationRole) : Prop :=
+  actorRole = .owner
+
+/-- 最后所有者保护(`PINNED`):撤销 owner 时同 org 必须还有一个不同的 owner。 -/
+def LastOwnerProtected
+    (target : OrganizationMembership I)
+    (otherOwnersInOrg : List I.UserId) : Prop :=
+  target.role ≠ .owner ∨
+    ∃ other, other ∈ otherOwnersInOrg ∧ other ≠ target.user
+
 end Spec.System

spec/Spec/System/Permission.lean

@@ -5,8 +5,7 @@ import Spec.Prelude
 
 ADR-0004:权限走"飞书云文档式"——grant(`resource + principal + role`)与 settings
 分离;role 取自封闭的 `read / edit / manage`,且 **read ⊂ edit ⊂ manage** 累积赋能;
-强制释放锁是 **admin-only**,在 role 体系之外。本模块把这套结构与"高 role 含低
-role 全部能力"的单调性钉死。
+强制释放锁是 **admin-only**,在 role 体系之外。
 -/
 
 namespace Spec.System

spec/Spec/System/PermissionGrant.lean

@@ -4,16 +4,14 @@ import Spec.System.Permission
 /-!
 # PermissionGrant —— 授权与设置(ADR-0004)
 
-ADR-0004 的"飞书云文档式"权限:**grant**(`resource × principal × role`)与 **settings**
-(各 policy 旋钮)分离;role 决定"谁能"(能力,见 `Permission`),settings 决定"此资源
-是否开某类操作"(策略)。本模块把 grant/settings 的结构钉死——`Permission` 已落 role 能
-力格,本模块补"授权如何挂到资源/主体上"。
+ADR-0004 的"飞书云文档式"权限:grant(`resource × principal × role`)与 settings
+(各 policy 旋钮)分离;role 决定能力(见 `Permission`),settings 决定"此资源是否
+开某类操作"。
 
-principal 子类型学(user/chat/department/…)与各 policy 值域均为 `OPEN`(ADR 未定,非本
-层分歧点)。**role-capability 与 settings-policy 如何组合成最终授权决策**亦 `OPEN`——
-ADR-0004 把二者列为分离的闸,但未明文规定组合规则(AND?settings 能否超出 role?),实现
-须 surface,不得默认。ADR-0020 另行钉死 TEAM principal 授权 PROJECT resource 时必须
-同 organization;该 tenant well-scopedness 见 `Spec.System.Organization`。
+principal 子类型学(user/chat/department/…)与各 policy 值域 `OPEN`。role-capability
+与 settings-policy 如何组合成最终授权决策亦 `OPEN`——ADR-0004 把二者列为分离的闸,
+但未明文规定组合规则。ADR-0020 约束 TEAM principal 授权 PROJECT resource 时必须同
+organization,见 `Spec.System.Organization`。
 -/
 
 namespace Spec.System
@@ -45,9 +43,8 @@ structure PermissionGrant where
   role : Role
 
 /-- 资源策略设置(`PINNED` 结构 + 六旋钮, ADR-0004 `PermissionSettings`):与 grant 分离,
-控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定,非本层
-分歧点)。共享同一 opaque `Policy` 类型:契约只钉死"旋钮存在且相互独立",不钉死"各旋钮
-值域互异"——值域是实现/后续 ADR 的事。 -/
+控制"此资源是否开某类操作"。六旋钮由 ADR 逐字列名;各旋钮值域 `OPEN`(ADR 未定)。
+共享同一 opaque `Policy` 类型:契约只约束"旋钮存在且相互独立";值域是实现/后续 ADR 的事。 -/
 structure PermissionSettings where
   /-- 设置所属资源(`PINNED`, ADR-0004)。 -/
   resource : Resource I ArtifactId

spec/Spec/System/PlatformAdministration.lean

@@ -8,8 +8,8 @@ import Spec.Prelude
 单一平级管理员角色、绑定身份的 invitation、可撤销服务端 session、mutation 与平台审计
 同成同败、最后管理员保护,以及无常驻账号的双因子离线恢复。
 
-本模块只钉死这些会导致安全边界分歧的语义。cookie 属性、token hash、具体 TTL、审计
-字段表示/保留期、recovery key 介质和 CLI/SQL 机制仍为 `OPEN`,由对应实现决策承载。
+这些安全边界语义见下。cookie 属性、token hash、具体 TTL、审计
+字段表示/保留期、recovery key 介质和 CLI/SQL 机制 `OPEN`。
 -/
 
 namespace Spec.System

spec/Spec/System/ProjectGroup.lean

@@ -3,26 +3,23 @@ import Spec.Prelude
 /-!
 # ProjectGroup —— 飞书项目群作为协作空间(ADR-0001)
 
-ADR-0001 的核心:一个 project 对应一个**长生命周期**飞书项目群;群是协作空间,**不是锁
-owner**(锁归 `AgentRun`,见 `Lock` / ADR-0002),不是临时处理 session。群可在无 Claude
-处理时保持开启;教师离群/静音与项目权限、与 Claude 生命周期相互独立。本模块钉死
-project↔group 的**active**一对一绑定——likec4 画得出"project has group",画不出"恰好一个、
-且群不持锁"。
+一个 project 对应一个长生命周期飞书项目群;群是协作空间,不持锁(锁归 `AgentRun`,
+见 `Lock` / ADR-0002)。群可在无 agent 处理时保持开启;教师离群/静音与项目权限、
+与 agent 生命周期相互独立。
 
-**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可以保留 archived
-historical binding rows 供审计/纠错,但 `GroupBinding` 谓词只刻画当前 active 快照。
-群解散/不可达的自动化处理仍为 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
+**绑定历史(`PINNED`, ADR-0021):** active binding 严格 1:1;实现可保留 archived
+historical binding rows 供审计,但 `GroupBinding` 谓词只刻画当前 active 快照。
+群解散/不可达的自动化处理 `OPEN`;pilot 纠错由 org admin 显式归档绑定。
 -/
 
 namespace Spec.System
 
 variable (I : Identifiers)
 
-/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的绑定;
-**不是锁 owner**(锁归 `AgentRun`,见 `Lock`);不是临时 session。 -/
+/-- 飞书项目群(`PINNED` 长生命周期协作空间, ADR-0001)。承载 project 与飞书 chat 的
+绑定;不持锁(锁归 `AgentRun`,见 `Lock`)。 -/
 structure ProjectGroup where
-  /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001 "one project has one Feishu project
-  group";chat 标识见 `Identifiers.ChatId`)。 -/
+  /-- 群对应的飞书 chat(`PINNED` 关系, ADR-0001;chat 标识见 `Identifiers.ChatId`)。 -/
   chat : I.ChatId
 
 /-- 项目↔active 群绑定表(`PINNED` 每项目至多一个 active 群, ADR-0001/0021)。
@@ -30,9 +27,9 @@ structure ProjectGroup where
 自带);良构补另一半——单射。 -/
 def GroupBinding := I.ProjectId → Option I.ChatId
 
-/-- Active 绑定良构:**单射**——不同 project 不绑同一 active chat(`PINNED` 1:1 的另一半,
-ADR-0001/0021)。"每 project 至多一个群"由 `Option` 结构自带;这条钉死"每群至多属于一个
-project"。archived historical bindings 不在本快照不变式内。 -/
+/-- Active 绑定良构:单射——不同 project 不绑同一 active chat(`PINNED`, ADR-0001/0021)。
+"每 project 至多一个群"由 `Option` 结构自带;这条约束"每群至多属于一个 project"。
+archived historical bindings 不在本快照不变式内。 -/
 def GroupBinding.WellFormed (b : GroupBinding I) : Prop :=
   ∀ p₁ p₂ c, b p₁ = some c → b p₂ = some c → p₁ = p₂
 

spec/Spec/System/ProjectWorkspace.lean

@@ -3,12 +3,11 @@ import Spec.Prelude
 /-!
 # ProjectWorkspace —— project explorer 与飞书建项入口(ADR-0021)
 
-ADR-0021 把 org 后台里的"文件管理器式"项目管理收口为透明 folder + project:
-folder 只负责导航、排序、层级与用量聚合,当前不是权限资源。project 仍是授权边界。
+org 后台里的"文件管理器式"项目管理:folder 只负责导航、排序、层级与用量聚合,当前
+不是权限资源。project 仍是授权边界。
 
-本模块只钉死会影响实现分歧的不变量:folder/project 同 org、folder 不参与权限、普通成员
-从飞书群创建 project 必须受 org policy 控制。folder visibility/team policy/继承授权仍为
-未来扩展,不得在当前实现中半隐式加入。
+不变量:folder/project 同 org、folder 不参与权限、普通成员从飞书群创建 project 受
+org policy 控制。folder visibility/team policy/继承授权 `OPEN`。
 -/
 
 namespace Spec.System
@@ -39,7 +38,7 @@ def ProjectFolderPlacement.WellScoped
   ∃ o, projectOrg placement.project = some o ∧ folderOrg placement.folder = some o
 
 /-- Folder 当前透明(`PINNED`, ADR-0021):folder 不是权限资源,不持有 grants,移动 project
-不改变 project 自身授权。未来 folder policy 若出现,必须新增显式语义而不是复用本谓词。 -/
+不改变 project 自身授权。未来 folder policy 若出现,须新增显式语义。 -/
 structure FolderTransparent where
   /-- 透明性命题本身;字段存在是为了让 contract 明确可引用(`PINNED`, ADR-0021)。 -/
   current : True

spec/Spec/System/User.lean

@@ -0,0 +1,12 @@
+import Spec.Prelude
+
+/-!
+# User —— 用户创建路径
+
+用户实体见 `Hierarchy.User`;外部连接见 `Spec.System.Connections`。
+
+用户创建当前只定义管理员直接创建;飞书自助注册→管理员审批 `OPEN`。
+-/
+
+namespace Spec.System
+end Spec.System