diff --git a/multiplayer-next.md b/multiplayer-next.md
index df514f7e..6b6358c8 100644
--- a/multiplayer-next.md
+++ b/multiplayer-next.md
@@ -80,6 +80,27 @@ up a row, verify its claim against the code before planning against it** —
 and correct the row if it is stale, since an unverified row is a rumour, not
 a backlog item.
 
+Every corrected claim is backed by an executable test rather than by having
+located an implementation, because locating one proves it exists, not that it
+works:
+
+| Claim | Proof |
+|---|---|
+| 8.6 allocated `ServerConfig` fields | `test_server_config.gd::test_allocated_mode_is_opt_in_and_requires_compatibility_manifest` |
+| 8.6 signed-authorisation admission | `test_match_net.gd` join-authorisation cases, incl. the key-rotation set |
+| 8.6 endpoint wiring | `test_assignment_state.gd` — endpoint preserved, unsafe endpoint rejected |
+| 8.8 cross-replica revocation | `TestPostgreSQLSessionRevocationIsImmediateOnAnotherReplica` |
+| 8.19 lineup reached through formation | `TestPrepareProposalBuildsCasualLineupBeforeCreatingProposal` |
+| 8.19 all four penalty kinds durable | existing integration tests, plus `TestPostgreSQLInitialConnectNoShowWritesADurablePenalty` |
+| 8.30 signed roster metadata | `TestRealAllocatorWorkerPublishesSignedAssignmentRoster` |
+| 8.42 season countdown | `test_control_plane_client.gd` — `"Season ends in 2d"` and the clamped case |
+| 8.16/8.43 matcher deployed | `test_kubernetes_policies.py::test_every_required_workload_role_is_deployed` |
+
+Two claims had no proof and needed one written: `INITIAL_CONNECT_NO_SHOW`
+penalties and cross-replica revocation. Both new tests were mutation-checked —
+disabling the behaviour makes them fail — so they assert something real. 8.13
+and 8.52 are cross-references and assert nothing.
+
 ### Blocking sign-off — the work exists, the verification does not
 
 | # | What | Why it is not done | Detail |
diff --git a/server/store/postgres_integration_test.go b/server/store/postgres_integration_test.go
index 6985e6fa..f45dc4f2 100644
--- a/server/store/postgres_integration_test.go
+++ b/server/store/postgres_integration_test.go
@@ -2433,3 +2433,132 @@ func TestPostgreSQLInvalidTierPolicyIsRejectedRatherThanIgnored(t *testing.T) {
 		})
 	}
 }
+
+// Proof for the audit's claim that all four penalty kinds are durably
+// written. MATCH_ABANDONED, PROPOSAL_DECLINED and PROPOSAL_TIMEOUT already
+// had integration coverage; INITIAL_CONNECT_NO_SHOW did not, so that part of
+// the claim rested on reading the code rather than on evidence.
+func TestPostgreSQLInitialConnectNoShowWritesADurablePenalty(t *testing.T) {
+	db := openIntegrationPostgres(t)
+	applyIntegrationMigrations(t, db)
+
+	ctx := context.Background()
+	now := time.Now().UTC().Truncate(time.Microsecond)
+	for i := 0; i < 2; i++ {
+		playerID := fmt.Sprintf("noshow-player-%d", i)
+		if _, err := db.ExecContext(ctx, `INSERT INTO identities (player_id, steam_id) VALUES ($1, $2)`, playerID, "steam-"+playerID); err != nil {
+			t.Fatal(err)
+		}
+		if _, err := db.ExecContext(ctx, `INSERT INTO queue_tickets (ticket_id, player_id, playlist, state, client_build, protocol_version, enqueued_at, expires_at) VALUES ($1, $2, 'casual', 'ASSIGNMENT_READY', 'integration-build', 1, $3, $4)`,
+			fmt.Sprintf("noshow-ticket-%d", i), playerID, now, now.Add(time.Hour)); err != nil {
+			t.Fatal(err)
+		}
+	}
+	if _, err := db.ExecContext(ctx, `INSERT INTO game_servers (server_id, region, build, protocol_version, transport, state) VALUES ('noshow-server', 'EU', 'integration-build', 1, 'enet', 'ALLOCATED')`); err != nil {
+		t.Fatal(err)
+	}
+	if _, err := db.ExecContext(ctx, `INSERT INTO matches (match_id, playlist, state, region, protocol_version) VALUES ('noshow-match', 'casual', 'ALLOCATING', 'EU', 1)`); err != nil {
+		t.Fatal(err)
+	}
+	if _, err := db.ExecContext(ctx, `INSERT INTO allocations (allocation_id, match_id, server_id, region, build, protocol_version, transport, request_digest, state, allocated_at) VALUES ('noshow-allocation', 'noshow-match', 'noshow-server', 'EU', 'integration-build', 1, 'enet', $1, 'ALLOCATED', $2)`, []byte("request"), now); err != nil {
+		t.Fatal(err)
+	}
+	if _, err := db.ExecContext(ctx, `UPDATE matches SET state = 'ASSIGNMENT_READY', server_id = 'noshow-server', allocation_id = 'noshow-allocation', allocation_claimed_at = $1, initial_connect_ready_at = $1 WHERE match_id = 'noshow-match'`, now); err != nil {
+		t.Fatal(err)
+	}
+	for i := 0; i < 2; i++ {
+		playerID := fmt.Sprintf("noshow-player-%d", i)
+		slot := i * 3
+		if _, err := db.ExecContext(ctx, `INSERT INTO match_participants (match_id, player_id, ticket_id, slot, team) VALUES ('noshow-match', $1, $2, $3, $4)`, playerID, fmt.Sprintf("noshow-ticket-%d", i), slot, i); err != nil {
+			t.Fatal(err)
+		}
+		if _, err := db.ExecContext(ctx, `INSERT INTO assignments (match_id, player_id, allocation_id, server_id, slot, region, client_build, protocol_version, transport, endpoint, join_authorisation, manifest_digest, expires_at) VALUES ('noshow-match', $1, 'noshow-allocation', 'noshow-server', $2, 'EU', 'integration-build', 1, 'enet', '127.0.0.1:7777', 'join-token', $3, $4)`,
+			playerID, slot, []byte("manifest"), now.Add(time.Hour)); err != nil {
+			t.Fatal(err)
+		}
+	}
+
+	// Only player 0 ever connects. Player 1 is the no-show.
+	binding := domain.WorkloadBinding{AllocationID: "noshow-allocation", MatchID: "noshow-match", ServerID: "noshow-server"}
+	if _, err := ClaimPlayerConnection(ctx, db, binding, "noshow-player-0", 0, "noshow-receipt-key-00000", now); err != nil {
+		t.Fatalf("connecting player receipt: %v", err)
+	}
+
+	// Casual deliberately waits past InitialConnectWindow to CasualBotStartAfter
+	// before deciding, giving a slow-loading player longer than the ranked
+	// deadline. Reconciling at the earlier window only yields WAIT.
+	afterWindow := now.Add(domain.CasualBotStartAfter + time.Second)
+	if _, err := ReconcileInitialConnect(ctx, db, afterWindow, 10); err != nil {
+		t.Fatalf("reconcile: %v", err)
+	}
+
+	var endsAt time.Time
+	err := db.QueryRowContext(ctx, `SELECT ends_at FROM penalties WHERE player_id = 'noshow-player-1' AND kind = 'INITIAL_CONNECT_NO_SHOW'`).Scan(&endsAt)
+	if err != nil {
+		t.Fatalf("no INITIAL_CONNECT_NO_SHOW penalty was written for the absent player: %v", err)
+	}
+	if !endsAt.After(afterWindow.Add(-time.Second)) {
+		t.Fatalf("penalty ends_at %s is not in the future relative to %s", endsAt, afterWindow)
+	}
+
+	// The player who did connect must not be penalised for someone else's
+	// absence.
+	var innocent int
+	if err := db.QueryRowContext(ctx, `SELECT count(*) FROM penalties WHERE player_id = 'noshow-player-0'`).Scan(&innocent); err != nil {
+		t.Fatal(err)
+	}
+	if innocent != 0 {
+		t.Fatalf("the connecting player received %d penalties", innocent)
+	}
+}
+
+// Proof for the audit's claim that distributed revocation needs no
+// cross-replica protocol. The claim rests on sessions being durable and
+// re-read on every authenticated request, so a revocation on one replica is
+// effective on another with no coordination, invalidation broadcast or TTL to
+// wait out. That is a behavioural property, not something reading the code
+// establishes -- an in-memory cache in front of the session read would break
+// it silently while leaving every call site looking correct.
+func TestPostgreSQLSessionRevocationIsImmediateOnAnotherReplica(t *testing.T) {
+	db := openIntegrationPostgres(t)
+	applyIntegrationMigrations(t, db)
+
+	ctx := context.Background()
+	now := time.Now().UTC().Truncate(time.Microsecond)
+	if _, err := db.ExecContext(ctx, `INSERT INTO identities (player_id, steam_id) VALUES ('revoke-player', 'revoke-steam')`); err != nil {
+		t.Fatal(err)
+	}
+	// Independently constructed stores stand in for two control-plane
+	// replicas; they share only the database.
+	issuing := PostgresSessions{DB: db}
+	other := PostgresSessions{DB: db}
+
+	session, token, err := issuing.Issue(ctx, "revoke-player", time.Hour, now)
+	if err != nil {
+		t.Fatalf("issue: %v", err)
+	}
+	if _, err := other.Authenticate(ctx, session.SessionID, token, now); err != nil {
+		t.Fatalf("the other replica could not authenticate a valid session: %v", err)
+	}
+
+	// Revoke on one replica...
+	if err := issuing.Revoke(ctx, session.SessionID, now); err != nil {
+		t.Fatalf("revoke: %v", err)
+	}
+	// ...and the very next request on the other must fail, with no delay and
+	// nothing propagated between them.
+	if _, err := other.Authenticate(ctx, session.SessionID, token, now); err == nil {
+		t.Fatal("a revoked session still authenticated on another replica")
+	}
+
+	// An unrelated session belonging to the same player is unaffected, so
+	// revocation is session-scoped rather than identity-scoped. (Identity-wide
+	// revocation is the ban path, covered separately.)
+	survivor, survivorToken, err := issuing.Issue(ctx, "revoke-player", time.Hour, now)
+	if err != nil {
+		t.Fatalf("issue second session: %v", err)
+	}
+	if _, err := other.Authenticate(ctx, survivor.SessionID, survivorToken, now); err != nil {
+		t.Fatalf("revoking one session invalidated another: %v", err)
+	}
+}