Summary

Fixes #38788 — Context compaction cross-contamination where cron session summaries leak into unrelated live conversations.

Root Cause

ContextCompressor.on_session_end() is inherited as a no-op from ContextEngine. When a cron or background session compresses and rotates, _previous_summary survives session end. The memory manager's on_session_switch path exposes it to the next live session, causing compaction summaries to leak across session boundaries.

The comment at run_agent.py:2773-2777 already acknowledges this class of bug ("engines that accumulate per-session state... leak that state"), but the fix only called on_session_end — it didn't make on_session_end actually clear the state.

Fix

Override on_session_end() in ContextCompressor to clear _previous_summary = None. This is a 3-line change.

Verification

Quint Formal Spec

• Bug model: specs/session_isolation.qnt — Quint finds the violation in 13ms (3 states)
• Fix model: specs/session_isolation_fixed.qnt — Quint passes 100K+ traces with zero violations

Unit Tests

• test_on_session_end_clears_previous_summary: summary is None after session end
• test_on_session_end_preserves_other_state: global state (token tracking, compression count) is preserved
• Full compressor test suite: 93 passed, 0 regressions

Spec Design (Socratic Flow)

The formal spec was developed through an interactive Socratic specification process:

1. Should Session A's summary be visible to Session B? → No (default isolation)
2. Should compaction summaries be treated like memory? → No (session-scoped)
3. Where should isolation live? → Correct by construction, not convention
4. Compromise for this codebase? → Per-agent instances already exist; fix the cleanup gap
5. Where to store summaries? → As messages with session_id (already done)
6. Design choice: clear state on session end (structural fix, not query filter)

See specs/session_isolation.qnt and specs/session_isolation_fixed.qnt for the formal models.