Version 10.5.0 changes no public API, no library behaviour and no Dafny contract. It records what happens when the header length contract itself is wrong, writes down the rules the verification work follows, and turns one of them into a check.

• A weakened contract still verifies. verification/contract-weakening.md weakens the two length bounds of HeaderValid, the RFC 6455 section 5.2 rule that a length uses the fewest bytes. With either bound weakened the verifier still reports 41 verified, 0 errors, because the decoder calls the contract and changes with it. The generated-code check fails, but only because the C# was not regenerated. After regenerating, the tests built from the RFC catch both: two tests fail on one row each, on all six targets, and nothing else fails. The header mutant written for the weakened bound survives. No open gap was found for these two bounds. The weakened contract is not in the shipped code or the mutation catalog; the patches, commands and outputs are in docs/evidence/contract-weakening/.
• Rules for verification work. verification/README.md states three rules: when a requirement is in question, the RFC wins; expected bytes never come from production code; a new test is seen to fail on the old code, and that run is recorded, before its fix is trusted. AGENTS.md points to them and to the boundary register.
• RFC citations are checked. ./scripts/pdd.sh validate fails when a declaration in the Dafny sources has neither an RFC 6455 section nor a stated "Library policy:" in the comment directly above it, or a requirement's origin has neither. A declaration form the check does not read fails too, so none is skipped. Its first run found two masking lemmas without a citation; they now cite section 5.3. The comments are not embedded in the generated C#, so Masking.g.cs is unchanged. The rules are in tools/Pdd/README.md and the runs in docs/evidence/citation-check/.
• The README links to Proof vs. vibes, a video series that uses this library as its worked example, and docs/proof-vs-vibes/ guides viewers through what episode 1 shows. Every line reference in the guide names 8f8f207 (10.3.0), the version the episode shows, except the 2016 code at 3e60ed1.
• The exploration harness (verification/exploration/run.py) starts its net11.0 build and runs again, and the README's .NET badge and the mutation and Stryker guides name .NET 11. The 10.4 bump had missed them.

No new public API and no new production dependency. The library's C# and the generated code are the same as in 10.4.0. The 10.5 plan has the steps, decisions and lessons.

Version 10.4.0 adds .NET 11 and changes no public API or documented behaviour. It is the first release built with the .NET 11 SDK.

• New target: net11.0. The package now has six builds: .NET Standard 2.0 and 2.1, .NET 8, .NET 9, .NET 10 and .NET 11. .NET 8 and .NET 9 reached end of support on 2026-11-10; their builds stay, so nobody on them is moved to a different build in a release that promises no behaviour change.
• The .NET 11 build uses Runtime Async. On .NET 11 the runtime, not compiler-generated state machines, suspends and resumes the library's async methods. The net11.0 assembly has none of the 48 state machines left and is 102 KiB instead of 136 KiB. In an end-to-end loopback benchmark every measured path allocates 216 to 351 bytes less per operation, and none is measurably slower. Live stack traces and debugger call stacks show fewer frames; exception stack traces are unchanged. The other five builds are compiled as before. The report is verification/runtime-async.md.
• The library is compiled with C# 15 (LangVersion 15) but does not yet use C# 15 syntax. A union for the internal handshake result is written and tested, but Stryker.NET, which runs the mutation checks for every release, cannot compile C# 15 yet. It waits for a Stryker release that can. The 10.4 plan has the details.
• Microsoft.Bcl.AsyncInterfaces stays on 10.0.x: version 11.0.0 warns that it does not support .NET 8 or .NET 9, and the interface package would pass that warning to every .NET 8 and 9 build that uses it.
• Tests, tooling, CI and the dev container use the .NET 11 SDK. All six library builds are tested on a .NET 11 host, and the controlled ordering experiments and Stryker run against the net11.0 build.

No new public API and no new production dependency. The Dafny proofs, their scope and the generated code are unchanged. The evidence and its limits are in the 10.4 plan.

Version 10.3.0 adds no feature and changes no public behaviour. It ties the header length rule to RFC 6455, makes the header tests fail when the check they name is removed, and records two experiments about the boundary between the C# client and the verified protocol core. One is adopted and one is not.

• Every contract-bearing method and lemma in the Dafny core now names the RFC 6455 section it implements, or says that it is library policy. The comments are not embedded in the generated C#, so Masking.g.cs is unchanged.
• The rule that a frame length must use the fewest bytes (RFC 6455 section 5.2) is a traced requirement (HEADER-001, with HEADER-002 for refusing a frame from its header before any payload is read) with two Dafny mutants. The test for it used to pass on a parser that accepted non-minimal lengths, because the frames carried no payload and the old parser threw at end of stream. Tests now send the payload a header announces, so an accepting parser fails on its own. The header length note has the replay.
• Test parity for the header rules: a row for every reserved value (RSV2, RSV3, opcodes 4 to 7 and 11 to 15), a frame of exactly the configured limit is read and one byte more is refused from its header, and a truncated header ends in the end-of-stream error at every prefix. The validation note lists every claim, its test, its failing-first run and what stays unbacked.
• A test for a rejected handshake awaits the connect call and checks that no sender is installed. It replaces a kill that depended on a race: the Stryker mutant that removes throw handshakeException; was only caught when a test happened to run first.
• Adopted: named types at the verified core boundary. The receive, transmit and close states and the close event are small internal structs that cannot hold a value outside the range the generated core requires, so an out-of-range code cannot be passed from C#. The measured per-frame paths allocate the same number of bytes and show no measurable change in time. The report is verification/core-boundary-types.md.
• Not adopted: the reconnect lifecycle decision as a pure function. It was built, measured and reverted. It mirrored the six lock sites one to one and removed nothing from the expensive part of the tests, so the production change is not in this release. The report and its evidence stay: verification/reconnect-decision.md.
• The Pdd tooling reads Dafny declarations more carefully (attributes, bodiless functions, set displays in contracts), and its fixtures name a declaration and an offset instead of an absolute line, so a comment in Protocol.dfy no longer breaks eleven tests.

All five library targets remain supported. These changes add no public API and no new production dependency. The only production C# changes are the internal boundary types above and one internal constant for the end-of-stream message. The Dafny proofs retain their scope: the new mutants show that the contract catches a decoder that accepts one refused header, not that the whole decoder is covered. See the verification guide and the 10.3 session plan for the evidence and its limits.

Version 10.2.0 strengthens cancellation, teardown and sequential reconnect behavior, and expands the evidence for the C# boundaries around the verified protocol core.

• Transport abort wakes queued writers so they can settle instead of remaining blocked behind a disposed gate. Controlled tests cover cancellation before admission, queued writes and in-flight ownership.
• Sequential reconnect cleanup respects connection ownership. Late cleanup from an old connection cannot clear the current sender, and disposal prevents new connection admission.
• Tests cover payload buffer lifetime and once-only return, parser retention and metadata, scratch-buffer ownership, Close ordering, observer terminal signals and periodic Ping cleanup.
• Verification receipts bind tests, proof checks and mutation results to their source and runtime. Missing, stale, interrupted or timed-out evidence fails acceptance; bounded process cleanup retains diagnostic output.

All five library targets remain supported. These changes add no public API or new production dependency. The Dafny proofs retain their existing scope; asynchronous ownership and lifecycle behavior are tested C# boundaries, not proofs of arbitrary schedules or network progress. See the Phase 3 validation record for repeatability, costs and remaining platform qualification limits.

Version 10.1.0 extends the Dafny core with receive admission that includes fragmentation state, outgoing message transitions, closing transitions, exact segment concatenation, and a length-header round-trip theorem.

• List sends hold the data-message gate until their final fragment; Ping/Pong can still interleave. All list items are validated before the first write. Cancellation after a partial list prevents further data sends; an uncertain partial wire write prevents all further frames.
• Orphan continuations, conflicting data frames and aggregate-size violations fail from the header, before payload allocation or reading.
• Manual sends reject invalid message sequences. Callers still own the sequencing of manually supplied continuations and must not mutate byte arrays during a send.
• Asynchronous disposal waits for the peer's Close response, with a five-second response timeout after the bounded Close send. Synchronous disposal remains bounded, best-effort teardown.

The proofs cover synchronous decisions and byte operations under explicit preconditions. C# lock ownership, socket progress, cancellation and event delivery remain reviewed and tested boundaries. See the verification guide for the contracts and evidence.

Version 10.0.0 introduces proof driven development with Dafny for critical WebSocket protocol logic. The library runs C# generated from verified implementations of header parsing, fragmentation decisions, frame sizing, header encoding and masking, with explicit handshake and Close acceptance predicates.

What this means

The verified algorithms are checked against written contracts for every input allowed by those contracts, complementing the examples covered by tests. This gives stronger assurance about byte transformations, bounds and protocol state transitions. CI is configured to repeat verification and detect stale generated code when those implementations change.

Protocol improvements

• Reject malformed frames before payload allocation. Validate server masking, reserved bits/opcodes, canonical lengths, control-frame constraints and size limits.
• Handle fragmentation consistently. Reject orphan continuations and new data frames during unfinished messages; preserve state across Ping/Pong; correct reassembled metadata and validate complete text as strict UTF-8.
• Validate the handshake before reporting success. Check the accept value against the actual request key, Upgrade/Connection tokens and subprotocol selection. Reject unsupported extensions and overrides of protocol-owned request headers.
• Strengthen outgoing framing and Close validation. Check size arithmetic, set FIN correctly on explicit final continuations, reject invalid control frames and Close payloads, and reject invalid UTF-16 strings during encoding.

Compatibility and dependencies

All five target frameworks remain supported. Consumers do not need Dafny or Z3; the library adds a dependency on DafnyRuntime 4.11.0. Stricter validation may reject malformed traffic or custom handshake headers accepted by earlier versions.

The proofs cover the synchronous core, not the entire asynchronous client. Local validation passed 161 tests against each library target and achieved 79.9% line coverage. Active sender masking benchmarks measured zero allocations and improved throughput; these are local kernel measurements, not network performance guarantees.

Read what we proved, what improved and where the proof stops for the guarantees, limitations, upgrade implications and validation results.

WebsocketClientLite 9.2.0 – Highlights

Dependencies

• System.Reactive 7.0.0 (previously 6.1.0). Projects that reference this
  package move to Rx 7.
• HttpMachine.PCL 6.2.0.
• Microsoft.Bcl.AsyncInterfaces 10.0.14 (netstandard2.0).

No API changes.

WebsocketClientLite 9.1.0 – Highlights

New

• IAsyncDisposable on ClientWebSocketRx (and the legacy MessageWebsocketRx);
  IWebSocketClientRx now extends IAsyncDisposable. await using is the
  preferred lifecycle: DisposeAsync awaits the RFC 6455 close handshake of
  any still-active connection before releasing the socket. Dispose() remains
  the abrupt counterpart (bounded best-effort close, never hangs).

Bug fixes and internals

• Unified teardown: the close handshake runs exactly once on every end path
  (server close, read error, unsubscribe, Dispose, DisposeAsync) through one
  shared mechanism, and every path can await an in-flight close — close
  frame before socket teardown, no cross-mechanism races.
• Read-loop errors reliably reach the subscriber as OnError with the
  original exception; previously they could race teardown and be swallowed
  into a graceful completion.
• Removed the unsound public ObservableExtensions.FinallyAsync operator
  (never fired on unsubscribe; could replace the stream error).
• HttpMachine.PCL 6.0.1: span-based, allocation-free handshake parsing;
  case-insensitive header lookups; upstream HTTP conformance fixes.

Notes

• Publishing now uses NuGet Trusted Publishing (OIDC) instead of a
  long-lived API key.

WebsocketClientLite 9.0.2 – Highlights

• Fixes a race in the 9.0.1 close-on-unsubscribe behavior: disposing the
  subscription immediately after WebsocketConnected could skip the close
  handshake. The close hook is now registered before WebsocketConnected is
  emitted and runs on every teardown path. Use 9.0.2 instead of 9.0.1.

Includes all 9.0.1 changes:

Bug fixes

• Unsubscribing from the connection observable now sends the RFC 6455 close
  handshake (best-effort, exactly once) instead of just dropping the TCP
  connection.
• A failed handshake (e.g. HTTP 404) now fails fast with the server's status
  code instead of reporting an internal success state and waiting out the
  handshake timeout.
• Send failures now throw WebsocketClientLiteException at the await site, in
  addition to reporting SendError on the status channel.
• The final Disconnected status is delivered (Rx-grammar fix in the status
  callbacks).
• A Close frame received mid-fragmentation cleanly aborts the message and the
  read loop no longer runs into EOF after a close.
• Disposing the client while a connection is active no longer throws from
  teardown.
• NuGet packaging: the interface assembly is no longer bundled into
  lib/netstandard2.0/2.1 alongside the IWebsocketClientLite dependency.

New

• ClientWebSocketRx.NegotiatedSubprotocols exposes the subprotocol(s) the
  server accepted during the handshake.

Notes

• A user-supplied TcpClient can only serve the first connection; leave
  TcpClient unset when using reconnect patterns (Retry/Repeat). The console
  sample and README have been updated accordingly.

WebsocketClientLite 9.0.0 – Highlights

Bug fixes

• Subprotocols are now actually sent in the handshake (Sec-WebSocket-Protocol).
• Close status codes are sent big-endian per RFC 6455.
• ExcludeZeroApplicationDataInPong is now honored (Slack RTM).
• The CancellationToken passed to WebsocketConnectObservable is forwarded.
• Fragmented messages reassemble correctly on .NET 8/9/10 and .NET Standard 2.1.
• Writes to the connection are serialized, fixing mid-stream disconnects when
  client pings interleave with sends.

Security hardening

• Configurable MaxFrameSize (default 16 MiB) caps incoming frames and reassembled
  messages to guard against memory-exhaustion from a malicious server.
• Control frames are validated (<=125 bytes, not fragmented) per RFC 6455 §5.5.
• Handshake header/origin/subprotocol values containing CR/LF/NUL are rejected.
• CheckCertificateRevocation option (default true) enables TLS revocation checking.

Performance

• Receive path reads each payload once and unmasks in place (no MemoryStream,
  far fewer allocations); frames are read from a single subscription.
• Send path avoids per-frame mask-key and text-encoding allocations.

Breaking changes

• ClientWebSocketRx is now a class instead of a record, and its TcpClient
  property is nullable.
• CheckCertificateRevocation defaults to true; set it to false if your
  environment cannot reach OCSP/CRL endpoints.

Tooling

• Tests run against every target framework (netstandard2.0..net10) and a CI
  workflow builds, tests, and gates code coverage.