Repository navigation
DEN-3970: Complete Zed platform onboarding, shared services, discovery, and repository boundaries #61
Description
Activity
Rust/formal-methods follow-up: formalize the real browser mutation boundary in zed-web-server.rs under DEN-3970. Confirmed 303 success/authentication ambiguity and lost rotated-session cookie after delegation failure. Plan explicit Rust outcomes, same-principal cookie preservation, a schema-v1 fmctl manifest, finite Quint/TLC model with non-vacuous witnesses, and a complete bounded outcome matrix against the async Rust implementation. Preserve customer/admin separation and keep this umbrella open; this is not a claim that the platform or all-org audit is complete.
Current-default-branch formal inventory, 2026-09-05. This is discovery, not a claim that every repository has been exhaustively audited. Enumerated all repositories (no remaining GraphQL pages) in the four named organizations: zed-pkg: 37, daedalus-fab: 26, quaestor-ledger: 27, shared-auth: 29. Total 119. Sixteen had a root formal/ tree at the observed heads, before merging Zed web PR #48.
Repository Exact observed main/default head Formal area zed-pkg/zed-cli 6aa3ed2a0a2f PROCEDURE.md, procedure.toml, review-procedure zed-pkg/zed-api-server.rs a990103b5b04 README.md, dependency_resolution.fm.toml, dependency_resolution.qnt, fm.toml, latest_selection.fm.toml, latest_selection.qnt, package_publication.qnt zed-pkg/zed-sync 8d2716ad170a README.md, app-lifecycle.fm.toml, app_lifecycle.qnt, fm.toml, write_lifecycle.qnt zed-pkg/zed-lock 3b1942119070 README.md, fm.toml, waiter_lifecycle.qnt daedalus-fab/fabrication-server.rs 5c516be49c3e PROCEDURE.md, README.md, procedure.toml, release_gate.qnt daedalus-fab/daedalus-clients 8f30b0be26ca README.md, client_sync.qnt, fm.toml, replay.py, test_replay.py, traces.json daedalus-fab/daedalus-sync 8a3320b78783 README.md, sync_protocol.qnt quaestor-ledger/quaestor-ledger-server.rs 36e8d370bd1a PROCEDURE.md, auth-contract, authz-model, ledger-model, procedure.toml, scheduler-model, shared-auth-runtime quaestor-ledger/quaestor-executor 018deec8d1ed PROCEDURE.md, procedure.toml quaestor-ledger/quaestor-api-server.rs ac9025b8c77a PROCEDURE.md, auth-contract, authz-model, ledger-model, procedure.toml, scheduler-model, shared-auth-runtime shared-auth/shared-auth-server.rs 2bbfcac8c46a auth-state-machines.md, review-procedure shared-auth/shared-auth-clients 511abec23ce8 AuthLifecycle.cfg, AuthLifecycle.tla, README.md, auth-lifecycle.json shared-auth/shared-auth-sync 561e495feace README.md, authority_reconciliation.qnt, fm.toml shared-auth/shared-auth-nats-bridge.rs bbae687da542 README.md, authenticated_delivery.fm.toml, authenticated_delivery.qnt, bridge_delivery.qnt, fm.toml shared-auth/shared-auth-formal 2a315881f473 dual_realm.qnt, echo.py, fm.toml, trace-0.itf.json shared-auth/shared-auth-session-formal 461acb316191 echo.py, fm.toml, session_lifecycle.qnt, trace-0.itf.json Zed web PR zed-pkg/zed-web-server.rs#48 adds the requested additional consumer, with a manifest, finite model, real Rust BFF replay and negative controls. This inventory only detects the governed root formal/ location; models elsewhere and all other accessible organizations remain part of the broader audit.
The referenced ORESoftware/k8s-server repository returned 404 with current access. The accessible ORESoftware/k8s-cluster contains remote/deployments/formal-methods-server-rs and formal-methods-service-rs, while the reusable runner is ORESoftware/formal-methods.rs.
Confirmed follow-ups are preserved in DEN-565 (verifier bundled protobuf warning; ORESoftware/formal-methods.rs#3) and amended DEN-97 (standalone echo slots must be reconciled with existing canonical Shared Auth runtime models; no duplicate authentication model). Linear refused a new child because of the workspace free-issue limit; the existing correct-project ticket was amended instead.
Implementation PR: zed-pkg/zed-web-server.rs#48 at 4a9aedd2986b04059976127fc6f648d170194f38. The fetched remote main profile change was semantically retained by a normal merge. Hosted formal mutation safety, Rust tests, source-policy lint, agent-policy checks, and graph controls are green; the container build is still running. Local tests, strict Clippy, docs, release build, both fmctl runners, generated Rust replay, negative controls, and desktop/mobile preview passed. Additional correct-project audit tracking: ORESoftware/formal-methods.rs#3 with DEN-565; shared-auth/shared-auth-formal#1 with amended DEN-97. Keep the umbrella open.
Completed customer-web/Rust formal slice: PR #48 merged as 0251593c9f0d44d75cfa2544349a2ef9c2f89db7 after all six hosted checks passed, including the container build. The working checkout is synchronized with freshly fetched origin/main and clean. The merge tree matches the exact verified PR head. Temporary loopback UI preview was stopped. Remaining web PRs (#47, #46, #43, #42, #40) and full-fleet/platform scope are still open; #47 is an older independent clone salvage with legacy deployment/lint files, not a duplicate of the new onboarding/formal implementation, and was not blindly merged or closed.
Continuation plan (2026-09-05): connect the marketing site to the merged customer onboarding flow.\n\nCurrent evidence: zed-pkg.github.io origin/main f0f7d1c is current and clean; zed-web-server.rs origin/main 0251593 contains /onboarding/individual and /onboarding/organization (PR #48). No existing marketing PR implements these entry paths. PRs #14/#17 carry older overlapping browser-test/lint work and remain preserved for semantic reconciliation; #16 targets a separate runtime distribution branch.\n\nImplementation:\n- Add an accessible, responsive marketing account page and homepage entry cards for individual and organization journeys, with exact customer-app login/signup return paths and a credential-free CLI alternative.\n- Keep customer organization owners distinct from platform administrators; do not invent org-domain routing, domain-based membership, or live-deployment claims.\n- Preserve no-JavaScript navigation. Audit the existing session hint as a presentation-only state machine: anonymous, authenticated, unknown, and unavailable must remain distinct; failures must not manufacture a signed-out result.\n- Bind link contracts to the merged Rust route/return-path behavior; add automated route/security/state tests and real-browser desktop/mobile/no-JS evidence.\n- Publish a focused PR with exact-revision checks, then merge through normal protection gates. Update this issue and the existing GitHub umbrella instead of creating duplicate Linear issues.\n\nExisting Python browser/HTML checks remain temporarily because this slice changes their exercised UI contract; use the established harness first. A future Rust contract-checker migration must preserve positive/negative fixtures and is part of the existing lint/contract-parity work, not a substitute for onboarding delivery.
Dependency hardening addendum for DEN-3970: the marketing build currently resolves Astro 5.18.2 and npm audit reports six affected packages (4 high, 1 moderate, 1 low). Upgrade the static toolchain using the official Astro 6/7 migration guides, regenerate the lockfile, and rerun all route, metadata, state, and browser contracts before landing. The hosted-account promotion gate remains false; the current customer image is published but public customer routes still return 404/503.
2026-09-05 — marketing account journeys merged and live
Merged zed-pkg.github.io PR #18 at
fd5fa2db58ca00867800f6e20dfeeec8d6c4a6d6. Local main is clean and equals freshly fetched origin/main. No conflict resolution or history deletion was needed.Delivered:
- Individual and organization account journeys, homepage/navigation entry points, membership/identity/admin separation, and no-JavaScript fallback.
- Exhaustively checked four-state marketing session hint: unknown, anonymous, authenticated, unavailable. Unavailable never means signed out. Exact origin, strict Boolean payload, 2 KiB streaming body limit, strict UTF-8/JSON, HTTP 200 only, redirect rejection, 10-second abort, and single-flight refresh.
- Locked Astro 7.3.1 / Node 24.19.0 build; strict checks, four unit-test groups, expanded real Chromium regression matrix, locked production install, and audit gates. npm audit reports zero current advisories across the resolved dependency graph; this is not a proof of absence of vulnerabilities.
- Regression evidence covers 14 failure classes from both initial signed-in and anonymous states, recovery, actual stalled-request timeout, refresh deduplication, mobile/desktop/keyboard/no-JavaScript journeys, and both rollout flag branches. Committed flag remains false.
Post-merge evidence:
- Production deployment: success.
- Main public-site/browser contract: success.
- Post-deployment live-site smoke: success.
- Direct production GET of https://zpkg.net/account/ returned 200; real production browser confirms canonical URL, both persona sections, zero forms, pending-deployment marker, and account state unavailable.
Still open:
Fresh unauthenticated GET probes at approximately 18:16 UTC show app.zpkg.net /, /auth/sign-in, /auth/session/status, /onboarding/individual, and /onboarding/organization returning 404; /login and /signup return 503. The merged Rust app and published image are not evidence that the public application is deployed correctly. Reconcile deployed origin/image/routing, verify exact Shared Auth return-path registration and credentialed CORS, and run synthetic real PKCE → customer API/DB onboarding including negative cases before enabling hosted CTAs. See account rollout contract.The GitHub merge automatically completed DEN-3970; restored it to In Progress because the broad cross-repository audit remains unfinished. This update amends existing DEN-3970 / DEN-1147 rather than creating a duplicate. Older marketing PRs #14, #17, and #16 remain preserved, not blindly merged: #17 references an absent lint dependency, and legacy browser coverage needs conceptual reconciliation with the current canonical opto-sync suite.
Continuation plan: trace the customer edge and harden WebSocket delivery in zed-infra. Existing 52 tests pass, but the shared origin proxy strips Upgrade/Connection before the upgrade branch and skips typed failure handling there. Reproduce; preserve real upgrade/socket and end-to-end headers; add bounded handshake setup with established-socket survival, denial/redirect tests, and finite transition conformance; land a tested PR. Deployment remains separate: the last Cloudflare workflow stopped at missing scoped credentials, the local OAuth identity lacks required lease/route permissions, and the AWS operator profile is expired. Do not bypass deployment leases, credential policy, or onboarding rollout gates.
2026-09-05 delivered: formally checked edge WebSocket handshakes
Merged zed-infra #42 as
4439ac332cacb12d696333948619e51fbc9b3ec0after all 11 hosted checks passed at exact head7b760473cf026d9eb3cdc9dd794004a31fb440e7. Overlapping rescue #41 is also merged through the explicitly reviewed history reconciliation599cd28.Audit reproduced and repaired stripped WebSocket upgrade headers, escaping transport failures, and a setup timer that could abort a live socket. The checked finite boundary rejects malformed upgrades before origin I/O, preserves origin authentication denials and manual redirects, and hands off only the exact origin 101 response with its runtime socket.
Evidence:
- Hosted CI: 57 unit groups including all 276 finite actual-handler cases, strict decision checking, and three real TCP/workerd/WebSocket suites for app/user/web. Locked dependency audit and infrastructure gates passed.
- Formal evidence: 276 initial scenarios, 736 distinct reachable states, complete depth 3; seven simulation witnesses; all 16 generated traces replayed through the production handler with zero mismatches.
- Both independent negative controls passed: actual TLC invariant violation for a redirect-policy mutant, and actual production/model mismatch for a corrupted terminal observation.
- Public fallback attestation passed after fixing its missing locked-runtime installation. All three Workers also passed pinned Wrangler dry-run bundling.
- Fresh standalone Rust fmctl at
734a1c3passed locally; hosted CI independently used the immutable public runner export. The upstream Quint/Apalache protobuf warning remains tracked by DEN-565.
Semantic merge: all nine rescue paths were compared. Maintenance paths, retry behavior, snapshot/If-Match/KV lease, deployment targets and tests were retained alongside newer public registry/CDN canaries, handshake fixes and formal gates. No rebase, force push, or lost history.
Production is NOT complete: post-merge deployment run 33985120868 failed at the scoped-identity preflight because
CLOUDFLARE_WORKERS_DEPLOY_TOKENis absent; no upload occurred. Local Cloudflare OAuth lacks the required lease/route scopes, and the approved dd-codex AWS session is expired. Do not bypass the lease path or enable hosted-account marketing until authorized promotion and real Shared Auth/API/DB onboarding acceptance pass.DEN-3970 remains In Progress. This is bounded handshake assurance, not proof of authentication, cryptography, distributed reconnection/backpressure, or full platform deployment. Other draft/rescue PRs remain open for semantic review; the separate runtime-cache-only rescue was not included.
Post-merge acceptance result
The merge commit also passed main CI and main formal verification. The main public-fallback attestation correctly remained red: its single required failure was the live registry canary returning HTTP 502 without the expected edge evidence. Direct GitHub, the deliberately origin-down local Worker fallback, the live CDN (byte-identical archive), and the public site passed. PR mode does not require the undeployed live registry; main mode does, and that distinction was preserved. This is an unresolved production routing/origin/deployment acceptance gap, not a reason to weaken the attestation. No Worker upload occurred because the scoped-credential preflight failed.
Next Rust hardening slice
Rust rate-limit audit plan (2026-09-05), continuing the explicit pattern-matching/formal-methods and shared-service requests.
Reuse zed-api-server.rs PR #53; do not create a duplicate issue. Its DEN-4253 reference is unrelated OTLP sidecar work in another project and will be removed, not amended there. This work belongs to DEN-3970 in github.com/zed-pkg, with DEN-99 as the formal-methods inventory reference.
- Merge current origin/main into the existing PR branch without rebasing or discarding either history. Preserve the current server healthcheck, ORM connection APIs, flags boundary, retry behavior, and shared middleware; translate only the intended rate-limit startup changes.
- Audit the real pinned ores-rl-lib-core transition API. Use exhaustive state/decision handling, exact rate parsing, conservative clock/error behavior, and a bounded bucket lifecycle that never restores spent capacity early.
- Reproduce the slow-refill eviction counterexample and add implementation-level bounded trace/model checks, concurrency and HTTP regressions, with explicit verification limits and an fmctl entry where supported.
- Generate and verify the committed dependency lock, test/format/lint the exact head, and publish evidence to this issue and GitHub. Do not merge a red dependency graph.
Known infrastructure boundary: ores-rl-lib-core is PRIVATE while this consumer is PUBLIC. Existing PR CI fails to authenticate fetching the pinned revision, and this repository exposes no Actions secrets. No private source will be vendored into the public repo and no credentials/visibility changes are authorized by this plan. Exhaust safe build/source alternatives; if CI still needs approved cross-repository read access, retain the PR as draft and record the exact blocker.
The embedding audit is tracked separately in DEN-1165: current legacy /v1 code still pads to 2050 dimensions while canonical ORM uses native JSON vectors. A coordinated model-registry/schema/query migration is still required; rate-limit work does not satisfy that acceptance criterion.
2026-09-05 Rust formal-methods delivery: zed-api-server.rs PR #53 now points at exact head fafe700290e6ccc00f64cca81a4583f34548ccf2. It preserves main's healthcheck/ORM/retry behavior, adds exhaustive fail-closed CoreDecision handling, exact integer refill parsing, monotonic watermark, safe full-bucket-only eviction, and a 100,000-identity memory ceiling. Local evidence: 183 workspace tests, 15 limiter tests, fmt, Clippy -D warnings, fmctl check/simulation with all four witnesses, and TLC exhaustive adapter model (1,270 reachable states, no invariant violation). The generated Cargo.lock pins the exact private ores-rate-limit core revision and the temporary lock workflow was removed. Hosted merge remains blocked only by the existing public-consumer/private-dependency Actions read boundary; no credentials, visibility changes, or private-source vendoring were used.
Hosted exact-head status for the Rust hardening slice: formal workflow 33987349416 passed (new limiter manifest, four witnesses, exhaustive finite graph); validate and agents policy passed. Test, Clippy, image, and both package roundtrip jobs fail before compilation because the public consumer cannot authenticate to private ores-rate-limit/ores-rl-lib-core. PR #53 stays draft until an approved cross-org Actions read path exists.
DEN-390 rate-limit dependency-chain update (2026-09-11): the public API currently has a canonical
.ores-rl.toml, but execution is still a separate process-local token bucket (src/ratelimit.rs+ZED_RATE_LIMIT_BURST/ZED_RATE_LIMIT_PER_SECOND). The authored policy is strict Redis token-bucket, so this is a real authority/runtime divergence. I opened zed-api-server.rs#74 for the consumer migration and ores-rate-limit/ores-rl-lib-core#23 for the upstream blocker: canonical distributed execution currently supports fixed-window Redis only, so substituting it now would silently change semantics. I also checked the current roots of zed-admin-api-server.rs, zed-web-server.rs, zed-admin-web-server.rs, and zed-mcp-server.rs; none currently has a root.ores-rl.toml. Treat this as two work classes under the existing shared-service outcome: (1) reconcile the public API's declared-vs-executed policy after #23 is exact-head green/consumable; (2) define and test explicit canonical rate-limit contracts for admin/web/MCP surfaces according to their trust boundary instead of cloning the public API policy mechanically. Preserve separate admin/non-admin policy and data-plane boundaries.
2026-09-05 platform goal and verification ledger
Expand this ongoing zed-pkg audit to deliver the full product platform requested in the active task. The August lifecycle slice remains completed; it is only one part of this goal.
Required outcomes:
Initial evidence: GitHub currently contains every requested repository role. Four missing local clones have now been acquired (admin web, admin API, public core, lambdas). Repository existence does not establish implementation: admin servers and public core are scaffolds; standalone ORM migration is partial; several transports/shared-service improvements remain in open PRs.
Execution order: inspect and reconcile existing PR intent; build complete onboarding/account flows and customer/admin UI; finish the shared ORM and interface dependency boundary; integrate and certify shared transports/services/chat and discovery; update release-set/deployment pins; verify the complete capability matrix. Keep this issue In Progress until all requirements have independent evidence.
Canonical tracking: https://linear.app/denman/issue/DEN-3970