transport: fix zero-state reconnect duplicate delivery; add P formal verification

[cbrewster]

Why: a client that sent messages but never received an ack is indistinguishable
from a new session at handshake time, so reconnecting to a server that lost the
session (restart or grace expiry) replayed the send buffer and re-executed
handlers while the original calls hung forever.

What changed:

• Handshake requests now carry expectedSessionState.isReconnect (optional,
  wire-compatible; sessions track hadConnection across transitions), and the
  server rejects marked reconnects to unknown sessions with
  SESSION_STATE_MISMATCH, yielding the documented hard-reconnect semantics
  (UNEXPECTED_DISCONNECT, fresh session, no replay). Deterministic regression
  test in tests/zerostate.test.ts; PROTOCOL.md documents the field.
• Adds verification/ (P language, Nix-packaged toolchain): a model-checked
  transport/session model with fault injection (which found this bug and
  reproduces d7c0ec9 as a must-fail regression), an inductive UCLID5 proof of
  the seq/ack sliding window, and PObserve runtime conformance checking of the
  hegel property-suite traces against the model. npm run model:check /
  model:observe; not wired into CI.

Staging test: run two server instances behind a flaky link (or kill/restart one
mid-call with heartbeats disabled); a client with an in-flight rpc against the
restarted server must get UNEXPECTED_DISCONNECT and the handler must not run
twice for the same request. Locally: npx vitest run __tests__/zerostate.test.ts,
nix develop .#verification --command verification/p/check.sh && verification/p/observe.sh.

[cbrewster]

Pull Request Stack

• transport: fix zero-state reconnect duplicate delivery; add P formal verification #405 ←

---

Stack managed with jj-github

[lhchavez]

need to read it in depth, but it looks fantastic

[lhchavez]

@replit/zerg rewrite in Kotlin, make no mistakes