fix(DEN-3970): formally verify edge WebSocket handshakes

[ORESoftware]

Outcome

Harden the shared app/user/web Cloudflare origin boundary and add a repository-owned fmctl manifest, finite model, actual-handler trace adapter, and real workerd/TCP WebSocket regressions.

Audited fixes

• Rebuild the upstream Upgrade/Connection handshake after removing hop-by-hop headers; preserve origin identity and subprotocol inputs.
• Reject malformed/non-GET upgrades before origin I/O.
• Keep origin 401/403 and redirects authoritative; never follow a redirect with credentials.
• Catch transport failures and disarm setup timeouts when the handshake settles.
• Return the original 101 response only when the WebSocket request has a real runtime socket.
• Separate checked finite decisions from effects, with exhaustive request-mode checking.

The added regressions failed before the production patch for stripped headers, escaping transport errors, and a leaked post-handshake timer.

Verification

• 57 Node unit groups, including all 276 finite actual-handler cases.
• Strict TypeScript decision checking.
• Three real workerd/TCP/WebSocket suites for the actual app, user, and web modules: text/binary frames, subprotocol, clean closure, post-deadline survival, origin denials, redirect, disconnect, and stalled setup.
• Rust fmctl: validate, check, simulation with seven witnesses, exhaustive TLC (276 initial scenarios / 736 distinct reachable states / depth 3), 16 generated production-handler replays.
• Both negative controls passed: a real TLC invariant counterexample and a real production/model mismatch.
• Locked npm audit: zero reported vulnerabilities.
• All workflow actionlint checks and git diff --check passed.
• Wrangler 4.127.1 dry-run bundling passed for all three route Workers; no upload.
• Locally checked with freshly fetched ORESoftware/formal-methods.rs at 734a1c3; CI also checks the immutable public runner export used by the Zed web/API formal gates.

Scope and production hold

This finite handshake model does not prove authentication, cryptography, distributed reconnect/backpressure, or live deployment. Shared Auth and the origin retain authentication authority. The existing exact-path maintenance policy, snapshot/If-Match/KV lease, route scoping, and deployment canaries are preserved.

Production promotion is not complete: the repository deployment secret is missing, local Cloudflare OAuth lacks required lease/route scopes, and the dd-codex AWS session is expired. No credential, DNS, or cluster mutation was performed. The upstream Quint/Apalache protobuf warning remains separately tracked in DEN-565 and is not suppressed.

Related: DEN-3970; zed-pkg/.github#61. Keep the umbrella issue open after this bounded slice.

[linear-code]

DEN-3970