diff --git a/Beam/Broker/DocumentState.lean b/Beam/Broker/DocumentState.lean
index 4fbc5ba9..bdac6c26 100644
--- a/Beam/Broker/DocumentState.lean
+++ b/Beam/Broker/DocumentState.lean
@@ -63,6 +63,7 @@ inductive SyncFileAction where
 structure SyncFileDecision where
   action : SyncFileAction
   version : Nat
+  nextVersion : Nat
   docs : Docs
 
 structure VersionMarkResult where
@@ -103,7 +104,8 @@ private def docStateOfSnapshot (version : Nat) (snapshot : FileSnapshot) : DocSt
 
 /--
 Decide how a freshly read file snapshot should update the broker's LSP document
-mirror.
+mirror. `nextVersion` is the session-wide allocator, retained when documents close.
+Only opens and source changes consume a revision; unchanged and superseded reads preserve it.
 
 Request handlers reserve nonzero `readSeq` values before reading the filesystem.
 If an older read finishes after a newer read has already been applied, the older
@@ -114,13 +116,15 @@ newer LSP document versions.
 def syncFileDecision
     (docs : Docs)
     (uri : DocumentUri)
-    (snapshot : FileSnapshot) : SyncFileDecision :=
+    (snapshot : FileSnapshot)
+    (nextVersion : Nat) : SyncFileDecision :=
   match docs.get? uri with
   | none =>
-      let version := 1
+      let version := nextVersion
       {
         action := .open
         version
+        nextVersion := version + 1
         docs := docs.insert uri (docStateOfSnapshot version snapshot)
       }
   | some docState =>
@@ -128,12 +132,14 @@ def syncFileDecision
         {
           action := .unchanged
           version := docState.version
+          nextVersion
           docs
         }
       else if docState.textHash == snapshot.textHash then
         {
           action := .unchanged
           version := docState.version
+          nextVersion
           docs := docs.insert uri {
             docState with
             textTraceHash := snapshot.textTraceHash
@@ -143,10 +149,11 @@ def syncFileDecision
           }
         }
       else
-        let version := docState.version + 1
+        let version := nextVersion
         {
           action := .change
           version
+          nextVersion := version + 1
           docs := docs.insert uri {
             (docStateOfSnapshot version snapshot) with
             checkpointedVersion? := none
diff --git a/Beam/Broker/OpenDocs.lean b/Beam/Broker/OpenDocs.lean
index 1e84116d..88e2c32e 100644
--- a/Beam/Broker/OpenDocs.lean
+++ b/Beam/Broker/OpenDocs.lean
@@ -17,6 +17,7 @@ namespace OpenDocs
 
 structure SessionView where
   root : System.FilePath
+  sessionToken : String
   docs : DocumentState.Docs := {}
 
 inductive DiskStatus where
@@ -48,6 +49,7 @@ def docDiskStatus (path : System.FilePath) (docState : DocState) : IO DiskStatus
 
 def docJson
     (root : System.FilePath)
+    (sessionToken : String)
     (uri : DocumentUri)
     (docState : DocState) : IO Json := do
   let path? := System.Uri.fileUriToPath? uri
@@ -65,7 +67,7 @@ def docJson
   pure <| Json.mkObj <|
     [
       ("uri", toJson uri),
-      ("version", toJson docState.version),
+      ("snapshot", toJson ({ session := sessionToken, revision := docState.version } : SnapshotRef)),
       ("diskStatus", toJson status),
       ("checkpointed", toJson checkpointed)
     ] ++
@@ -84,7 +86,7 @@ def sessionJson (session? : Option SessionView) : IO Json := do
       ]
   | some session =>
       let files ← session.docs.toList.mapM fun (uri, docState) =>
-        docJson session.root uri docState
+        docJson session.root session.sessionToken uri docState
       pure <| Json.mkObj [
         ("active", toJson true),
         ("files", Json.arr files.toArray)
diff --git a/Beam/Broker/Pending.lean b/Beam/Broker/Pending.lean
index 4051a5b7..f3c8709d 100644
--- a/Beam/Broker/Pending.lean
+++ b/Beam/Broker/Pending.lean
@@ -206,39 +206,45 @@ private def observeSyncFileProgress
       progress?
 
 private def trackedPublishDiagnosticsParam?
-    (trackedUri? : Option DocumentUri)
+    (tracked? : Option (DocumentUri × Nat))
     (diagnosticParam : PublishDiagnosticsParams) : Option PublishDiagnosticsParams :=
-  match trackedUri? with
-  | some uri =>
+  match tracked? with
+  | some (uri, version) =>
       let diagnosticParam := normalizePublishDiagnostics diagnosticParam
-      if diagnosticParam.uri == uri then
+      if diagnosticParam.uri == uri &&
+          diagnosticParam.version?.all (· == Int.ofNat version) then
         some diagnosticParam
       else
         none
   | none =>
       none
 
-private def diagnosticStreamKey (diagnostic : Diagnostic) : String :=
-  (toJson diagnostic).compress
+private def diagnosticStreamKey
+    (snapshot? : Option SnapshotRef) (diagnostic : Diagnostic) : String :=
+  (toJson (snapshot?, diagnostic)).compress
 
 private def emitNewTrackedDiagnostics
     (root : System.FilePath)
+    (sessionToken : String)
     (seen : Std.TreeSet String compare)
     (diagnosticParam : PublishDiagnosticsParams)
     (diagnosticScope : DiagnosticScope)
     (emitDiagnostic? : Option (StreamDiagnostic → IO Unit) := none) :
     IO (Std.TreeSet String compare) := do
+  let snapshot? := diagnosticParam.version?.bind fun version =>
+    if version > 0 then some { session := sessionToken, revision := version.toNat }
+    else none
   let mut seen := seen
   let diagnostics := filterSyncDiagnostics diagnosticScope diagnosticParam.diagnostics
   for diagnostic in diagnostics do
-    let key := diagnosticStreamKey diagnostic
+    let key := diagnosticStreamKey snapshot? diagnostic
     if !seen.contains key then
       seen := seen.insert key
       match emitDiagnostic? with
       | some emitDiagnostic =>
           try
             emitDiagnostic <|
-              streamDiagnosticOfDiagnostic root diagnosticParam.uri diagnosticParam.version? diagnostic
+              streamDiagnosticOfDiagnostic root diagnosticParam.uri snapshot? diagnostic
           catch _ =>
             pure ()
       | none =>
@@ -264,9 +270,10 @@ def observeProgress
 
 def observePublishDiagnostics
     (root : System.FilePath)
+    (sessionToken : String)
     (pending : PendingRequest)
     (diagnosticParam : PublishDiagnosticsParams) : IO Unit := do
-  match trackedPublishDiagnosticsParam? (pending.tracked?.map Prod.fst) diagnosticParam with
+  match trackedPublishDiagnosticsParam? pending.tracked? diagnosticParam with
   | none =>
       pure ()
   | some diagnosticParam =>
@@ -274,20 +281,9 @@ def observePublishDiagnostics
       pending.diagnosticsRef.set diagnosticParam.diagnostics
       let seen ← pending.seenDiagnosticKeysRef.get
       let seen ←
-        emitNewTrackedDiagnostics root seen diagnosticParam pending.diagnosticScope pending.emitDiagnostic?
+        emitNewTrackedDiagnostics root sessionToken seen diagnosticParam pending.diagnosticScope pending.emitDiagnostic?
       pending.seenDiagnosticKeysRef.set seen
 
-def observeDiagnostics
-    [ToJson α]
-    (root : System.FilePath)
-    (pending : PendingRequest)
-    (param : α) : IO Unit := do
-  match fromJson? (toJson param) with
-  | .ok (diagnosticParam : PublishDiagnosticsParams) =>
-      observePublishDiagnostics root pending diagnosticParam
-  | .error _ =>
-      pure ()
-
 end PendingRequest
 
 namespace PendingRequestStore
diff --git a/Beam/Broker/Protocol.lean b/Beam/Broker/Protocol.lean
index 08eaccd7..af14385e 100644
--- a/Beam/Broker/Protocol.lean
+++ b/Beam/Broker/Protocol.lean
@@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import Lean
 import Beam.LSP.Todo
+import Beam.Snapshot
 import Beam.Workspace.Protocol
 
 open Lean
@@ -246,10 +247,10 @@ structure RequestBackend where
 structure RequestFile extends RequestBackend where
   path : String
 
-structure RequestVersionedFile extends RequestFile where
-  version : Nat
+structure RequestSnapshotFile extends RequestFile where
+  snapshot : SnapshotRef
 
-structure RequestPosition extends RequestVersionedFile where
+structure RequestPosition extends RequestSnapshotFile where
   line : Nat
   character : Nat
 
@@ -271,7 +272,7 @@ structure ReferencesRequest extends RequestPosition where
 structure WorkspaceSymbolsRequest extends RequestBackend where
   query : String
 
-structure CodeActionResolveRequest extends RequestVersionedFile where
+structure CodeActionResolveRequest extends RequestSnapshotFile where
   codeAction : Lsp.CodeAction
 
 structure SaveOleanRequest extends RequestFile where
@@ -324,7 +325,7 @@ inductive RequestPayload where
   | signatureHelp (request : RequestPosition)
   | definition (request : RequestPosition)
   | references (request : ReferencesRequest)
-  | documentSymbols (request : RequestVersionedFile)
+  | documentSymbols (request : RequestSnapshotFile)
   | workspaceSymbols (request : WorkspaceSymbolsRequest)
   | codeActionResolve (request : CodeActionResolveRequest)
   | saveOlean (request : SaveOleanRequest)
@@ -433,23 +434,23 @@ private def Op.requestFields (op : Op) : Array String :=
       #["path", "diagnosticScope", "diagnosticsInResult"]
   | .close => #["path", "diagnosticScope", "saveArtifacts"]
   | .runAt =>
-      #["path", "version", "line", "character", "text", "storeHandle"]
+      #["path", "snapshot", "line", "character", "text", "storeHandle"]
   | .hover | .signatureHelp | .definition =>
-      #["path", "version", "line", "character"]
+      #["path", "snapshot", "line", "character"]
   | .references =>
-      #["path", "version", "line", "character", "includeDeclaration"]
-  | .documentSymbols => #["path", "version"]
+      #["path", "snapshot", "line", "character", "includeDeclaration"]
+  | .documentSymbols => #["path", "snapshot"]
   | .workspaceSymbols => #["query"]
-  | .codeActionResolve => #["path", "version", "codeAction"]
+  | .codeActionResolve => #["path", "snapshot", "codeAction"]
   | .saveOlean => #["path", "diagnosticScope"]
   | .goals =>
       #[
-        "path", "version", "line", "character", "text", "mode", "compact",
+        "path", "snapshot", "line", "character", "text", "mode", "compact",
         "ppFormat"
       ]
   | .todo =>
       #[
-        "path", "version", "line", "character", "endLine", "endCharacter", "kinds",
+        "path", "snapshot", "line", "character", "endLine", "endCharacter", "kinds",
         "suggest"
       ]
   | .runWith =>
@@ -475,12 +476,12 @@ private def optionalJsonField [ToJson α] (name : String) : Option α → List (
 private def RequestFile.jsonFields (request : RequestFile) : List (String × Json) :=
   [("path", toJson request.path)]
 
-private def RequestVersionedFile.jsonFields
-    (request : RequestVersionedFile) : List (String × Json) :=
-  request.toRequestFile.jsonFields ++ [("version", toJson request.version)]
+private def RequestSnapshotFile.jsonFields
+    (request : RequestSnapshotFile) : List (String × Json) :=
+  request.toRequestFile.jsonFields ++ [("snapshot", toJson request.snapshot)]
 
 private def RequestPosition.jsonFields (request : RequestPosition) : List (String × Json) :=
-  request.toRequestVersionedFile.jsonFields ++ [
+  request.toRequestSnapshotFile.jsonFields ++ [
     ("line", toJson request.line),
     ("character", toJson request.character)
   ]
@@ -511,7 +512,7 @@ private def RequestPayload.jsonFields : RequestPayload → List (String × Json)
   | .workspaceSymbols request =>
       [("query", toJson request.query)]
   | .codeActionResolve request =>
-      request.toRequestVersionedFile.jsonFields ++ [("codeAction", toJson request.codeAction)]
+      request.toRequestSnapshotFile.jsonFields ++ [("codeAction", toJson request.codeAction)]
   | .saveOlean request =>
       request.toRequestFile.jsonFields ++
       optionalJsonField "diagnosticScope" request.diagnosticScope?
@@ -629,21 +630,21 @@ private def decodeRequestFile
     path := ← requiredField j "path"
   }
 
-private def decodeRequestVersionedFile
+private def decodeRequestSnapshotFile
     (j : Json)
-    (backend : Backend) : Except String RequestVersionedFile := do
+    (backend : Backend) : Except String RequestSnapshotFile := do
   let target ← decodeRequestFile j backend
   pure {
     toRequestFile := target
-    version := ← requiredField j "version"
+    snapshot := ← requiredField j "snapshot"
   }
 
 private def decodeRequestPosition
     (j : Json)
     (backend : Backend) : Except String RequestPosition := do
-  let target ← decodeRequestVersionedFile j backend
+  let target ← decodeRequestSnapshotFile j backend
   pure {
-    toRequestVersionedFile := target
+    toRequestSnapshotFile := target
     line := ← requiredField j "line"
     character := ← requiredField j "character"
   }
@@ -694,16 +695,16 @@ instance : FromJson Request where
             toRequestPosition := target
             includeDeclaration? := ← optionalField? (α := Bool) j "includeDeclaration"
           }
-      | .documentSymbols => .documentSymbols <$> decodeRequestVersionedFile j backend
+      | .documentSymbols => .documentSymbols <$> decodeRequestSnapshotFile j backend
       | .workspaceSymbols =>
           pure <| .workspaceSymbols {
             backend
             query := ← requiredField j "query"
           }
       | .codeActionResolve => do
-          let target ← decodeRequestVersionedFile j backend
+          let target ← decodeRequestSnapshotFile j backend
           pure <| .codeActionResolve {
-            toRequestVersionedFile := target
+            toRequestSnapshotFile := target
             codeAction := ← requiredField j "codeAction"
           }
       | .saveOlean => do
@@ -786,7 +787,7 @@ structure SyncFileProgress where
   rangeStartLine? : Option Nat := none
   /-- One-based upper line bound from Lean's processing ranges; not the source file line count. -/
   rangeEndLine? : Option Nat := none
-  deriving Inhabited, FromJson, ToJson, BEq, Repr
+  deriving FromJson, ToJson, BEq, Repr
 
 namespace SyncFileProgress
 
@@ -942,7 +943,7 @@ instance : FromJson SyncResultReadiness where
 structure StreamDiagnostic where
   path : String
   uri : String
-  version? : Option Int := none
+  snapshot? : Option SnapshotRef := none
   severity? : Option Lsp.DiagnosticSeverity := none
   range : Lsp.Range
   message : String
@@ -954,12 +955,12 @@ instance : FromJson StreamDiagnostic where
   fromJson? json := do
     requireOnlyJsonFields "stream diagnostic"
       #[
-        "path", "uri", "version", "severity", "range", "message", "saveBlocking",
+        "path", "uri", "snapshot", "severity", "range", "message", "saveBlocking",
         "completionBlocking"
       ] json
     let path ← json.getObjValAs? String "path"
     let uri ← json.getObjValAs? String "uri"
-    let version? ← optionalField? (α := Int) json "version"
+    let snapshot? ← optionalField? (α := SnapshotRef) json "snapshot"
     let severity? ← optionalField? (α := Lsp.DiagnosticSeverity) json "severity"
     let range ← json.getObjValAs? Lsp.Range "range"
     let message ← json.getObjValAs? String "message"
@@ -968,7 +969,7 @@ instance : FromJson StreamDiagnostic where
     pure {
       path
       uri
-      version?
+      snapshot?
       severity?
       range
       message
@@ -998,22 +999,21 @@ instance : FromJson SyncResultDiagnostics where
 
 structure SyncFileResult where
   path : String
-  version : Nat
+  snapshot : SnapshotRef
   diagnostics : SyncResultDiagnostics := {}
   readiness : SyncResultReadiness := {}
-  deriving Inhabited
 
 structure UpdateFileResult where
-  version : Nat
+  snapshot : SnapshotRef
   changed : Bool := false
-  deriving Inhabited, FromJson, ToJson, BEq, Repr
+  deriving FromJson, ToJson, BEq, Repr
 
 structure CancelResult where
   cancelled : Bool
   deriving FromJson, ToJson
 
 structure CodeActionResolveResult where
-  version : Nat
+  snapshot : SnapshotRef
   codeAction : Lsp.CodeAction
   deriving FromJson, ToJson
 
@@ -1022,21 +1022,21 @@ instance : ToJson SyncFileResult where
     Json.mkObj <|
       [
         ("path", toJson result.path),
-        ("version", toJson result.version),
+        ("snapshot", toJson result.snapshot),
         ("diagnostics", toJson result.diagnostics),
         ("readiness", toJson result.readiness)
       ]
 
 instance : FromJson SyncFileResult where
   fromJson? json := do
-    requireOnlyJsonFields "sync result" #["path", "version", "diagnostics", "readiness"] json
+    requireOnlyJsonFields "sync result" #["path", "snapshot", "diagnostics", "readiness"] json
     let path ← json.getObjValAs? String "path"
-    let version ← json.getObjValAs? Nat "version"
+    let snapshot ← json.getObjValAs? SnapshotRef "snapshot"
     let diagnostics ← json.getObjValAs? SyncResultDiagnostics "diagnostics"
     let readiness ← json.getObjValAs? SyncResultReadiness "readiness"
     pure {
       path
-      version
+      snapshot
       diagnostics
       readiness
     }
@@ -1054,13 +1054,12 @@ structure SaveOleanResult where
   ir? : Option String := none
   bc? : Option String := none
   sync : SyncFileResult
-  deriving Inhabited
 
 def SaveOleanResult.path (result : SaveOleanResult) : String :=
   result.sync.path
 
-def SaveOleanResult.version (result : SaveOleanResult) : Nat :=
-  result.sync.version
+def SaveOleanResult.snapshot (result : SaveOleanResult) : SnapshotRef :=
+  result.sync.snapshot
 
 instance : ToJson SaveOleanResult where
   toJson result :=
@@ -1068,7 +1067,7 @@ instance : ToJson SaveOleanResult where
       [
         ("path", toJson result.path),
         ("module", toJson result.module),
-        ("version", toJson result.version),
+        ("snapshot", toJson result.snapshot),
         ("sourceHash", toJson result.sourceHash),
         ("olean", toJson result.olean),
         ("ilean", toJson result.ilean),
@@ -1092,12 +1091,12 @@ instance : ToJson SaveOleanResult where
 instance : FromJson SaveOleanResult where
   fromJson? json := do
     requireOnlyJsonFields "save result" #[
-      "path", "module", "version", "sourceHash", "olean", "ilean", "c", "trace",
+      "path", "module", "snapshot", "sourceHash", "olean", "ilean", "c", "trace",
       "oleanServer", "oleanPrivate", "ir", "bc", "sync"
     ] json
     let path ← json.getObjValAs? String "path"
     let module ← json.getObjValAs? String "module"
-    let version ← json.getObjValAs? Nat "version"
+    let snapshot ← json.getObjValAs? SnapshotRef "snapshot"
     let sourceHash ← json.getObjValAs? String "sourceHash"
     let olean ← json.getObjValAs? String "olean"
     let ilean ← json.getObjValAs? String "ilean"
@@ -1110,8 +1109,8 @@ instance : FromJson SaveOleanResult where
     let sync ← json.getObjValAs? SyncFileResult "sync"
     unless path == sync.path do
       throw s!"save result path '{path}' does not match sync path '{sync.path}'"
-    unless version == sync.version do
-      throw s!"save result version {version} does not match sync version {sync.version}"
+    unless snapshot == sync.snapshot do
+      throw s!"save result snapshot {snapshot} does not match sync snapshot {sync.snapshot}"
     pure {
       module
       sourceHash
@@ -1129,7 +1128,6 @@ instance : FromJson SaveOleanResult where
 /-- Stable broker result for an artifact save followed by closing the mirrored document. -/
 structure CloseSaveResult where
   saved : SaveOleanResult
-  deriving Inhabited
 
 def CloseSaveResult.closed (_ : CloseSaveResult) : Bool :=
   true
diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean
index 356111d9..f0cafe24 100644
--- a/Beam/Broker/Server.lean
+++ b/Beam/Broker/Server.lean
@@ -65,11 +65,16 @@ structure Session where
   stdout : IO.FS.Stream
   stderrCapture : BackendStderrCapture
   pending : PendingRequestStore
+  /-- Allocate fresh Lean/Rocq revisions across all document lifetimes in this session. -/
+  nextDocumentVersion : Nat := 1
   nextId : Nat := 1
   nextEventSeq : Nat := 1
   moduleHistory : Std.TreeMap String ModuleHistory := {}
   docs : Std.TreeMap String DocState := {}
 
+private def Session.snapshotRef (session : Session) (version : Nat) : SnapshotRef :=
+  { session := session.sessionToken, revision := version }
+
 structure BackendState where
   nextEpoch : Nat := 1
   session? : Option Session := none
@@ -516,7 +521,7 @@ partial def sessionReaderLoop (session : Session) : IO Unit := do
             let pending ← PendingRequestStore.snapshot session.pending
             traceBroker s!"lsp publishDiagnostics pending={pending.size} params={(toJson param).compress}"
             for req in pending do
-              PendingRequest.observePublishDiagnostics session.root req diagnosticParam
+              PendingRequest.observePublishDiagnostics session.root session.sessionToken req diagnosticParam
         | .error _ =>
             pure ()
     | _ =>
@@ -844,7 +849,7 @@ private def withSessionForSnapshot
 private def syncFileSnapshotDetailed
     (session : Session)
     (snapshot : FileSyncSnapshot) : IO SyncedFileSnapshot := do
-  let decision := DocumentState.syncFileDecision session.docs snapshot.uri snapshot.file
+  let decision := DocumentState.syncFileDecision session.docs snapshot.uri snapshot.file session.nextDocumentVersion
   let session ←
     match decision.action with
     | .open =>
@@ -869,7 +874,7 @@ private def syncFileSnapshotDetailed
     | .unchanged =>
         pure session
   pure {
-    session := { session with docs := decision.docs }
+    session := { session with docs := decision.docs, nextDocumentVersion := decision.nextVersion }
     uri := snapshot.uri
     version := decision.version
     changed := decision.action != .unchanged
@@ -929,6 +934,7 @@ private def markDocSavedVersion (session : Session) (uri : DocumentUri) (version
   applyVersionMarkResult session result
 
 private def openDocsSessionView (session : Session) : OpenDocs.SessionView := {
+  sessionToken := session.sessionToken
   root := session.root
   docs := session.docs
 }
@@ -1554,7 +1560,12 @@ private def mergeFileProgressIfCurrent
     (uri : DocumentUri)
     (fileProgress? : Option SyncFileProgress) : IO Unit := do
   server.withState do
-    modifyCurrentSessionIfMatching session (fun current => recordFileProgress current uri fileProgress?)
+    modifyCurrentSessionIfMatching session fun current =>
+      match session.docs.get? uri, current.docs.get? uri with
+      | some captured, some now =>
+          if captured.version == now.version then recordFileProgress current uri fileProgress?
+          else current
+      | _, _ => current
 
 private def withCurrentMatchingSession
     (server : ServerRuntime)
@@ -1581,15 +1592,6 @@ private def withCurrentMatchingSession
           message := "broker backend session exited while request was in flight"
         }
 
-private def recordCompletedSync
-    (server : ServerRuntime)
-    (session : Session)
-    (uri : DocumentUri)
-    (version : Nat) : HandlerM Unit := do
-  withCurrentMatchingSession server session fun current => do
-    let current := markDocSyncedVersion current uri version
-    updateSession current
-
 private structure StartedSyncedRequest where
   session : Session
   uri : DocumentUri
@@ -1621,13 +1623,47 @@ private def documentVersionMismatchFailure
       (currentVersion? := some acceptedVersion)
       (uri? := some uri))
 
+private def snapshotMismatchFailure
+    (expected : SnapshotRef)
+    (current? : Option SnapshotRef)
+    (uri : DocumentUri) : ResponseFailure :=
+  responseFailureFor .contentModified
+    s!"source snapshot changed for {uri}; read the source and resolve the intended target again before retrying"
+    (some <| Json.mkObj <|
+      [("reason", toJson "snapshotMismatch"), ("expectedSnapshot", toJson expected),
+       ("uri", toJson uri)] ++
+      (current?.toList.map fun current => ("currentSnapshot", toJson current)))
+
+/-- Check document identity and apply a completion transition under the same state lock. -/
+private def withCurrentMatchingDocument
+    (server : ServerRuntime)
+    (session : Session)
+    (uri : DocumentUri)
+    (version : Nat)
+    (k : Session → M α) : HandlerM α := do
+  let result ← withCurrentMatchingSession server session fun current => do
+    let expected := session.snapshotRef version
+    let current? := (current.docs.get? uri).map fun doc => current.snapshotRef doc.version
+    if current? != some expected then
+      return .error <| snapshotMismatchFailure expected current? uri
+    return .ok (← k current)
+  requestArg result
+
+private def recordCompletedSync
+    (server : ServerRuntime)
+    (session : Session)
+    (uri : DocumentUri)
+    (version : Nat) : HandlerM Unit :=
+  withCurrentMatchingDocument server session uri version fun current =>
+    updateSession (markDocSyncedVersion current uri version)
+
 private def startSyncedDocumentRequest
     (session : Session)
     (snapshot : FileSyncSnapshot)
     (method : String)
     (mkParams : DocumentUri → DocState → Json)
     (trackedFor : DocumentUri → DocState → Option (DocumentUri × Nat))
-    (expectedVersion? : Option Nat := none)
+    (expectedSnapshot? : Option SnapshotRef := none)
     (clientRequestId? : Option String := none)
     (emitProgress? : Option (SyncFileProgress → IO Unit) := none)
     (diagnosticScope : DiagnosticScope := .errors)
@@ -1640,11 +1676,12 @@ private def startSyncedDocumentRequest
   let session ← syncFileSnapshot session snapshot
   let uri := snapshot.uri
   let docState ← requireDocState session uri
-  match expectedVersion? with
-  | some expectedVersion =>
-      if docState.version != expectedVersion then
+  match expectedSnapshot? with
+  | some expectedSnapshot =>
+      if session.snapshotRef docState.version != expectedSnapshot then
         updateSession session
-        return .error <| documentVersionMismatchFailure expectedVersion docState.version uri
+        return .error <| snapshotMismatchFailure expectedSnapshot
+          (some <| session.snapshotRef docState.version) uri
   | none =>
       pure ()
   let tracked := trackedFor uri docState
@@ -1675,7 +1712,7 @@ private def startSyncedWorkspaceRequest
     (method : String)
     (mkParams : DocumentUri → DocState → Json)
     (trackedFor : DocumentUri → DocState → Option (DocumentUri × Nat))
-    (expectedVersion? : Option Nat := none)
+    (expectedSnapshot? : Option SnapshotRef := none)
     (clientRequestId? : Option String := none)
     (emitProgress? : Option (SyncFileProgress → IO Unit) := none)
     (diagnosticScope : DiagnosticScope := .errors)
@@ -1683,7 +1720,7 @@ private def startSyncedWorkspaceRequest
     (cancelRef? : Option (IO.Ref Bool) := none) :
     M (Except ResponseFailure StartedSyncedRequest) :=
   withSessionForSnapshot workspaceId backend snapshot fun session =>
-    startSyncedDocumentRequest session snapshot method mkParams trackedFor expectedVersion?
+    startSyncedDocumentRequest session snapshot method mkParams trackedFor expectedSnapshot?
       clientRequestId? emitProgress? diagnosticScope emitDiagnostic? cancelRef?
 
 private def awaitSyncedDocumentRequest
@@ -1692,11 +1729,10 @@ private def awaitSyncedDocumentRequest
     (cancelRef? : Option (IO.Ref Bool) := none) : HandlerM PendingResult := do
   liftHandlerIO <| propagatePendingCancellation started.session cancelRef?
   let pending ← awaitPending started.pending
-  if started.tracked.isSome then
-    withFailureProgress pending.progress? <|
-      liftHandlerIO <| mergeFileProgressIfCurrent server started.session started.uri pending.progress?
   withFailureProgress pending.progress? <|
-    withCurrentMatchingSession server started.session fun _ => pure ()
+    withCurrentMatchingDocument server started.session started.uri started.version fun current => do
+      if started.tracked.isSome then
+        updateSession (recordFileProgress current started.uri pending.progress?)
   pure pending
 
 private def readRequestSyncSnapshot
@@ -1957,7 +1993,7 @@ private def saveOleanCore
       { hash := started.textTraceHash, mtime := started.textMTime }
       (some leanConfig.command) leanConfig.lakeHelper?
   let syncResult :=
-    mkSyncFileResult spec.relPath started.version currentDiagnostics saveReadiness
+    mkSyncFileResult spec.relPath (started.session.snapshotRef started.version) currentDiagnostics saveReadiness
   withFailureProgress barrierProgress? <|
     recordCompletedSync server started.session started.uri started.version
   if let some reason := spec.unsupportedSetupReason? then
@@ -2104,13 +2140,13 @@ private def handleSyncFileOp
       barrierOutcome.completionDiagnostics fileProgress?
   let replyDiagnostics? :=
     if request.diagnosticsInResult?.getD false then
-      some <| streamDiagnosticsForReply started.session.root started.uri started.version
+      some <| streamDiagnosticsForReply started.session.root started.uri (started.session.snapshotRef started.version)
         (request.diagnosticScope?.getD .errors) currentDiagnostics
     else
       none
   let resultPath := trackedPathLabel started.session.root started.uri
   let syncResult :=
-    mkSyncFileResult resultPath started.version currentDiagnostics saveReadiness replyDiagnostics?
+    mkSyncFileResult resultPath (started.session.snapshotRef started.version) currentDiagnostics saveReadiness replyDiagnostics?
   withFailureProgress fileProgress? <|
     recordCompletedSync server started.session started.uri started.version
   liftHandlerIO <| traceBroker
@@ -2158,7 +2194,7 @@ private def handleUpdateFileOp
       updateSession synced.session
       pure (.ok synced)
   pure <| Response.success (toJson ({
-    version := updated.version
+    snapshot := updated.session.snapshotRef updated.version
     changed := updated.changed
     : UpdateFileResult
   }))
@@ -2208,8 +2244,8 @@ private def handleRunAtOp
   let snapshot ← liftFailureIO <| readRequestSyncSnapshot server req path
   let started ← liftFailureIO <| server.withRequestBackendState req do
     startSyncedWorkspaceRequest req.workspaceId req.backend snapshot method
-      (fun uri _ => Json.mkObj <|
-        [ ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier }))
+      (fun uri docState => Json.mkObj <|
+        [ ("textDocument", toJson ({ uri := uri, version? := some docState.version : VersionedTextDocumentIdentifier }))
         , ("position", toJson ({ line := request.line, character := request.character : Lsp.Position }))
         , ("text", toJson request.text)
         ] ++
@@ -2217,7 +2253,7 @@ private def handleRunAtOp
         | some b => [("storeHandle", toJson b)]
         | none => [])
       trackedDocumentVersion
-      (expectedVersion? := some request.version)
+      (expectedSnapshot? := some request.snapshot)
       (clientRequestId? := req.clientRequestId?)
       (emitProgress? := emitProgress?)
       (emitDiagnostic? := runAtSetupProgressEmitter? emitDiagnostic?)
@@ -2231,10 +2267,11 @@ private def handleRunAtOp
 private def positionLspParams
     (request : RequestPosition)
     (uri : DocumentUri)
+    (docState : DocState)
     (extraFields : List (String × Json) := []) : Json :=
   Json.mkObj <|
     [
-      ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier })),
+      ("textDocument", toJson ({ uri := uri, version? := some docState.version : VersionedTextDocumentIdentifier })),
       ("position", toJson ({ line := request.line, character := request.character : Lsp.Position }))
     ] ++ extraFields
 
@@ -2252,9 +2289,9 @@ private def handlePositionLspOp
     readRequestSyncSnapshot server req (System.FilePath.mk request.path)
   let started ← liftFailureIO <| server.withRequestBackendState req do
     startSyncedWorkspaceRequest req.workspaceId req.backend snapshot method
-      (fun uri _ => positionLspParams request uri extraFields)
+      (fun uri docState => positionLspParams request uri docState extraFields)
       (trackedLeanDocumentVersion req.backend)
-      (expectedVersion? := some request.version)
+      (expectedSnapshot? := some request.snapshot)
       (clientRequestId? := req.clientRequestId?)
       (emitProgress? := emitProgress?)
       (cancelRef? := cancelRef?)
@@ -2311,7 +2348,7 @@ private def handleReferencesOp
 private def handleDocumentSymbolsOp
     (server : ServerRuntime)
     (req : BackendWorkspaceRequest)
-    (request : RequestVersionedFile)
+    (request : RequestSnapshotFile)
     (cancelRef? : Option (IO.Ref Bool) := none)
     (emitProgress? : Option (SyncFileProgress → IO Unit) := none) :
     HandlerM Response := do
@@ -2325,7 +2362,7 @@ private def handleDocumentSymbolsOp
         ("textDocument", toJson ({ uri := uri : TextDocumentIdentifier }))
       ])
       (trackedLeanDocumentVersion req.backend)
-      (expectedVersion? := some request.version)
+      (expectedSnapshot? := some request.snapshot)
       (clientRequestId? := req.clientRequestId?)
       (emitProgress? := emitProgress?)
       (cancelRef? := cancelRef?)
@@ -2385,14 +2422,14 @@ private def handleCodeActionResolveOp
     startSyncedWorkspaceRequest req.workspaceId req.backend snapshot method
       (fun _uri _docState => toJson request.codeAction)
       (trackedLeanDocumentVersion req.backend)
-      (expectedVersion? := some request.version)
+      (expectedSnapshot? := some request.snapshot)
       (clientRequestId? := req.clientRequestId?)
       (emitProgress? := emitProgress?)
       (cancelRef? := cancelRef?)
   let pending ← awaitSyncedDocumentRequest server started cancelRef?
   let resolved : CodeAction ← liftHandlerIO <| decodeResponseAs pending.result
   let payload : CodeActionResolveResult := {
-    version := started.version
+    snapshot := started.session.snapshotRef started.version
     codeAction := resolved
   }
   pure <| Response.withOptionalFileProgress (Response.success (toJson payload)) pending.progress?
@@ -2432,7 +2469,7 @@ private def handleGoalsOp
         match req.backend with
         | .lean =>
             Json.mkObj [
-              ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier })),
+              ("textDocument", toJson ({ uri := uri, version? := some docState.version : VersionedTextDocumentIdentifier })),
               ("position", toJson position)
             ]
         | .rocq =>
@@ -2449,7 +2486,7 @@ private def handleGoalsOp
               | none => []
             Json.mkObj fields)
       (trackedLeanDocumentVersion req.backend)
-      (expectedVersion? := some request.version)
+      (expectedSnapshot? := some request.snapshot)
       (clientRequestId? := req.clientRequestId?)
       (emitProgress? := emitProgress?)
       (cancelRef? := cancelRef?)
@@ -2473,8 +2510,8 @@ private def handleTodoOp
     readRequestSyncSnapshot server req (System.FilePath.mk request.path)
   let started ← liftFailureIO <| server.withRequestBackendState req do
     startSyncedWorkspaceRequest req.workspaceId req.backend snapshot method
-      (fun uri _docState => Json.mkObj <|
-        [ ("textDocument", toJson ({ uri := uri, version? := some request.version : VersionedTextDocumentIdentifier }))
+      (fun uri docState => Json.mkObj <|
+        [ ("textDocument", toJson ({ uri := uri, version? := some docState.version : VersionedTextDocumentIdentifier }))
         , ("range", toJson range)
         ] ++
         (match request.kinds? with
@@ -2484,7 +2521,7 @@ private def handleTodoOp
         | some suggest => [("suggest", toJson suggest)]
         | none => []))
       (trackedLeanDocumentVersion req.backend)
-      (expectedVersion? := some request.version)
+      (expectedSnapshot? := some request.snapshot)
       (clientRequestId? := req.clientRequestId?)
       (emitProgress? := emitProgress?)
       (cancelRef? := cancelRef?)
diff --git a/Beam/Broker/SyncResult.lean b/Beam/Broker/SyncResult.lean
index 4354b57a..eb809829 100644
--- a/Beam/Broker/SyncResult.lean
+++ b/Beam/Broker/SyncResult.lean
@@ -59,7 +59,7 @@ def syncResultReadiness
 
 def mkSyncFileResult
     (path : String)
-    (version : Nat)
+    (snapshot : SnapshotRef)
     (diagnostics : Array Diagnostic)
     (readiness : SyncSaveReadiness)
     (items? : Option (Array StreamDiagnostic) := none) : SyncFileResult :=
@@ -67,7 +67,7 @@ def mkSyncFileResult
   let readiness := normalizeSyncSaveReadiness diagnostics readiness
   {
     path
-    version
+    snapshot
     diagnostics := {
       counts := diagnosticCounts diagnostics
       items?
diff --git a/Beam/Broker/SyncSaveSupport.lean b/Beam/Broker/SyncSaveSupport.lean
index 8f6a27a8..dadbfaae 100644
--- a/Beam/Broker/SyncSaveSupport.lean
+++ b/Beam/Broker/SyncSaveSupport.lean
@@ -103,11 +103,11 @@ def diagnosticDisplayPath (root : System.FilePath) (uri : DocumentUri) : String
 def streamDiagnosticOfDiagnostic
     (root : System.FilePath)
     (uri : DocumentUri)
-    (version? : Option Int)
+    (snapshot? : Option SnapshotRef)
     (diagnostic : Diagnostic) : StreamDiagnostic := {
   path := diagnosticDisplayPath root uri
   uri
-  version?
+  snapshot?
   severity? := effectiveSyncDiagnosticSeverity diagnostic
   range := diagnostic.fullRange
   message := diagnostic.message
@@ -117,11 +117,11 @@ def streamDiagnosticOfDiagnostic
 def streamDiagnosticsForReply
     (root : System.FilePath)
     (uri : DocumentUri)
-    (version : Nat)
+    (snapshot : SnapshotRef)
     (diagnosticScope : DiagnosticScope)
     (diagnostics : Array Diagnostic) : Array StreamDiagnostic :=
   (filterSyncDiagnostics diagnosticScope diagnostics).map fun diagnostic =>
-    streamDiagnosticOfDiagnostic root uri (some (Int.ofNat version)) diagnostic
+    streamDiagnosticOfDiagnostic root uri (some snapshot) diagnostic
 
 def syncErrorCount (diagnostics : Array Diagnostic) : Nat :=
   diagnostics.foldl (init := 0) fun count diagnostic =>
diff --git a/Beam/Cli/Args.lean b/Beam/Cli/Args.lean
index 0023b9f8..71231914 100644
--- a/Beam/Cli/Args.lean
+++ b/Beam/Cli/Args.lean
@@ -6,6 +6,7 @@ Author: Emilio J. Gallego Arias
 
 import Lean
 import Beam.Broker.Protocol
+import Beam.Lean.Operation
 import Beam.Path
 import Beam.LSP.Todo
 
@@ -29,6 +30,17 @@ def parseNatArg (name value : String) : IO Nat := do
     | throw <| IO.userError s!"invalid {name} '{value}'"
   pure n
 
+def parseLeanDocumentArgs (path snapshotText : String) : IO Beam.Lean.DocumentInput := do
+  pure { path, snapshot := ← IO.ofExcept <| SnapshotRef.decode snapshotText }
+
+def parseLeanPositionArgs
+    (path snapshotText lineText characterText : String) : IO Beam.Lean.PositionInput := do
+  pure {
+    toDocumentInput := ← parseLeanDocumentArgs path snapshotText
+    line := ← parseNatArg "line" lineText
+    character := ← parseNatArg "character" characterText
+  }
+
 def joinTextArgs (args : List String) : Option String :=
   if args.isEmpty then none else some <| String.intercalate " " args
 
@@ -137,7 +149,7 @@ def parseLeanCloseSaveArgs (args : List String) : IO Beam.Broker.DiagnosticScope
   parseLeanDiagnosticScopeArgs "close-save" args
 
 def leanReferencesUsage : String :=
-  "usage: lean-beam [--root PATH] references <path> <version> <line> <character> [--include-declaration|--exclude-declaration]"
+  "usage: lean-beam [--root PATH] references <path> <snapshot> <line> <character> [--include-declaration|--exclude-declaration]"
 
 def parseLeanReferencesArgs (args : List String) : IO Bool := do
   match args with
@@ -147,7 +159,7 @@ def parseLeanReferencesArgs (args : List String) : IO Bool := do
   | _ => throw <| IO.userError leanReferencesUsage
 
 def leanGoalsUsage : String :=
-  "usage: lean-beam [--root PATH] goals before|after <path> <version> <line> <character>"
+  "usage: lean-beam [--root PATH] goals before|after <path> <snapshot> <line> <character>"
 
 def parseLeanGoalsModeArg (mode : String) : IO GoalMode := do
   match mode with
@@ -170,7 +182,7 @@ private def parseTodoSuggestArg (value : String) : IO Beam.LSP.Todo.TodoSuggestM
       throw <| IO.userError s!"invalid todo suggest mode '{value}' (expected one of: {allowed}): {err}"
 
 def leanTodoUsage : String :=
-  "usage: lean-beam [--root PATH] todo <path> <version> <startLine> <startCharacter> <endLine> <endCharacter> [--kind <kind> ...] [--suggest none|basic]"
+  "usage: lean-beam [--root PATH] todo <path> <snapshot> <startLine> <startCharacter> <endLine> <endCharacter> [--kind <kind> ...] [--suggest none|basic]"
 
 def parseLeanTodoArgs (args : List String) :
     IO (Option (Array Beam.LSP.Todo.TodoKind) × Option Beam.LSP.Todo.TodoSuggestMode) := do
diff --git a/Beam/Cli/Broker.lean b/Beam/Cli/Broker.lean
index ac0d7c3f..0fb19616 100644
--- a/Beam/Cli/Broker.lean
+++ b/Beam/Cli/Broker.lean
@@ -171,7 +171,7 @@ private def syncLikeCompleteMsg (completeLabel path : String) (resp : Response)
   match decodeSyncFileResult? resp with
   | some result =>
       let suffix := syncFileProgressSuffix (responseFileProgress? resp)
-      s!"beam: {completeLabel} complete for {path} (version {result.version}{suffix}{syncReadinessSuffix result})"
+      s!"beam: {completeLabel} complete for {path} (snapshot {result.snapshot}{suffix}{syncReadinessSuffix result})"
   | none =>
       s!"beam: {completeLabel} complete for {path}"
 
diff --git a/Beam/Cli/Commands.lean b/Beam/Cli/Commands.lean
index e6496d4a..a012a80d 100644
--- a/Beam/Cli/Commands.lean
+++ b/Beam/Cli/Commands.lean
@@ -74,35 +74,33 @@ private def mkSessionStatus
   detail?
 }
 
-private def updateVersionForRocqGoals
+private def updateSnapshotForRocqGoals
     (root : System.FilePath)
     (client : ProjectDaemonClient)
-    (path : String) : IO Nat := do
+    (path : String) : IO SnapshotRef := do
   let resp ← requestBroker root client {
     payload := .updateFile { backend := .rocq, path }
   }
   match decodeUpdateFileResult resp with
-  | .ok result => pure result.version
+  | .ok result => pure result.snapshot
   | .error (.broker failure) => throw <| IO.userError failure.error.message
   | .error (.invalidPayload detail) =>
       throw <| IO.userError <|
-        s!"update_file returned an invalid result while obtaining document version: {detail}"
+        s!"update_file returned an invalid result while obtaining document snapshot: {detail}"
 
 private def runLeanRunAt
     (opts : CliOptions)
-    (action path versionText lineText characterText : String)
+    (action path snapshotText lineText characterText : String)
     (textArgs : List String)
     (storeHandle : Bool := false) : IO Unit := do
-  let version ← parseNatArg "version" versionText
-  let line ← parseNatArg "line" lineText
-  let character ← parseNatArg "character" characterText
-  let parsedText ← parseTextArg s!"{action} <path> <version> <line> <character>" textArgs
+  let position ← parseLeanPositionArgs path snapshotText lineText characterText
+  let parsedText ← parseTextArg s!"{action} <path> <snapshot> <line> <character>" textArgs
   let root ← projectRoot opts .lean
   withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client => do
     let req ← withEnvClientRequestId <|
-      leanRunAtRequest path version line character parsedText.text (storeHandle := storeHandle)
+      leanRunAtRequest position parsedText.text (storeHandle := storeHandle)
     maybeEmitTextDebug req.clientRequestId? action parsedText.source parsedText.text
-    callBrokerWithProgress root client req (leanRunAtWaitSpec action path line character)
+    callBrokerWithProgress root client req (leanRunAtWaitSpec action path position.line position.character)
 
 private def runLeanRunWith
     (opts : CliOptions)
@@ -293,59 +291,51 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
       serveBackend home opts .lean
   | "serve" :: backend :: [] =>
       serveBackend home opts (← parseBackendName backend)
-  | "run-at" :: path :: version :: line :: character :: text =>
-      runLeanRunAt opts "run-at" path version line character text
-  | "run-at-handle" :: path :: version :: line :: character :: text =>
-      runLeanRunAt opts "run-at-handle" path version line character text
+  | "run-at" :: path :: snapshot :: line :: character :: text =>
+      runLeanRunAt opts "run-at" path snapshot line character text
+  | "run-at-handle" :: path :: snapshot :: line :: character :: text =>
+      runLeanRunAt opts "run-at-handle" path snapshot line character text
         (storeHandle := true)
-  | "hover" :: path :: versionText :: line :: character :: [] =>
+  | "hover" :: path :: snapshotText :: line :: character :: [] =>
       let root ← projectRoot opts .lean
-      let version ← parseNatArg "version" versionText
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
+      let position ← parseLeanPositionArgs path snapshotText line character
       let action := "hover"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanHoverRequest path version line character)
-          (leanHoverWaitSpec path line character action)
-  | "signature-help" :: path :: versionText :: line :: character :: [] =>
+          (leanHoverRequest position)
+          (leanHoverWaitSpec path position.line position.character action)
+  | "signature-help" :: path :: snapshotText :: line :: character :: [] =>
       let root ← projectRoot opts .lean
-      let version ← parseNatArg "version" versionText
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
+      let position ← parseLeanPositionArgs path snapshotText line character
       let action := "signature-help"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanSignatureHelpRequest path version line character)
-          (leanSignatureHelpWaitSpec path line character action)
-  | "definition" :: path :: versionText :: line :: character :: [] =>
+          (leanSignatureHelpRequest position)
+          (leanSignatureHelpWaitSpec path position.line position.character action)
+  | "definition" :: path :: snapshotText :: line :: character :: [] =>
       let root ← projectRoot opts .lean
-      let version ← parseNatArg "version" versionText
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
+      let position ← parseLeanPositionArgs path snapshotText line character
       let action := "definition"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanDefinitionRequest path version line character)
-          (leanDefinitionWaitSpec path line character action)
-  | "references" :: path :: versionText :: line :: character :: extra =>
+          (leanDefinitionRequest position)
+          (leanDefinitionWaitSpec path position.line position.character action)
+  | "references" :: path :: snapshotText :: line :: character :: extra =>
       let root ← projectRoot opts .lean
-      let version ← parseNatArg "version" versionText
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
+      let position ← parseLeanPositionArgs path snapshotText line character
       let includeDeclaration ← parseLeanReferencesArgs extra
       let action := "references"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanReferencesRequest path version line character includeDeclaration)
-          (leanReferencesWaitSpec path line character action)
-  | "document-symbols" :: path :: versionText :: [] =>
+          (leanReferencesRequest position includeDeclaration)
+          (leanReferencesWaitSpec path position.line position.character action)
+  | "document-symbols" :: path :: snapshotText :: [] =>
       let root ← projectRoot opts .lean
-      let version ← parseNatArg "version" versionText
+      let document ← parseLeanDocumentArgs path snapshotText
       let action := "document-symbols"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanDocumentSymbolsRequest path version)
+          (leanDocumentSymbolsRequest document)
           (leanDocumentSymbolsWaitSpec path action)
   | "workspace-symbols" :: queryParts =>
       let root ← projectRoot opts .lean
@@ -358,20 +348,18 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
         callBrokerWithProgress root client
           (leanWorkspaceSymbolsRequest query)
           (leanWorkspaceSymbolsWaitSpec query action)
-  | "goals" :: modeText :: path :: versionText :: line :: character :: [] =>
+  | "goals" :: modeText :: path :: snapshotText :: line :: character :: [] =>
       let root ← projectRoot opts .lean
       let mode ← parseLeanGoalsModeArg modeText
-      let version ← parseNatArg "version" versionText
-      let line ← parseNatArg "line" line
-      let character ← parseNatArg "character" character
+      let position ← parseLeanPositionArgs path snapshotText line character
       let action := "goals"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanGoalsRequest path version line character mode)
-          (leanGoalsWaitSpec path line character mode (some action))
-  | "todo" :: path :: versionText :: startLine :: startCharacter :: endLine :: endCharacter :: extra => do
+          (leanGoalsRequest position mode)
+          (leanGoalsWaitSpec path position.line position.character mode (some action))
+  | "todo" :: path :: snapshotText :: startLine :: startCharacter :: endLine :: endCharacter :: extra => do
       let root ← projectRoot opts .lean
-      let version ← parseNatArg "version" versionText
+      let snapshot ← IO.ofExcept <| SnapshotRef.decode snapshotText
       let startLine ← parseNatArg "startLine" startLine
       let startCharacter ← parseNatArg "startCharacter" startCharacter
       let endLine ← parseNatArg "endLine" endLine
@@ -380,7 +368,7 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
       let action := "todo"
       withProjectDaemon root .lean (explicitControlDir? := opts.explicitControlDir?) fun client =>
         callBrokerWithProgress root client
-          (leanTodoRequest path version startLine startCharacter endLine endCharacter kinds? suggest?)
+          (leanTodoRequest path snapshot startLine startCharacter endLine endCharacter kinds? suggest?)
           (leanTodoWaitSpec path startLine startCharacter endLine endCharacter action)
   | "run-with" :: path :: args =>
       runLeanRunWith opts "run-with" path args
@@ -432,12 +420,12 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
   | "rocq-goals-after" :: path :: line :: character :: text =>
       let root ← projectRoot opts .rocq
       withProjectDaemon root .rocq (explicitControlDir? := opts.explicitControlDir?) fun client => do
-        let version ← updateVersionForRocqGoals root client path
+        let snapshot ← updateSnapshotForRocqGoals root client path
         callBroker root client {
           payload := .goals {
             backend := .rocq
             path
-            version
+            snapshot
             line := ← parseNatArg "line" line
             character := ← parseNatArg "character" character
             mode? := some .after
@@ -449,12 +437,12 @@ def runCommand (home : System.FilePath) (opts : CliOptions) : IO Unit := do
   | "rocq-goals-prev" :: path :: line :: character :: text =>
       let root ← projectRoot opts .rocq
       withProjectDaemon root .rocq (explicitControlDir? := opts.explicitControlDir?) fun client => do
-        let version ← updateVersionForRocqGoals root client path
+        let snapshot ← updateSnapshotForRocqGoals root client path
         callBroker root client {
           payload := .goals {
             backend := .rocq
             path
-            version
+            snapshot
             line := ← parseNatArg "line" line
             character := ← parseNatArg "character" character
             mode? := some .before
diff --git a/Beam/Cli/LeanOperation.lean b/Beam/Cli/LeanOperation.lean
index fe072c3c..504f80dd 100644
--- a/Beam/Cli/LeanOperation.lean
+++ b/Beam/Cli/LeanOperation.lean
@@ -13,12 +13,10 @@ namespace Beam.Cli
 open Beam.Broker
 
 def leanRunAtRequest
-    (path : String)
-    (version : Nat)
-    (line character : Nat)
+    (position : Beam.Lean.PositionInput)
     (text : String)
     (storeHandle : Bool := false) : Request :=
-  ({ path, version, line, character, text } : Beam.Lean.RunAtInput).toBrokerRequest
+  ({ toPositionInput := position, text } : Beam.Lean.RunAtInput).toBrokerRequest
     (storeHandle := storeHandle)
 
 def leanRunWithRequest
@@ -32,62 +30,44 @@ def leanRunWithRequest
 def leanReleaseRequest (path : String) (handle : Handle) : Request :=
   ({ path, handle } : Beam.Lean.ReleaseInput).toBrokerRequest
 
-def leanHoverRequest
-    (path : String)
-    (version : Nat)
-    (line character : Nat) : Request :=
-  ({ path, version, line, character } : Beam.Lean.PositionInput).toHoverBrokerRequest
+def leanHoverRequest (position : Beam.Lean.PositionInput) : Request :=
+  position.toHoverBrokerRequest
 
-def leanSignatureHelpRequest
-    (path : String)
-    (version : Nat)
-    (line character : Nat) : Request :=
-  ({ path, version, line, character } : Beam.Lean.PositionInput).toSignatureHelpBrokerRequest
+def leanSignatureHelpRequest (position : Beam.Lean.PositionInput) : Request :=
+  position.toSignatureHelpBrokerRequest
 
-def leanDefinitionRequest
-    (path : String)
-    (version : Nat)
-    (line character : Nat) : Request :=
-  ({ path, version, line, character } : Beam.Lean.PositionInput).toDefinitionBrokerRequest
+def leanDefinitionRequest (position : Beam.Lean.PositionInput) : Request :=
+  position.toDefinitionBrokerRequest
 
 def leanReferencesRequest
-    (path : String)
-    (version : Nat)
-    (line character : Nat)
+    (position : Beam.Lean.PositionInput)
     (includeDeclaration : Bool := true) : Request :=
   ({
-    path
-    version
-    line
-    character
+    toPositionInput := position
     includeDeclaration? := some includeDeclaration
   } : Beam.Lean.ReferencesInput).toBrokerRequest
 
-def leanDocumentSymbolsRequest
-    (path : String)
-    (version : Nat) : Request :=
-  ({ path, version } : Beam.Lean.DocumentSymbolsInput).toBrokerRequest
+def leanDocumentSymbolsRequest (document : Beam.Lean.DocumentInput) : Request :=
+  document.toDocumentSymbolsBrokerRequest
 
 def leanWorkspaceSymbolsRequest
     (query : String) : Request :=
   ({ query } : Beam.Lean.WorkspaceSymbolsInput).toBrokerRequest
 
 def leanGoalsRequest
-    (path : String)
-    (version : Nat)
-    (line character : Nat)
+    (position : Beam.Lean.PositionInput)
     (mode : GoalMode) : Request :=
-  ({ path, version, line, character } : Beam.Lean.PositionInput).toGoalsBrokerRequest mode
+  position.toGoalsBrokerRequest mode
 
 def leanTodoRequest
     (path : String)
-    (version : Nat)
+    (snapshot : SnapshotRef)
     (startLine startCharacter endLine endCharacter : Nat)
     (kinds? : Option (Array Beam.LSP.Todo.TodoKind))
     (suggest? : Option Beam.LSP.Todo.TodoSuggestMode) : Request :=
   ({
     path
-    version
+    snapshot
     startLine
     startCharacter
     endLine
diff --git a/Beam/Cli/Usage.lean b/Beam/Cli/Usage.lean
index d0641c13..d50cf84a 100644
--- a/Beam/Cli/Usage.lean
+++ b/Beam/Cli/Usage.lean
@@ -14,16 +14,16 @@ def usage : String :=
     "  lean-beam --version",
     "  lean-beam version",
     "  lean-beam [--root PATH] [--session-dir DIR] serve [lean|rocq]",
-    "  lean-beam [--root PATH] run-at <path> <version> <line> <character> (--stdin | --text-file <path> | -- <text...> | <text...>)",
-    "  lean-beam [--root PATH] run-at-handle <path> <version> <line> <character> (--stdin | --text-file <path> | -- <text...> | <text...>)",
-    "  lean-beam [--root PATH] hover <path> <version> <line> <character>",
-    "  lean-beam [--root PATH] signature-help <path> <version> <line> <character>",
-    "  lean-beam [--root PATH] definition <path> <version> <line> <character>",
-    "  lean-beam [--root PATH] references <path> <version> <line> <character> [--include-declaration|--exclude-declaration]",
-    "  lean-beam [--root PATH] document-symbols <path> <version>",
+    "  lean-beam [--root PATH] run-at <path> <snapshot> <line> <character> (--stdin | --text-file <path> | -- <text...> | <text...>)",
+    "  lean-beam [--root PATH] run-at-handle <path> <snapshot> <line> <character> (--stdin | --text-file <path> | -- <text...> | <text...>)",
+    "  lean-beam [--root PATH] hover <path> <snapshot> <line> <character>",
+    "  lean-beam [--root PATH] signature-help <path> <snapshot> <line> <character>",
+    "  lean-beam [--root PATH] definition <path> <snapshot> <line> <character>",
+    "  lean-beam [--root PATH] references <path> <snapshot> <line> <character> [--include-declaration|--exclude-declaration]",
+    "  lean-beam [--root PATH] document-symbols <path> <snapshot>",
     "  lean-beam [--root PATH] workspace-symbols <query...>",
-    "  lean-beam [--root PATH] goals before|after <path> <version> <line> <character>",
-    "  lean-beam [--root PATH] todo <path> <version> <startLine> <startCharacter> <endLine> <endCharacter> [--kind <kind> ...] [--suggest none|basic]",
+    "  lean-beam [--root PATH] goals before|after <path> <snapshot> <line> <character>",
+    "  lean-beam [--root PATH] todo <path> <snapshot> <startLine> <startCharacter> <endLine> <endCharacter> [--kind <kind> ...] [--suggest none|basic]",
     "  lean-beam [--root PATH] run-with <path> <handle-json|-|--handle-file <path>> (--stdin | --text-file <path> | -- <text...> | <text...>)",
     "  lean-beam [--root PATH] run-with-linear <path> <handle-json|-|--handle-file <path>> (--stdin | --text-file <path> | -- <text...> | <text...>)",
     "  lean-beam [--root PATH] release <path> <handle-json|-|--handle-file <path>>",
@@ -50,12 +50,12 @@ def usage : String :=
     "Project-session commands accept an absolute --session-dir DIR as an exact alternate session selection.",
     "Use the same --root and --session-dir for serving, attachment, diagnostics, stopping, and recovery.",
     "Beam never applies source edits to `.lean` files on disk; the client applies source edits.",
-    "Lean edit loop: save the file, then run update for a broker document version.",
+    "Lean edit loop: save the file, then run update for a broker source snapshot.",
     "Run sync when you need the diagnostics/readiness barrier. save is sync plus a",
     "workspace-module checkpoint, refresh is close plus sync, and close-save",
     "adds closing the tracked file afterward.",
-    "Run update first, then pass its returned version to Lean position/range/document probes.",
-    "Separate run-at calls are independent probes on the broker document version they name.",
+    "Run update first, then pass its returned snapshot to Lean position/range/document probes.",
+    "Separate run-at calls are independent probes on the broker source snapshot they name.",
     "For exact speculative chaining, use run-at-handle and then run-with / run-with-linear.",
     "For multiline text-carrying Lean probes, prefer --stdin or --text-file <path>; use -- before",
     "text that itself starts with --.",
diff --git a/Beam/JsonPretty.lean b/Beam/JsonPretty.lean
index 2b04bd00..07949a5e 100644
--- a/Beam/JsonPretty.lean
+++ b/Beam/JsonPretty.lean
@@ -23,10 +23,10 @@ private def jsonFieldPriority : String -> Nat
   | "result" => 1
   | "error" => 2
   | "reason" => 13
-  | "expectedVersion" => 4
+  | "expectedVersion" | "expectedSnapshot" => 4
   | "acceptedVersion" => 5
   | "path" => 10
-  | "version" => 11
+  | "snapshot" => 11
   | "saveReady" => 12
   | "changed" => 14
   | "diagnostics" => 20
diff --git a/Beam/Lean/Operation.lean b/Beam/Lean/Operation.lean
index 36fc0d15..7323902f 100644
--- a/Beam/Lean/Operation.lean
+++ b/Beam/Lean/Operation.lean
@@ -104,8 +104,8 @@ private def operationDescription : Operation → String
   | .runWith => "Speculatively continue from a stored handle without consuming the parent handle. The continuation remains speculative and is not persisted as source. To keep the result, first edit and save the Lean file so it contains the complete accepted source; only then call the sync operation."
   | .runWithLinear => "Speculatively continue from a stored handle and consume that handle on success or failure. The continuation remains speculative and is not persisted as source. To keep the result, first edit and save the Lean file so it contains the complete accepted source; only then call the sync operation."
   | .release => "Release a stored Lean follow-up handle."
-  | .update => "Read the current on-disk Lean source into the broker's LSP mirror and return its document version without waiting for diagnostics."
-  | .sync => "Read the current on-disk Lean source into the broker's LSP mirror, wait for diagnostics and readiness, and return its document version. This never applies or recovers speculative text."
+  | .update => "Read the current on-disk Lean source into the broker's LSP mirror and return its document snapshot without waiting for diagnostics."
+  | .sync => "Read the current on-disk Lean source into the broker's LSP mirror, wait for diagnostics and readiness, and return its document snapshot. This never applies or recovers speculative text."
   | .refresh => "Close the tracked LSP document, reread the current on-disk Lean source, and wait for fresh diagnostics."
   | .save => "Read and synchronize the current on-disk Lean source, then write Lean/Lake build artifacts as a zero-build development checkpoint when possible."
   | .closeSave => "Read and synchronize the current on-disk Lean source, write the same Lean/Lake build artifacts when possible, and close the tracked LSP document."
@@ -132,8 +132,8 @@ def Operation.description (operation : Operation) : String :=
 private def pathField : String × Json :=
   ("path", Beam.JsonSchema.string "Lean file path, relative to the server root unless absolute.")
 
-private def versionField : String × Json :=
-  ("version", Beam.JsonSchema.natural "Document version returned by a successful update or sync operation for this file.")
+private def snapshotField : String × Json :=
+  ("snapshot", Beam.JsonSchema.string "Opaque snapshot token returned by update or sync for this file. After contentModified, read the source and resolve the target again before retrying with a fresh token.")
 
 private def lineField : String × Json :=
   ("line", Beam.JsonSchema.natural "Zero-based LSP line.")
@@ -200,15 +200,15 @@ private def diagnosticsInResultField : String × Json :=
 
 private def codeActionField : String × Json :=
   ("code_action", Beam.JsonSchema.object
-    "Raw Lean LSP CodeAction payload returned by the todo operation. The action must include its data field so Lean can resolve it against this document version.")
+    "Raw Lean LSP CodeAction payload returned by the todo operation. The action must include its data field so Lean can resolve it against this document snapshot.")
 
 private def positionFields : List (String × Json) :=
-  [pathField, versionField, lineField, characterField]
+  [pathField, snapshotField, lineField, characterField]
 
 private def rangeFields : List (String × Json) :=
   [
     pathField,
-    versionField,
+    snapshotField,
     rangeStartLineField,
     rangeStartCharacterField,
     rangeEndLineField,
@@ -216,27 +216,27 @@ private def rangeFields : List (String × Json) :=
   ]
 
 private def documentFields : List (String × Json) :=
-  [pathField, versionField]
+  [pathField, snapshotField]
 
 open Beam.JsonSchema in
 def Operation.inputSchema : Operation → Json
   | .runAt | .runAtHandle =>
-      inputObject (positionFields ++ [runAtTextField]) #["path", "version", "line", "character", "text"]
+      inputObject (positionFields ++ [runAtTextField]) #["path", "snapshot", "line", "character", "text"]
   | .hover | .signatureHelp | .definition =>
-      inputObject positionFields #["path", "version", "line", "character"]
+      inputObject positionFields #["path", "snapshot", "line", "character"]
   | .references =>
-      inputObject (positionFields ++ [includeDeclarationField]) #["path", "version", "line", "character"]
+      inputObject (positionFields ++ [includeDeclarationField]) #["path", "snapshot", "line", "character"]
   | .documentSymbols =>
-      inputObject documentFields #["path", "version"]
+      inputObject documentFields #["path", "snapshot"]
   | .workspaceSymbols =>
       inputObject [workspaceSymbolQueryField] #["query"]
   | .goals =>
-      inputObject (positionFields ++ [goalsModeField]) #["path", "version", "line", "character", "mode"]
+      inputObject (positionFields ++ [goalsModeField]) #["path", "snapshot", "line", "character", "mode"]
   | .todo =>
       inputObject (rangeFields ++ [kindsField, suggestField])
-        #["path", "version", "start_line", "start_character", "end_line", "end_character"]
+        #["path", "snapshot", "start_line", "start_character", "end_line", "end_character"]
   | .codeActionResolve =>
-      inputObject (documentFields ++ [codeActionField]) #["path", "version", "code_action"]
+      inputObject (documentFields ++ [codeActionField]) #["path", "snapshot", "code_action"]
   | .runWith | .runWithLinear =>
       inputObject [pathField, handleField, continuationTextField] #["path", "handle", "text"]
   | .release =>
@@ -254,23 +254,23 @@ def Operation.inputSchema : Operation → Json
 def Operation.validateInputFields (operation : Operation) (input : Json) : Except String Unit :=
   Beam.JsonSchema.validateInputFields operation.key operation.inputSchema input
 
-/-- Input for position-based Lean execution. Coordinates use LSP zero-based line/character units. -/
-structure RunAtInput where
+/-- A file and the opaque source token obtained from update or sync. -/
+structure DocumentInput where
   path : String
-  version : Nat
-  line : Nat
-  character : Nat
-  text : String
+  snapshot : SnapshotRef
   deriving FromJson, ToJson
 
-/-- Input for position-based Lean inspection operations. -/
-structure PositionInput where
-  path : String
-  version : Nat
+/-- A source-bound position in zero-based LSP line/character units. -/
+structure PositionInput extends DocumentInput where
   line : Nat
   character : Nat
   deriving FromJson, ToJson
 
+/-- Input for position-based Lean execution. -/
+structure RunAtInput extends PositionInput where
+  text : String
+  deriving FromJson, ToJson
+
 private def optionalField? [FromJson α] (j : Json) (field : String) : Except String (Option α) := do
   match j.getObjVal? field with
   | .ok value =>
@@ -281,39 +281,21 @@ private def optionalField? [FromJson α] (j : Json) (field : String) : Except St
       pure none
 
 /-- Input for Lean reference queries. -/
-structure ReferencesInput where
-  path : String
-  version : Nat
-  line : Nat
-  character : Nat
+structure ReferencesInput extends PositionInput where
   includeDeclaration? : Option Bool := none
 
 instance : ToJson ReferencesInput where
   toJson input :=
-    Json.mkObj <|
-      [ ("path", toJson input.path)
-      , ("version", toJson input.version)
-      , ("line", toJson input.line)
-      , ("character", toJson input.character)
-      ] ++
-      match input.includeDeclaration? with
-      | some includeDeclaration => [("include_declaration", toJson includeDeclaration)]
-      | none => []
+    let json := toJson input.toPositionInput
+    match input.includeDeclaration? with
+    | some includeDeclaration => json.setObjVal! "include_declaration" (toJson includeDeclaration)
+    | none => json
 
 instance : FromJson ReferencesInput where
   fromJson? j := do
-    let path ← j.getObjValAs? String "path"
-    let version ← j.getObjValAs? Nat "version"
-    let line ← j.getObjValAs? Nat "line"
-    let character ← j.getObjValAs? Nat "character"
+    let toPositionInput ← fromJson? j
     let includeDeclaration? ← optionalField? (α := Bool) j "include_declaration"
-    pure { path, version, line, character, includeDeclaration? }
-
-/-- Input for file-scoped Lean document symbol queries. -/
-structure DocumentSymbolsInput where
-  path : String
-  version : Nat
-  deriving FromJson, ToJson
+    pure { toPositionInput, includeDeclaration? }
 
 /-- Input for workspace-wide Lean symbol queries. -/
 structure WorkspaceSymbolsInput where
@@ -343,18 +325,12 @@ instance : FromJson GoalsMode where
     | j => .error s!"expected goals mode 'before' or 'after', got {j.compress}"
 
 /-- Input for read-only Lean goal inspection at a file position. -/
-structure GoalsInput where
-  path : String
-  version : Nat
-  line : Nat
-  character : Nat
+structure GoalsInput extends PositionInput where
   mode : GoalsMode
   deriving FromJson, ToJson
 
 /-- Input for range-based Lean todo inspection operations. -/
-structure TodoInput where
-  path : String
-  version : Nat
+structure TodoInput extends DocumentInput where
   startLine : Nat
   startCharacter : Nat
   endLine : Nat
@@ -366,7 +342,7 @@ instance : ToJson TodoInput where
   toJson input :=
     Json.mkObj <|
       [ ("path", toJson input.path)
-      , ("version", toJson input.version)
+      , ("snapshot", toJson input.snapshot)
       , ("start_line", toJson input.startLine)
       , ("start_character", toJson input.startCharacter)
       , ("end_line", toJson input.endLine)
@@ -381,36 +357,28 @@ instance : ToJson TodoInput where
 
 instance : FromJson TodoInput where
   fromJson? j := do
-    let path ← j.getObjValAs? String "path"
-    let version ← j.getObjValAs? Nat "version"
+    let toDocumentInput ← fromJson? j
     let startLine ← j.getObjValAs? Nat "start_line"
     let startCharacter ← j.getObjValAs? Nat "start_character"
     let endLine ← j.getObjValAs? Nat "end_line"
     let endCharacter ← j.getObjValAs? Nat "end_character"
     let kinds? ← optionalField? (α := Array Beam.LSP.Todo.TodoKind) j "kinds"
     let suggest? ← optionalField? (α := Beam.LSP.Todo.TodoSuggestMode) j "suggest"
-    pure { path, version, startLine, startCharacter, endLine, endCharacter, kinds?, suggest? }
+    pure { toDocumentInput, startLine, startCharacter, endLine, endCharacter, kinds?, suggest? }
 
 /-- Input for resolving a Lean code action returned by the todo operation. -/
-structure CodeActionResolveInput where
-  path : String
-  version : Nat
+structure CodeActionResolveInput extends DocumentInput where
   codeAction : Lean.Lsp.CodeAction
 
 instance : ToJson CodeActionResolveInput where
   toJson input :=
-    Json.mkObj [
-      ("path", toJson input.path),
-      ("version", toJson input.version),
-      ("code_action", toJson input.codeAction)
-    ]
+    (toJson input.toDocumentInput).setObjVal! "code_action" (toJson input.codeAction)
 
 instance : FromJson CodeActionResolveInput where
   fromJson? j := do
-    let path ← j.getObjValAs? String "path"
-    let version ← j.getObjValAs? Nat "version"
+    let toDocumentInput ← fromJson? j
     let codeAction ← j.getObjValAs? Lean.Lsp.CodeAction "code_action"
-    pure { path, version, codeAction }
+    pure { toDocumentInput, codeAction }
 
 /-- Input for handle-based Lean execution. -/
 structure RunWithInput where
@@ -473,63 +441,51 @@ instance : FromJson SaveInput where
     let diagnosticScope? ← optionalField? (α := Beam.Broker.DiagnosticScope) j "diagnostic_scope"
     pure { path, diagnosticScope? }
 
+private def DocumentInput.toRequestSnapshotFile (input : DocumentInput) :
+    Beam.Broker.RequestSnapshotFile := {
+  path := input.path
+  snapshot := input.snapshot
+}
+
+private def PositionInput.toRequestPosition (input : PositionInput) : Beam.Broker.RequestPosition := {
+  toRequestSnapshotFile := input.toDocumentInput.toRequestSnapshotFile
+  line := input.line
+  character := input.character
+}
+
 def RunAtInput.toBrokerRequest
     (input : RunAtInput)
     (storeHandle : Bool := false) : Beam.Broker.Request := {
   payload := .runAt {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
+    toRequestPosition := input.toPositionInput.toRequestPosition
     text := input.text
     storeHandle? := if storeHandle then some true else none
   }
 }
 
 def PositionInput.toHoverBrokerRequest (input : PositionInput) : Beam.Broker.Request := {
-  payload := .hover {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
-  }
+  payload := .hover input.toRequestPosition
 }
 
 def PositionInput.toSignatureHelpBrokerRequest (input : PositionInput) :
     Beam.Broker.Request := {
-  payload := .signatureHelp {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
-  }
+  payload := .signatureHelp input.toRequestPosition
 }
 
 def PositionInput.toDefinitionBrokerRequest (input : PositionInput) : Beam.Broker.Request := {
-  payload := .definition {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
-  }
+  payload := .definition input.toRequestPosition
 }
 
 def ReferencesInput.toBrokerRequest (input : ReferencesInput) : Beam.Broker.Request := {
   payload := .references {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
+    toRequestPosition := input.toPositionInput.toRequestPosition
     includeDeclaration? := input.includeDeclaration?
   }
 }
 
-def DocumentSymbolsInput.toBrokerRequest (input : DocumentSymbolsInput) :
+def DocumentInput.toDocumentSymbolsBrokerRequest (input : DocumentInput) :
     Beam.Broker.Request := {
-  payload := .documentSymbols {
-    path := input.path
-    version := input.version
-  }
+  payload := .documentSymbols input.toRequestSnapshotFile
 }
 
 def WorkspaceSymbolsInput.toBrokerRequest (input : WorkspaceSymbolsInput) :
@@ -541,28 +497,21 @@ def PositionInput.toGoalsBrokerRequest
     (input : PositionInput)
     (mode : Beam.Broker.GoalMode) : Beam.Broker.Request := {
   payload := .goals {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
+    toRequestPosition := input.toRequestPosition
     mode? := some mode
   }
 }
 
 def GoalsInput.toBrokerRequest (input : GoalsInput) : Beam.Broker.Request := {
   payload := .goals {
-    path := input.path
-    version := input.version
-    line := input.line
-    character := input.character
+    toRequestPosition := input.toPositionInput.toRequestPosition
     mode? := some input.mode.toBrokerMode
   }
 }
 
 def TodoInput.toBrokerRequest (input : TodoInput) : Beam.Broker.Request := {
   payload := .todo {
-    path := input.path
-    version := input.version
+    toRequestSnapshotFile := input.toDocumentInput.toRequestSnapshotFile
     line := input.startLine
     character := input.startCharacter
     endLine := input.endLine
@@ -575,8 +524,7 @@ def TodoInput.toBrokerRequest (input : TodoInput) : Beam.Broker.Request := {
 def CodeActionResolveInput.toBrokerRequest
     (input : CodeActionResolveInput) : Beam.Broker.Request := {
   payload := .codeActionResolve {
-    path := input.path
-    version := input.version
+    toRequestSnapshotFile := input.toDocumentInput.toRequestSnapshotFile
     codeAction := input.codeAction
   }
 }
@@ -657,7 +605,7 @@ def Operation.toBrokerRequest
   | .references =>
       pure <| (← fromJson? (α := ReferencesInput) input).toBrokerRequest
   | .documentSymbols =>
-      pure <| (← fromJson? (α := DocumentSymbolsInput) input).toBrokerRequest
+      pure <| (← fromJson? (α := DocumentInput) input).toDocumentSymbolsBrokerRequest
   | .workspaceSymbols =>
       pure <| (← fromJson? (α := WorkspaceSymbolsInput) input).toBrokerRequest
   | .goals =>
diff --git a/Beam/Mcp/Projection.lean b/Beam/Mcp/Projection.lean
index cd8f0064..44f7fccb 100644
--- a/Beam/Mcp/Projection.lean
+++ b/Beam/Mcp/Projection.lean
@@ -282,7 +282,7 @@ def ToolName.validateInputFields (tool : ToolName) (input : Json) : Except Strin
 abbrev RunAtInput := Beam.Lean.RunAtInput
 abbrev PositionInput := Beam.Lean.PositionInput
 abbrev ReferencesInput := Beam.Lean.ReferencesInput
-abbrev DocumentSymbolsInput := Beam.Lean.DocumentSymbolsInput
+abbrev DocumentInput := Beam.Lean.DocumentInput
 abbrev WorkspaceSymbolsInput := Beam.Lean.WorkspaceSymbolsInput
 abbrev GoalsInput := Beam.Lean.GoalsInput
 abbrev TodoInput := Beam.Lean.TodoInput
@@ -418,8 +418,8 @@ def diagnosticJson (diagnostic : Beam.Broker.StreamDiagnostic) : Json :=
     (match diagnostic.saveBlocking? with
     | some saveBlocking => [("save_blocking", toJson saveBlocking)]
     | none => []) ++
-    match diagnostic.version? with
-    | some version => [("version", toJson version)]
+    match diagnostic.snapshot? with
+    | some snapshot => [("snapshot", toJson snapshot)]
     | none => []
 
 private def blockingDiagnosticJson (diagnostic : Beam.Broker.SyncBlockingDiagnostic) : Json :=
@@ -445,7 +445,7 @@ private def syncResultJson (result : Beam.Broker.SyncFileResult) : Json :=
     | none => []
   Json.mkObj [
     ("path", toJson result.path),
-    ("version", toJson result.version),
+    ("snapshot", toJson result.snapshot),
     ("diagnostics", Json.mkObj <|
       [("counts", toJson result.diagnostics.counts)] ++ diagnosticFields),
     ("readiness", Json.mkObj [
@@ -469,7 +469,7 @@ private def saveResultJson (result : Beam.Broker.SaveOleanResult) : Json :=
     [
       ("path", toJson result.path),
       ("module", toJson result.module),
-      ("version", toJson result.version),
+      ("snapshot", toJson result.snapshot),
       ("source_hash", toJson result.sourceHash),
       ("olean", toJson result.olean),
       ("ilean", toJson result.ilean),
diff --git a/Beam/Snapshot.lean b/Beam/Snapshot.lean
new file mode 100644
index 00000000..4f358197
--- /dev/null
+++ b/Beam/Snapshot.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Emilio J. Gallego Arias
+-/
+
+import Lean
+
+namespace Beam
+
+/-- A broker-owned source snapshot. Clients round-trip its opaque string representation. -/
+structure SnapshotRef where
+  session : String
+  revision : Nat
+  deriving BEq, Repr
+
+namespace SnapshotRef
+
+def encode (snapshot : SnapshotRef) : String :=
+  s!"{snapshot.session}/{snapshot.revision}"
+
+private def invalidSnapshot : String :=
+  "snapshot must be an opaque token returned by update or sync"
+
+def decode (text : String) : Except String SnapshotRef := do
+  match text.splitOn "/" with
+  | [session, revisionText] =>
+      unless !session.isEmpty do
+        throw invalidSnapshot
+      let some revision := revisionText.toNat?
+        | throw invalidSnapshot
+      unless revision > 0 && toString revision == revisionText do
+        throw invalidSnapshot
+      pure { session, revision }
+  | _ => throw invalidSnapshot
+
+end SnapshotRef
+
+instance : ToString SnapshotRef := ⟨SnapshotRef.encode⟩
+instance : Lean.ToJson SnapshotRef := ⟨fun snapshot => Lean.toJson snapshot.encode⟩
+instance : Lean.FromJson SnapshotRef := ⟨fun json => do
+  SnapshotRef.decode (← json.getStr?)⟩
+
+end Beam
diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md
index 91fadeb6..ac0fba7f 100644
--- a/docs/DEVELOPMENT.md
+++ b/docs/DEVELOPMENT.md
@@ -74,7 +74,7 @@ Preferred maintainer entrypoints:
 - [docs/STATUS.md](STATUS.md) is the public beta scope, limitation, and direction summary
 - [docs/MCP.md](MCP.md) owns MCP implementation, protocol, tool-list, and conformance notes
 - [docs/SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md) owns the exact sync, refresh, save,
-  progress, diagnostics, readiness, and stale-version contract
+  progress, diagnostics, readiness, and stale-snapshot contract
 - [docs/COMPATIBILITY.md](COMPATIBILITY.md),
   [validated-lean-toolchains](../validated-lean-toolchains), and
   [compatible-lean-release-lines](../compatible-lean-release-lines) own compatibility targets
@@ -273,7 +273,7 @@ completed. Use the closed `BrokerFailure` code set for failures generated by Bea
 against its closed `Operation.inputSchema` before typed decoding. Keep sync/refresh and
 save/close-save operation inputs separate: only sync-like inputs may carry final diagnostic replay
 control. Likewise, keep redundant wire observations derived internally: diagnostic `total` is the
-severity sum, save `path` and `version` come from its nested sync result, and a decoded close-save
+severity sum, save `path` and `snapshot` come from its nested sync result, and a decoded close-save
 result is always closed.
 
 ### Internal Broker Stream Contract
@@ -399,6 +399,14 @@ request handlers reserve a sequence number under the broker mutex, read and hash
 mutex, then ignore a completed snapshot if a newer read has already been applied to the same document.
 In-session syncs use sequence zero because they run inside the already-ordered session flow.
 
+`SnapshotRef` combines the backend session identity with a session-wide document revision. Keep
+revision allocation in the pure `DocumentState.syncFileDecision` transition, and persist its returned
+allocator with its document map. Closing a file removes the document but retains the allocator.
+Complete readonly document requests and sync barriers through the same current-document check under
+the broker state mutex. Native LSP parameters come from the accepted `DocState`, while clients
+round-trip the opaque token. Diagnostic publications with explicit revisions must match the pending
+request before contributing completion evidence.
+
 Keep readiness claims deliberately narrow: `fileProgress` is an observable LSP progress signal, and
 it is a barrier input only for the operations that define a diagnostics/save barrier (`sync`,
 `refresh`, `save`, and `close-save`). It is not a general semantic-ready signal, and it is not the
diff --git a/docs/MCP.md b/docs/MCP.md
index 8b80af57..df8ff4ed 100644
--- a/docs/MCP.md
+++ b/docs/MCP.md
@@ -240,8 +240,10 @@ the broken identity. Restart an agent or MCP client for `runtime_current: false`
 work.
 
 Direct MCP clients should call `lean_update` or `lean_sync` before snapshot-bound operations and
-pass the returned `version` for the same descriptor and path. `lean_workspace_symbols` is
-workspace-scoped but has no document version. `lean_run_with`, `lean_run_with_linear`, and
+pass the returned `snapshot` for the same descriptor and path. Token lifetimes and stale-state
+recovery follow the [source snapshot contract](SYNC_AND_DIAGNOSTICS.md#command-model).
+`lean_workspace_symbols` is
+workspace-scoped but has no document snapshot. `lean_run_with`, `lean_run_with_linear`, and
 `lean_release` take an opaque handle returned by a previous handle operation. The supplied workspace
 descriptor must resolve to the same private runtime identity carried by that handle. `lean_goals`
 also requires `mode: "before"` or `mode: "after"`.
@@ -261,7 +263,7 @@ needed. Both commands read the current on-disk file; neither applies or recovers
 
 `lean_code_action_resolve` takes a `code_action` payload previously returned by `lean_todo`. Clients
 apply any returned LSP `WorkspaceEdit` themselves, then call `lean_update` or `lean_sync` again so
-Beam observes the edited file and reports the new version. Use `lean_sync` instead of `lean_update`
+Beam observes the edited file and reports the new snapshot. Use `lean_sync` instead of `lean_update`
 when the client also needs the diagnostics/readiness barrier.
 
 `lean_save` and `lean_close_save` create development checkpoints from the accepted Lean server
@@ -397,7 +399,7 @@ The `structuredContent` for a clean `lean_sync` has this semantic shape (counts
 {
   "workspace": {"root": "/work/demo"},
   "path": "Main.lean",
-  "version": 3,
+  "snapshot": "example-session/3",
   "diagnostics": {
     "counts": {"error": 0, "warning": 0, "information": 0, "hint": 0, "unknown": 0, "total": 0}
   },
@@ -413,7 +415,7 @@ The `structuredContent` for a clean `lean_sync` has this semantic shape (counts
 ```
 
 `lean_save` returns artifact paths plus `sync` containing that same
-path/version/diagnostics/readiness object. Optional backend artifacts (`olean_server`,
+path/snapshot/diagnostics/readiness object. Optional backend artifacts (`olean_server`,
 `olean_private`, `ir`, and `bc`) appear only when Lean produced them:
 
 ```json
@@ -421,7 +423,7 @@ path/version/diagnostics/readiness object. Optional backend artifacts (`olean_se
   "workspace": {"root": "/work/demo"},
   "path": "Main.lean",
   "module": "Main",
-  "version": 3,
+  "snapshot": "example-session/3",
   "source_hash": "9a9bdc9950870951",
   "olean": "/work/demo/.lake/build/lib/lean/Main.olean",
   "ilean": "/work/demo/.lake/build/lib/lean/Main.ilean",
@@ -429,7 +431,7 @@ path/version/diagnostics/readiness object. Optional backend artifacts (`olean_se
   "trace": "/work/demo/.lake/build/lib/lean/Main.olean.trace",
   "sync": {
     "path": "Main.lean",
-    "version": 3,
+    "snapshot": "example-session/3",
     "diagnostics": {
       "counts": {"error": 0, "warning": 0, "information": 0, "hint": 0, "unknown": 0, "total": 0}
     },
@@ -474,11 +476,11 @@ tool arguments, but only on the tools listed below. Log delivery is session-wide
 
 | Tool or family | With `_meta.progressToken` | Without a token | Diagnostic arguments | Stable final result |
 | --- | --- | --- | --- | --- |
-| `lean_sync`, `lean_refresh` | Preparation, throttled Lake setup, and file-progress updates. | One `beam.status` on the first setup observation or after two seconds. | `diagnostic_scope`, `diagnostics_in_result` | Path/version, complete diagnostic counts, readiness, `document_progress`, and optional diagnostic items. |
+| `lean_sync`, `lean_refresh` | Preparation, throttled Lake setup, and file-progress updates. | One `beam.status` on the first setup observation or after two seconds. | `diagnostic_scope`, `diagnostics_in_result` | Path/snapshot, complete diagnostic counts, readiness, `document_progress`, and optional diagnostic items. |
 | `lean_save`, `lean_close_save` | Preparation, throttled Lake setup, and file-progress updates. | One `beam.status` on the first setup observation or after two seconds. | `diagnostic_scope` | Checkpoint result embedding the same sync/readiness result and `document_progress`; no diagnostic replay argument. |
 | `lean_run_at`, `lean_run_at_handle` | Preparation, Lake setup when observed, and file progress when Lean publishes it. | One `beam.status` on the first setup observation or after two seconds. | None | Run result messages, traces, proof state, and optional handle; no final `document_progress` or full-file diagnostic replay. |
 | `lean_run_with`, `lean_run_with_linear` | Preparation and file progress when Lean publishes it. | One `beam.status` after two seconds. | None | Continuation result and optional next handle. |
-| `lean_update` | Preparation phase only. | One `beam.status` after two seconds. | None | New document version and changed flag; no readiness barrier. |
+| `lean_update` | Preparation phase only. | One `beam.status` after two seconds. | None | New document snapshot and changed flag; no readiness barrier. |
 | `lean_hover`, `lean_signature_help`, `lean_definition`, `lean_references`, `lean_document_symbols`, `lean_goals`, `lean_todo`, `lean_code_action_resolve` | Preparation and file progress when Lean publishes it. | One `beam.status` after two seconds. | None | Operation-specific structured result. |
 | `lean_workspace_symbols` | Preparation phase only. | One pathless `beam.status` after two seconds. | None | Workspace-symbol result. |
 | `lean_release`, `lean_close` | Preparation, plus file progress for release when Lean publishes it. | One `beam.status` after two seconds if the normally short call is delayed. | None | Release/close result. |
diff --git a/docs/SETUP.md b/docs/SETUP.md
index 627df973..e4df9d73 100644
--- a/docs/SETUP.md
+++ b/docs/SETUP.md
@@ -218,11 +218,11 @@ lean-beam serve
 # terminal/session 2
 update_json="$(lean-beam update "Foo.lean")"
 printf '%s\n' "$update_json"
-version="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["version"])')"
-lean-beam hover "Foo.lean" "$version" 10 2
-lean-beam definition "Foo.lean" "$version" 10 2
-lean-beam goals before "Foo.lean" "$version" 10 2
-lean-beam run-at "Foo.lean" "$version" 10 2 "exact trivial"
+snapshot="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+lean-beam hover "Foo.lean" "$snapshot" 10 2
+lean-beam definition "Foo.lean" "$snapshot" 10 2
+lean-beam goals before "Foo.lean" "$snapshot" 10 2
+lean-beam run-at "Foo.lean" "$snapshot" 10 2 "exact trivial"
 ```
 
 `lean-beam serve` is the only wrapper command that starts a project session. Its
@@ -314,8 +314,8 @@ human-readable stderr diagnostic and no JSON. Use MCP when a client requires str
 progress, diagnostics, or failures; Beam intentionally does not expose its raw port, session
 capability, or generic broker request record as an installed client interface.
 
-The `python3` line extracts `result.version` for shell examples. You can also copy that version
-number from the printed `lean-beam update` JSON.
+The `python3` line extracts `result.snapshot` for shell examples. You can also copy that snapshot
+string from the printed `lean-beam update` JSON.
 
 Beam reads the saved file on disk, not unsaved editor buffers. After a real source edit, save the
 file normally and then update or sync that workspace module before trusting later probes:
@@ -329,24 +329,26 @@ For multiline speculative Lean text, pass the text on stdin:
 
 ```bash
 printf '%s\n' 'example : True := by' '  trivial' |
-  lean-beam run-at "Foo.lean" "$version" 10 2 --stdin
+  lean-beam run-at "Foo.lean" "$snapshot" 10 2 --stdin
 ```
 
 Read those commands like this:
 
 - `lean-beam update` opens or updates the broker's LSP mirror and returns the current document
-  version without waiting for diagnostics
+  snapshot without waiting for diagnostics
 - `lean-beam run-at` tries speculative Lean text without editing the file
 - `lean-beam sync` waits for diagnostics/readiness after a real saved edit
 - `lean-beam refresh` is `lean-beam close` plus `lean-beam sync`
 - `lean-beam save` checkpoints one synced workspace module; it does not validate downstream importers
 - `lean-beam doctor` explains toolchain support and runtime bundle selection
 
-Position and range probes are version-bound. Use the `version` returned by `lean-beam update` or
+Position and range probes are snapshot-bound. Use the `snapshot` returned by `lean-beam update` or
 `lean-beam sync` for `run-at`, `hover`, `signature-help`, `definition`, `references`,
 `document-symbols`, `goals`, and `todo`. Workspace symbol queries are workspace-scoped and do not
-take a file version. If Beam reports `contentModified`, update or sync the file again and retry
-with the accepted current version rather than guessing.
+take a file snapshot. If Beam reports `contentModified`, update or sync the file again and retry
+only after reading the current source and resolving the intended target again. A fresh snapshot
+token does not repair old coordinates or code actions. See the
+[full snapshot and recovery contract](SYNC_AND_DIAGNOSTICS.md#command-model).
 
 Useful follow-up commands:
 
@@ -359,7 +361,7 @@ lean-beam save "MyPkg/Sub/Module.lean"
 `lean-beam open-files` reports only documents tracked by the current project daemon. Each file's
 `diskStatus` is `matchesTracked`, `differsFromTracked`, `missing`, or `unknown`, comparing the current
 on-disk source with the broker's tracked text. `checkpointed` means this daemon recorded a successful
-`lean-beam save` for that tracked version and the source still matches. It does not revalidate Lake
+`lean-beam save` for that tracked snapshot and the source still matches. It does not revalidate Lake
 artifacts or predict whether another save will succeed; `lean-beam save` is authoritative for those
 checks.
 
diff --git a/docs/STATUS.md b/docs/STATUS.md
index 61655e51..3323135f 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -29,7 +29,7 @@ Pre-stable compatibility policy lives in [Compatibility Policy](COMPATIBILITY.md
 - explicit Lean `lean-beam sync` barrier with diagnostics wait and compact `fileProgress` reporting
 - zero-build `lean-beam save` development checkpoint for one synced workspace module, including
   structured Lake setup already applied by the Lean file worker
-- typed sync summaries with current diagnostic/readiness counts for the synced document version
+- typed sync summaries with current diagnostic/readiness counts for the synced document snapshot
 
 ### Local Beam Layer
 
@@ -113,16 +113,15 @@ The `lean-beam update`, `lean-beam sync`, `lean-beam save`, and `lean-beam close
 a progression:
 
 - `lean-beam update` opens or updates the broker's LSP mirror and returns the current document
-  version without waiting for diagnostics
-- `lean-beam sync` establishes the diagnostics-complete saved file snapshot for the current document
-  version
+  snapshot without waiting for diagnostics
+- `lean-beam sync` waits for diagnostics/readiness for the saved source and returns its snapshot
 - `lean-beam save` creates a development checkpoint from that server snapshot for one module
 - `lean-beam close-save` creates the same checkpoint and then closes the tracked file
 
-Position/range/document operations are version-bound across the broker, MCP, and wrapper surfaces.
-Clients first update or sync a saved file, then pass the returned document version to later probes.
-Workspace symbol queries are workspace-scoped and do not take a file version. The canonical
-field-level contract for update, sync, save, progress, diagnostics, stale-version failures,
+Position/range/document operations are snapshot-bound across the broker, MCP, and wrapper surfaces.
+Clients first update or sync a saved file, then pass the returned opaque `snapshot` token to later probes.
+Workspace symbol queries are workspace-scoped and do not take a file snapshot. The canonical
+field-level contract for update, sync, save, progress, diagnostics, stale-snapshot failures,
 readiness, and recovery hints lives in [SYNC_AND_DIAGNOSTICS.md](SYNC_AND_DIAGNOSTICS.md).
 
 If a speculative probe looks right and should become real source, the current contract is still:
diff --git a/docs/SYNC_AND_DIAGNOSTICS.md b/docs/SYNC_AND_DIAGNOSTICS.md
index e6bda2da..fe261929 100644
--- a/docs/SYNC_AND_DIAGNOSTICS.md
+++ b/docs/SYNC_AND_DIAGNOSTICS.md
@@ -11,42 +11,53 @@ a source-editing command.
 
 `lean-beam update` is the cheap on-disk edit observation for a Lean file. It reads the current file,
 opens or updates the broker's LSP mirror when needed, and returns the broker-owned document
-`version` immediately without waiting for diagnostics. Its `changed` flag means the broker sent
+`snapshot` immediately without waiting for diagnostics. Its `changed` flag means the broker sent
 `didOpen` or `didChange` to the LSP session for this request; unchanged files keep the previous
-document version and return `changed: false`.
+document snapshot and return `changed: false`.
 
 `lean-beam sync` is the diagnostics/readiness barrier for a Lean file. It opens or updates the
-tracked file, waits for diagnostics for the current document version, streams fresh request
-diagnostics, and returns a machine-readable JSON verdict for that version. Wrapper stdout uses
+tracked file, waits for diagnostics for the current document snapshot, streams fresh request
+diagnostics, and returns a machine-readable JSON verdict for that snapshot. Wrapper stdout uses
 stable, agent-oriented field ordering after a broker operation completes. Selector, setup, or
 transport failures can instead exit nonzero with human-facing stderr and no JSON, so automation
 must check the exit status before parsing stdout. Clients that require structured live events and
 failures should use MCP.
 
-The returned document `version` is the snapshot token for broker, MCP, and wrapper callers.
-Position- or range-bound operations reject missing or stale versions; clients can obtain the
-version from `lean-beam update`, the internal broker `update_file` operation, or MCP `lean_update`.
-`lean-beam sync`, the internal broker `sync_file` operation, and MCP `lean_sync` also return the
-current version when the caller needs the diagnostics/readiness barrier.
-
-When the broker rejects a position- or range-bound request because the supplied version is stale,
-the failure uses `contentModified` and includes `error.data.reason = "documentVersionMismatch"`.
-The same payload reports `expectedVersion`, the currently accepted `acceptedVersion`, and
-`currentVersion` when the broker can name the current tracked document version.
-
-Example stale-version semantic response as printed by the wrapper on stdout:
+The returned `snapshot` is an opaque string identifying this file's source in one backend session.
+Pass it unchanged to position, range, document-symbol, and code-action resolution requests for the
+same workspace and file. `update` and `sync` preserve the token for unchanged tracked source.
+Source changes, refresh, close/reopen, backend restart, and workspace reset or recreation produce
+fresh tokens, even when the text is identical. Tokens from another file are also rejected.
+This source token identifies the whole tracked document. Lean's elaboration snapshots are the
+internal command or proof states at particular positions within that source. Native LSP revisions
+may appear in backend error details, but numeric `version` arguments are not accepted by the wrapper
+or MCP.
+
+The broker checks the token before dispatch and verifies that the document is still current before
+returning a document request's result or completing a sync barrier. A stale token produces
+`contentModified` with
+`error.data.reason = "snapshotMismatch"`, `expectedSnapshot`, and `currentSnapshot` when the file is
+still tracked. A backend that exits while a request is pending can instead produce `workerExited`.
+These checks concern the source tracked by the broker; they do not detect unsupported workspace
+configuration drift or guarantee that imported artifacts are current.
+
+After `contentModified`, read the current source and resolve the intended position, range, or code
+action again. Obtain a fresh token from `update` or `sync` before retrying. Replacing the token alone
+does not repair stale coordinates or actions. Treat tokens as opaque: do not construct, increment,
+or compare their internal parts.
+
+Example stale-snapshot response as printed by the wrapper on stdout:
 
 ```json
 {
   "ok": false,
   "error": {
     "code": "contentModified",
-    "message": "document version mismatch for file:///workspace/Foo.lean: expected document version 1, got 2",
+    "message": "source snapshot changed for file:///workspace/Foo.lean; read the source and resolve the intended target again before retrying",
     "data": {
-      "reason": "documentVersionMismatch",
-      "expectedVersion": 1,
-      "acceptedVersion": 2,
-      "currentVersion": 2,
+      "reason": "snapshotMismatch",
+      "expectedSnapshot": "example-session/1",
+      "currentSnapshot": "example-session/2",
       "uri": "file:///workspace/Foo.lean"
     }
   }
@@ -116,7 +127,7 @@ Their transport types differ by surface.
 | Progress | Request-scoped operation movement, not diagnostics and not final readiness. | MCP `notifications/progress`; internal broker `fileProgress` events; CLI progress text. |
 | Status | Best-effort notice that a no-token MCP request is doing setup or remains pending. | MCP `notifications/message` with logger `beam.status`. |
 | Streamed diagnostics | Lean-published events observed while a request is pending. | MCP `notifications/message` with logger `lean.diagnostic`; internal broker `diagnostic` events; CLI stderr diagnostics. |
-| Current result | Stable synced-state verdict for one document version. | Final internal broker response or wrapper stdout `diagnostics`, `readiness`, and `fileProgress` fields; MCP spells the progress field `document_progress`. |
+| Current result | Stable synced-state verdict for one document snapshot. | Final internal broker response or wrapper stdout `diagnostics`, `readiness`, and `fileProgress` fields; MCP spells the progress field `document_progress`. |
 
 Wrapper stderr is the human-facing surface. Machine consumers of an owned wrapper session should
 check exit status, then parse final stdout JSON when present. Use MCP for structured live events and
@@ -145,9 +156,13 @@ The MCP server advertises logging and forwards incremental Lean diagnostics as s
 `notifications/message` log events. Modern callers opt in for each request with
 `_meta["io.modelcontextprotocol/logLevel"]`; legacy callers set the connection-wide level with
 `logging/setLevel`. [MCP.md](MCP.md#progress-and-diagnostic-logs) defines the exact behavior for
-both protocol eras. Events include path, URI, version, range, severity, message data, and
+both protocol eras. Events include path, URI, range, severity, message data, and
 `completion_blocking=true` when a diagnostic is known to block file completion. They are
 request-scoped observations; save-blocking evidence is attached to the final sync/save verdict.
+Notifications with an explicit revision must match the request's tracked document revision before
+they can affect completion evidence or stream diagnostics. Their diagnostic events include `snapshot`.
+Unversioned notifications remain best-effort observations and omit the token; their events do not
+suppress an otherwise identical versioned event. Reply diagnostic items carry the barrier snapshot.
 
 MCP clients that cannot conveniently collect interleaved notifications can call `lean_sync` or
 `lean_refresh` with `diagnostics_in_result: true` to replay diagnostics in the final structured
@@ -208,7 +223,7 @@ request can return before the whole file reaches `done = true`.
 
 ## Readiness
 
-Successful sync responses expose one flat result for the current document version. MCP uses
+Successful sync responses expose one flat result for the current document snapshot. MCP uses
 snake_case field names; broker and CLI JSON use the corresponding camelCase names. The
 machine-facing MCP readiness fields are:
 
@@ -219,7 +234,7 @@ machine-facing MCP readiness fields are:
 - `readiness.blocking_messages`
 
 `diagnostics.counts.*` reports user-facing Lean-published diagnostic severities. It answers "what
-did Lean report?", while readiness answers "can this synced version be checkpointed?". The backend
+did Lean report?", while readiness answers "can this synced snapshot be checkpointed?". The backend
 readiness API is authoritative for `saveReady`; diagnostic severity summaries are evidence and
 counts, not a separate broker-side veto.
 
@@ -234,16 +249,16 @@ and message history are observations; clients should not reconstruct save readin
 
 ## Current Result
 
-Each sync result describes only the current synced document version. It does not carry deltas
+Each sync result describes only the current synced document snapshot. It does not carry deltas
 against previous responses. Clients that need comparisons should retain the previous response they
 care about and compare it explicitly.
 
-- `path` and `version`: the synced document described by the result
+- `path` and `snapshot`: the synced document described by the result
 - `diagnostics.counts`: current user-facing diagnostic counts by severity and total
 - `diagnostics.items`, when requested: diagnostics selected by `diagnostic_scope`
 - `readiness`: the current save-readiness verdict and blocking evidence
 
-Successful broker and wrapper saves repeat the synced document's top-level `path` and `version`, add
+Successful broker and wrapper saves repeat the synced document's top-level `path` and `snapshot`, add
 the checkpoint fields `module`, `sourceHash`, `olean`, `ilean`, `c`, and `trace`, and nest the
 canonical sync result under `sync`. Optional backend artifacts use `oleanServer`, `oleanPrivate`,
 `ir`, and `bc`. Close-save wraps the same save result as
@@ -252,7 +267,7 @@ see the complete [`lean_save` result example](MCP.md#stable-result-shapes).
 
 ## Failures And Recovery
 
-If Lean cannot reach a completed diagnostics barrier for the synced version, `lean-beam sync` fails
+If Lean cannot reach a completed diagnostics barrier for the synced snapshot, `lean-beam sync` fails
 instead of reporting partial success. `lean-beam save` and `lean-beam close-save` refuse to proceed
 past that incomplete barrier.
 
diff --git a/scripts/lean-beam-search b/scripts/lean-beam-search
index 9df564b0..6803e9e1 100755
--- a/scripts/lean-beam-search
+++ b/scripts/lean-beam-search
@@ -36,7 +36,7 @@ fi
 usage() {
   cat <<'EOF' >&2
 usage:
-  lean-beam-search [lean-beam opts...] mint <path> <version> <line> <character> <text...>
+  lean-beam-search [lean-beam opts...] mint <path> <snapshot> <line> <character> <text...>
   lean-beam-search [lean-beam opts...] branch <path> <text...>
   lean-beam-search [lean-beam opts...] linear <path> <text...>
   lean-beam-search [lean-beam opts...] playout <path> <step> [step...]
@@ -44,7 +44,7 @@ usage:
 
 notes:
   - branch, linear, playout, and release read a prior wrapper response or handle JSON from stdin
-  - mint requires the version returned by `lean-beam update <path>` or `lean-beam sync <path>`
+  - mint requires the snapshot returned by `lean-beam update <path>` or `lean-beam sync <path>`
   - lean-beam opts such as --root may appear before the subcommand
 EOF
   exit 1
@@ -77,14 +77,14 @@ case "$subcmd" in
   mint)
     [ "$#" -ge 5 ] || usage
     path="$1"
-    version="$2"
+    snapshot="$2"
     line="$3"
     character="$4"
     shift 4
     if [ -n "${prefix[*]-}" ]; then
-      exec "$cli_script" ${prefix[@]+"${prefix[@]}"} run-at-handle "$path" "$version" "$line" "$character" "$@"
+      exec "$cli_script" ${prefix[@]+"${prefix[@]}"} run-at-handle "$path" "$snapshot" "$line" "$character" "$@"
     else
-      exec "$cli_script" run-at-handle "$path" "$version" "$line" "$character" "$@"
+      exec "$cli_script" run-at-handle "$path" "$snapshot" "$line" "$character" "$@"
     fi
     ;;
   branch)
diff --git a/skills/lean-beam/SKILL.md b/skills/lean-beam/SKILL.md
index f3be1b63..10dce7c9 100644
--- a/skills/lean-beam/SKILL.md
+++ b/skills/lean-beam/SKILL.md
@@ -44,7 +44,7 @@ client so it launches the current runtime. If a newly resolved installed wrapper
 `false`, the install root's `current` link is missing or broken; stop normal Beam work and reinstall.
 If an installed identity reports `runtime_error`, do not treat it as a source checkout or try to
 clean it with `lean-beam prune`. After stopping active Beam agents and MCP clients, move an invalid
-manifest runtime out of `BEAM_INSTALL_ROOT/versions`, preserve it for inspection, and rerun the
+manifest runtime out of `BEAM_INSTALL_ROOT/snapshots`, preserve it for inspection, and rerun the
 installer. For an invalid install-root marker, preserve and rename the exact `BEAM_INSTALL_ROOT` as
 a unit before reinstalling; do not recreate its ownership marker in place or delete the preserved
 state.
@@ -68,7 +68,7 @@ family that fits the task.
 
 Agents may access Beam through the `lean-beam` wrapper or through a registered `lean-beam-mcp`
 server. This skill names wrapper commands because they are always available after installation. When
-your client exposes the matching MCP tools, use them with the same saved-file, version, update, sync,
+your client exposes the matching MCP tools, use them with the same saved-file, snapshot, update, sync,
 and isolation rules; do not treat MCP as a raw Lean LSP proxy.
 
 Supported command families:
@@ -113,7 +113,7 @@ Core workflow contract:
 - MCP owns its stdio runtime session automatically; do not start a separate wrapper holder solely
   for MCP tool calls
 - after every real Lean source edit: save the file normally, then run `lean-beam update` before the
-  next version-bound probe; run `lean-beam sync` when you need diagnostics/readiness
+  next snapshot-bound probe; run `lean-beam sync` when you need diagnostics/readiness
 - use `lean-beam save` only for a synced workspace module path in the current Lake workspace package
   graph, for example `MyPkg/Sub/Module.lean`
 - `lean-beam save` checks readiness and checkpoints only the module snapshot you save; it does not
@@ -153,7 +153,7 @@ A standalone scratch file has a high fixed cost: it starts from a detached modul
 and environment, and encourages simplified contexts that may not match the real source position.
 
 A `lean-beam run-at` probe has low marginal cost once the per-project daemon and module context are
-warm: it asks one speculative question against an explicit broker document version and the real
+warm: it asks one speculative question against an explicit broker document snapshot and the real
 module environment.
 
 This changes the right agent behavior:
@@ -194,11 +194,11 @@ Prefer the smallest command that matches the actual task:
 - before `lean-beam run-at`, `lean-beam run-at-handle`, `lean-beam hover`,
   `lean-beam signature-help`, `lean-beam definition`, `lean-beam references`,
   `lean-beam document-symbols`, `lean-beam goals`, or `lean-beam todo`, call
-  `lean-beam update <file>` and pass the returned `version`; `lean-beam workspace-symbols` takes
+  `lean-beam update <file>` and pass the returned `snapshot`; `lean-beam workspace-symbols` takes
   only a query
-- if a versioned request fails with `contentModified` and
-  `error.data.reason = "documentVersionMismatch"`, use `error.data.acceptedVersion` for the next
-  retry or run `lean-beam update` / `lean-beam sync` again; do not guess a version
+- if a request fails with `contentModified`, read the current source and resolve the intended
+  position, range, or code action again, then obtain a fresh `snapshot` from `lean-beam update`
+  or `lean-beam sync` before retrying; changing only the token does not repair stale coordinates
 - for `lean-beam run-at`, `lean-beam hover`, `lean-beam signature-help`,
   `lean-beam definition`, `lean-beam references`, `lean-beam goals`, and `lean-beam todo`, treat
   line and character arguments as Lean/LSP coordinates: line `0` is the first line, character `0`
@@ -238,7 +238,7 @@ batch-equivalence check rather than one-file probing.
 
 ## Lean-Run-At Semantics
 
-`lean-beam run-at` is a speculative execution request against one explicit broker document version.
+`lean-beam run-at` is a speculative execution request against one explicit broker document snapshot.
 Read it as "try this Lean text here", not as "edit the file here".
 
 What `lean-beam run-at` does not do:
@@ -350,7 +350,7 @@ Default rules:
 - start and keep one `lean-beam serve` owner before issuing wrapper workflow commands
 - start with `lean-beam run-at`
 - after every real source edit: save the file to disk normally, then `lean-beam update` before the
-  next version-bound probe; use `lean-beam sync` for diagnostics/readiness
+  next snapshot-bound probe; use `lean-beam sync` for diagnostics/readiness
 - if exact continuation matters: mint a handle
 - if search branches: use `lean-beam run-with`, `lean-beam run-with-linear`, and `lean-beam release`
 - if you want shorter shell commands for search loops: use `lean-beam-search`
@@ -367,21 +367,21 @@ lean-beam serve
 # terminal or agent process 2: inspect existing code or proof state
 update_out="$(lean-beam update "Foo.lean")"
 printf '%s\n' "$update_out"
-version="$(printf '%s\n' "$update_out" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["version"])')"
-lean-beam hover "Foo.lean" "$version" 10 2
-lean-beam signature-help "Foo.lean" "$version" 10 2
-lean-beam definition "Foo.lean" "$version" 10 2
-lean-beam references "Foo.lean" "$version" 10 2
-lean-beam document-symbols "Foo.lean" "$version"
+snapshot="$(printf '%s\n' "$update_out" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+lean-beam hover "Foo.lean" "$snapshot" 10 2
+lean-beam signature-help "Foo.lean" "$snapshot" 10 2
+lean-beam definition "Foo.lean" "$snapshot" 10 2
+lean-beam references "Foo.lean" "$snapshot" 10 2
+lean-beam document-symbols "Foo.lean" "$snapshot"
 lean-beam workspace-symbols "Foo.bar"
-lean-beam goals before "Foo.lean" "$version" 10 2
+lean-beam goals before "Foo.lean" "$snapshot" 10 2
 
 # try speculative Lean text without editing the file
-lean-beam run-at "Foo.lean" "$version" 10 2 "exact trivial"
+lean-beam run-at "Foo.lean" "$snapshot" 10 2 "exact trivial"
 # for multiline probes, prefer stdin
-printf 'example : True := by\n  trivial\n' | lean-beam run-at "Foo.lean" "$version" 10 2 --stdin
+printf 'example : True := by\n  trivial\n' | lean-beam run-at "Foo.lean" "$snapshot" 10 2 --stdin
 
-# after every real edit saved to disk, use update for the next probe version
+# after every real edit saved to disk, use update for the next probe snapshot
 lean-beam update "MyPkg/Sub/Module.lean"
 
 # when you need diagnostics/readiness, on that same workspace module path
@@ -495,7 +495,7 @@ Open these only when the task needs the detail:
 
 - prefer `lean-beam run-at` before editing when feasible
 - treat `lean-beam update` as mandatory after every real Lean file edit before the next speculative probe
-- do not assume one successful probe changes the basis of the next one; each probe starts from the explicit document version it names
+- do not assume one successful probe changes the basis of the next one; each probe starts from the explicit document snapshot it names
 - when continuation really matters, prefer an explicit stored handle over hoping the next probe will
   recover the same internal basis by accident
 - prefer `lean-beam save` / `lean-beam close-save` over a full `lake build` when only one file needs checkpointing
diff --git a/skills/lean-beam/references/anti-patterns.md b/skills/lean-beam/references/anti-patterns.md
index bdd22dce..5e7050f5 100644
--- a/skills/lean-beam/references/anti-patterns.md
+++ b/skills/lean-beam/references/anti-patterns.md
@@ -23,7 +23,7 @@ Use this reference as a short checklist of what not to assume in Lean `beam` wor
 - use `lean-beam definition`, `lean-beam references`, `lean-beam document-symbols`, and
   `lean-beam workspace-symbols` for semantic navigation
 - use `lean-beam goals before` / `lean-beam goals after` for existing proof state
-- use `lean-beam run-at` for one speculative snippet on an explicit broker document version
+- use `lean-beam run-at` for one speculative snippet on an explicit broker document snapshot
 - probe at the real source position with `lean-beam run-at`
 - pass multiline speculative text with `--stdin` instead of writing a temporary Lean file
 - use `lean-beam run-at-handle` plus `lean-beam run-with` / `lean-beam run-with-linear` for exact speculative chaining
diff --git a/skills/lean-beam/references/commit-speculative.md b/skills/lean-beam/references/commit-speculative.md
index f59caa4a..b5a790e6 100644
--- a/skills/lean-beam/references/commit-speculative.md
+++ b/skills/lean-beam/references/commit-speculative.md
@@ -15,8 +15,16 @@ That is the current explicit handoff from speculative execution to saved file st
 
 ## Minimal Pattern
 
+Read `Foo.lean` and select the intended position. Stop if `update` fails; after it succeeds,
+extract its token for the probes below:
+
+```bash
+update_json="$(lean-beam update "Foo.lean")"
+snapshot="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+```
+
 ```bash
-lean-beam run-at "Foo.lean" <version-from-update> 20 2 "exact h"
+lean-beam run-at "Foo.lean" "$snapshot" 20 2 "exact h"
 
 # if the speculative result is the change you want:
 # 1. edit Foo.lean for real
@@ -36,7 +44,7 @@ Sometimes the task is:
 Use the handle path first:
 
 ```bash
-root="$(lean-beam run-at-handle "Foo.lean" <version-from-update> 20 2 "tac1")"
+root="$(lean-beam run-at-handle "Foo.lean" "$snapshot" 20 2 "tac1")"
 next="$(printf '%s\n' "$root" | lean-beam run-with-linear "Foo.lean" - "tac2")"
 ```
 
diff --git a/skills/lean-beam/references/lean-run-at-semantics.md b/skills/lean-beam/references/lean-run-at-semantics.md
index b5b8713f..7219fac4 100644
--- a/skills/lean-beam/references/lean-run-at-semantics.md
+++ b/skills/lean-beam/references/lean-run-at-semantics.md
@@ -1,10 +1,18 @@
 # Lean Run-At Semantics
 
 Use this reference when a task is confused about what `lean-beam run-at` means. The short rule is:
-`lean-beam run-at` is a speculative execution probe against one explicit broker document version, not a source edit.
+`lean-beam run-at` is a speculative execution probe against one explicit broker document snapshot, not a source edit.
 
 For coordinates and tactic-state selection, see [Position Semantics](workflow-details.md#position-semantics).
 
+Read `Foo.lean` and resolve the intended position before obtaining its token. Stop if `update` fails.
+The examples below use this `snapshot` variable:
+
+```bash
+update_json="$(lean-beam update "Foo.lean")"
+snapshot="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+```
+
 ## What It Is Not
 
 - it is not an edit to the file on disk
@@ -19,7 +27,7 @@ For coordinates and tactic-state selection, see [Position Semantics](workflow-de
 Wrong expectation:
 
 ```bash
-lean-beam run-at "Foo.lean" <version-from-update> 20 2 "exact h"
+lean-beam run-at "Foo.lean" "$snapshot" 20 2 "exact h"
 # then expect diagnostics for unrelated later declarations as if Foo.lean had been edited
 ```
 
@@ -30,7 +38,7 @@ Correct workflow:
 lean-beam sync "Foo.lean"
 ```
 
-Use `lean-beam sync` when you need diagnostics for the saved file version as a whole. `lean-beam run-at`
+Use `lean-beam sync` when you need diagnostics for the saved file snapshot as a whole. `lean-beam run-at`
 only waits for the snapshot needed by that speculative request.
 
 It should still report errors produced by the speculative text itself. For example, a top-level
@@ -45,15 +53,15 @@ If the speculative probe looks right and you want to keep it, open
 Wrong expectation:
 
 ```bash
-lean-beam run-at "Foo.lean" <version-from-update> 30 2 "tac1"
-lean-beam run-at "Foo.lean" <version-from-update> 30 2 "tac2"
+lean-beam run-at "Foo.lean" "$snapshot" 30 2 "tac1"
+lean-beam run-at "Foo.lean" "$snapshot" 30 2 "tac2"
 # then expect the second call to continue from the speculative `tac1`
 ```
 
 Correct workflow:
 
 ```bash
-root="$(lean-beam run-at-handle "Foo.lean" <version-from-update> 30 2 "tac1")"
+root="$(lean-beam run-at-handle "Foo.lean" "$snapshot" 30 2 "tac1")"
 printf '%s\n' "$root" | lean-beam run-with-linear "Foo.lean" - "tac2"
 ```
 
@@ -71,13 +79,13 @@ If a speculative step looks right and you want it to become real source, open
 Wrong expectation:
 
 ```bash
-printf 'def tmpA : Nat := 1\n\n#check tmpA\n' | lean-beam run-at "Foo.lean" <version-from-update> 30 0 --stdin
+printf 'def tmpA : Nat := 1\n\n#check tmpA\n' | lean-beam run-at "Foo.lean" "$snapshot" 30 0 --stdin
 ```
 
 Correct workflows:
 
 ```bash
-root="$(lean-beam run-at-handle "Foo.lean" <version-from-update> 30 0 "def tmpA : Nat := 1")"
+root="$(lean-beam run-at-handle "Foo.lean" "$snapshot" 30 0 "def tmpA : Nat := 1")"
 printf '%s\n' "$root" | lean-beam run-with "Foo.lean" - "#check tmpA"
 ```
 
@@ -96,7 +104,7 @@ the second command.
 Wrong expectation:
 
 ```bash
-lean-beam run-at "Foo.lean" <version-from-update> 18 0 "exact h"
+lean-beam run-at "Foo.lean" "$snapshot" 18 0 "exact h"
 # where line 18 is a blank line inside an indented block, and expect the wrapper to infer indentation
 #
 # or expect the wrapper to add a leading/trailing newline around the text automatically
@@ -106,10 +114,10 @@ Correct workflow:
 
 ```bash
 # on a truly empty line, only column 0 is valid, so provide the indentation in the text yourself
-lean-beam run-at "Foo.lean" <version-from-update> 18 0 "    exact h"
+lean-beam run-at "Foo.lean" "$snapshot" 18 0 "    exact h"
 
 # or probe after the existing indentation and pass only the code text
-lean-beam run-at "Foo.lean" <version-from-update> 18 4 "exact h"
+lean-beam run-at "Foo.lean" "$snapshot" 18 4 "exact h"
 ```
 
 Or make the real edit in the file and save it before syncing:
@@ -131,13 +139,13 @@ For multi-line probes, include the actual newline characters you want Lean to pa
 
 ```bash
 # piping the exact text through stdin avoids shell-escape mistakes
-printf '  first | exact h1\n  | exact h2\n' | lean-beam run-at "Foo.lean" <version-from-update> 18 0 --stdin
+printf '  first | exact h1\n  | exact h2\n' | lean-beam run-at "Foo.lean" "$snapshot" 18 0 --stdin
 
 # or read the probe from a file
-lean-beam run-at "Foo.lean" <version-from-update> 18 0 --text-file probe.lean
+lean-beam run-at "Foo.lean" "$snapshot" 18 0 --text-file probe.lean
 
 # ANSI-C shell quoting also works when you do want to keep everything on one command line
-lean-beam run-at "Foo.lean" <version-from-update> 18 0 $'  first | exact h1\n  | exact h2'
+lean-beam run-at "Foo.lean" "$snapshot" 18 0 $'  first | exact h1\n  | exact h2'
 ```
 
 Do not expect the wrapper to turn `"first | exact h1 | exact h2"` into a properly line-broken block,
diff --git a/skills/lean-beam/references/mcts-search.md b/skills/lean-beam/references/mcts-search.md
index 94969826..e3065e4a 100644
--- a/skills/lean-beam/references/mcts-search.md
+++ b/skills/lean-beam/references/mcts-search.md
@@ -4,12 +4,20 @@ Use this reference when the task is no longer “try one tactic at one position
 “preserve a speculative proof state, branch from it, run linear playouts, and release side
 branches.”
 
+Read `Proofs.lean` and resolve the intended position before obtaining its token. Stop if `update` fails.
+The examples below use this `snapshot` variable:
+
+```bash
+update_json="$(lean-beam update "Proofs.lean")"
+snapshot="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+```
+
 ## Core pattern
 
 Use these commands:
 
 ```bash
-lean-beam run-at-handle "Proofs.lean" <version-from-update> 42 6 "constructor"
+lean-beam run-at-handle "Proofs.lean" "$snapshot" 42 6 "constructor"
 printf '%s\n' "$HANDLE_JSON" | lean-beam run-with "Proofs.lean" - "constructor"
 printf '%s\n' "$HANDLE_JSON" | lean-beam run-with-linear "Proofs.lean" - "exact trivial"
 printf '%s\n' "$HANDLE_JSON" | lean-beam release "Proofs.lean" -
@@ -18,7 +26,7 @@ printf '%s\n' "$HANDLE_JSON" | lean-beam release "Proofs.lean" -
 Or use the shorter helper:
 
 ```bash
-lean-beam-search mint "Proofs.lean" <version-from-update> 42 6 "constructor"
+lean-beam-search mint "Proofs.lean" "$snapshot" 42 6 "constructor"
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search branch "Proofs.lean" "constructor"
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search linear "Proofs.lean" "exact trivial"
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search playout "Proofs.lean" "exact trivial" "exact trivial"
@@ -27,7 +35,7 @@ printf '%s\n' "$HANDLE_JSON" | lean-beam-search release "Proofs.lean"
 
 Rules:
 
-- `lean-beam run-at-handle` mints a preserved root handle from the explicit broker document version
+- `lean-beam run-at-handle` mints a preserved root handle from the explicit broker document snapshot
 - `lean-beam run-with` is non-linear: it preserves the current handle and returns a successor handle
 - `lean-beam run-with-linear` is linear: it consumes the current handle and returns a successor handle
 - `lean-beam release` explicitly drops a preserved handle you no longer need
@@ -37,7 +45,7 @@ Rules:
 
 ```bash
 # with `lean-beam serve` running in another process
-root="$(lean-beam run-at-handle "Proofs.lean" <version-from-update> 42 6 "constructor")"
+root="$(lean-beam run-at-handle "Proofs.lean" "$snapshot" 42 6 "constructor")"
 
 # writing handles to files avoids stdin conflicts in larger shell scripts
 printf '%s\n' "$root" > root.handle.json
@@ -58,7 +66,7 @@ Use this when you want to explore multiple children from the same preserved basi
 
 ```bash
 # with `lean-beam serve` running in another process
-root="$(lean-beam run-at-handle "Proofs.lean" <version-from-update> 42 6 "constructor")"
+root="$(lean-beam run-at-handle "Proofs.lean" "$snapshot" 42 6 "constructor")"
 # file-backed handles are often easier in longer shell loops
 printf '%s\n' "$root" > root.handle.json
 step1="$(lean-beam run-with-linear "Proofs.lean" --handle-file root.handle.json "constructor")"
@@ -88,7 +96,7 @@ Concrete shell sketch:
 
 ```bash
 # with `lean-beam serve` running in another process
-root="$(lean-beam run-at-handle "Proofs.lean" <version-from-update> 42 6 "constructor")"
+root="$(lean-beam run-at-handle "Proofs.lean" "$snapshot" 42 6 "constructor")"
 
 child_a="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "constructor")"
 child_b="$(printf '%s\n' "$root" | lean-beam run-with "Proofs.lean" - "aesop")"
@@ -103,7 +111,7 @@ The same sketch with the helper:
 
 ```bash
 # with `lean-beam serve` running in another process
-root="$(lean-beam-search mint "Proofs.lean" <version-from-update> 42 6 "constructor")"
+root="$(lean-beam-search mint "Proofs.lean" "$snapshot" 42 6 "constructor")"
 child_a="$(printf '%s\n' "$root" | lean-beam-search branch "Proofs.lean" "constructor")"
 child_b="$(printf '%s\n' "$root" | lean-beam-search branch "Proofs.lean" "aesop")"
 playout_a="$(printf '%s\n' "$child_a" | lean-beam-search playout "Proofs.lean" "exact trivial" "exact trivial")"
@@ -130,7 +138,7 @@ Do not try to salvage old handles.
 ```bash
 # make a real edit and save the source file to disk
 lean-beam update "Proofs.lean"
-root="$(lean-beam run-at-handle "Proofs.lean" <version-from-update> 42 6 "constructor")"
+root="$(lean-beam run-at-handle "Proofs.lean" "$snapshot" 42 6 "constructor")"
 ```
 
 ## When to stop using search
diff --git a/skills/lean-beam/references/workflow-details.md b/skills/lean-beam/references/workflow-details.md
index 174c2a96..6c8aee06 100644
--- a/skills/lean-beam/references/workflow-details.md
+++ b/skills/lean-beam/references/workflow-details.md
@@ -4,8 +4,8 @@ Use this reference when the task needs more than the default loop in `SKILL.md`.
 
 ## Position Semantics
 
-- `lean-beam run-at` and `lean-beam run-at-handle` take the broker document version before
-  Lean/LSP `Position` coordinates: `<version> <line> <character>`; use the version from `update`
+- `lean-beam run-at` and `lean-beam run-at-handle` take the broker document snapshot before
+  Lean/LSP `Position` coordinates: `<snapshot> <line> <character>`; use the snapshot from `update`
 - line `0` is the first line, and character `0` is the first UTF-16 code unit on that line
 - on a truly empty line, only character `0` is valid; character `1` is already out of range
 - on an indented blank line, either probe after the existing spaces using that exact character
@@ -37,10 +37,13 @@ example (a b : Nat) (h : a = b) : 0 + a = b := by
 | `1 3`: inside `simp` | After `simp`: `a = b` | Succeeds |
 | `2 2`: start of `exact h` | Before `exact h`: `a = b` | Succeeds |
 
-After updating the file, this replacement probe correctly returns `result.success=false`:
+Read the source and select the intended position first. Stop if `update` fails; after it succeeds,
+extract its token. This replacement probe correctly returns `result.success=false`:
 
 ```bash
-lean-beam run-at "BeamRunAtProbe.lean" <version-from-update> 1 2 -- "exact h"
+update_json="$(lean-beam update "BeamRunAtProbe.lean")"
+snapshot="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+lean-beam run-at "BeamRunAtProbe.lean" "$snapshot" 1 2 -- "exact h"
 ```
 
 Nested tactics and whitespace may select an enclosing or neighboring tactic. `goals before` and
@@ -48,6 +51,14 @@ Nested tactics and whitespace may select an enclosing or neighboring tactic. `go
 
 ## Command Details
 
+The following position examples use `Foo.lean`; obtain its token separately after reading that file.
+Stop if `update` fails.
+
+```bash
+update_json="$(lean-beam update "Foo.lean")"
+snapshot="$(printf '%s\n' "$update_json" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+```
+
 Continue from a stored handle:
 
 ```bash
@@ -65,7 +76,7 @@ printf '%s\n' "$HANDLE_JSON" | lean-beam release "Foo.lean" -
 Short search helper:
 
 ```bash
-lean-beam-search mint "Foo.lean" <version-from-update> 10 2 "constructor"
+lean-beam-search mint "Foo.lean" "$snapshot" 10 2 "constructor"
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search branch "Foo.lean" "constructor"
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search playout "Foo.lean" "exact trivial" "exact trivial"
 printf '%s\n' "$HANDLE_JSON" | lean-beam-search release "Foo.lean"
@@ -74,24 +85,24 @@ printf '%s\n' "$HANDLE_JSON" | lean-beam-search release "Foo.lean"
 Inspect Lean type/term information at a specific position:
 
 ```bash
-lean-beam hover "Foo.lean" <version-from-update> 10 2
-lean-beam signature-help "Foo.lean" <version-from-update> 10 2
+lean-beam hover "Foo.lean" "$snapshot" 10 2
+lean-beam signature-help "Foo.lean" "$snapshot" 10 2
 ```
 
 Follow semantic navigation and symbol information:
 
 ```bash
-lean-beam definition "Foo.lean" <version-from-update> 10 2
-lean-beam references "Foo.lean" <version-from-update> 10 2
-lean-beam document-symbols "Foo.lean" <version-from-update>
+lean-beam definition "Foo.lean" "$snapshot" 10 2
+lean-beam references "Foo.lean" "$snapshot" 10 2
+lean-beam document-symbols "Foo.lean" "$snapshot"
 lean-beam workspace-symbols "Foo.bar"
 ```
 
 Inspect Lean proof goals at an existing tactic position:
 
 ```bash
-lean-beam goals before "Foo.lean" <version-from-update> 10 2
-lean-beam goals after "Foo.lean" <version-from-update> 10 2
+lean-beam goals before "Foo.lean" "$snapshot" 10 2
+lean-beam goals after "Foo.lean" "$snapshot" 10 2
 ```
 
 These commands return structured goals in `result.goals`. A solved state uses
@@ -143,8 +154,8 @@ What is not a valid checkpoint target:
 - `lean-beam hover` and `lean-beam signature-help` are normal read-only semantic inspection
   commands for an existing position
 - `lean-beam definition`, `lean-beam references`, and `lean-beam document-symbols` are normal
-  read-only semantic navigation commands against a specific document version
-- `lean-beam workspace-symbols` is a read-only workspace query and does not take a document version
+  read-only semantic navigation commands against a specific document snapshot
+- `lean-beam workspace-symbols` is a read-only workspace query and does not take a document snapshot
 - `lean-beam goals before` and `lean-beam goals after` are the normal read-only proof-state
   inspection commands for an existing tactic position
 - `lean-beam goals before` / `lean-beam goals after` return `result.goals`, not speculative execution output,
@@ -152,7 +163,7 @@ What is not a valid checkpoint target:
 - `lean-beam` only sees the on-disk file, not unsaved editor buffers
 - actual source edits happen through the normal file-edit workflow
 - after every real source edit to a Lean file, save the file in the normal editor/file sense and
-  then run `lean-beam update "Foo.lean"` before the next version-bound probe; use
+  then run `lean-beam update "Foo.lean"` before the next snapshot-bound probe; use
   `lean-beam sync "Foo.lean"` when the workflow needs a diagnostics/readiness barrier
 - use `lean-beam refresh "Foo.lean"` when a tracked file needs `lean-beam close` plus `lean-beam sync`
   as one step, especially after saving an upstream dependency
@@ -167,7 +178,7 @@ What is not a valid checkpoint target:
   interactive progress text goes to stderr, while selector, setup, or transport failures may exit
   nonzero with no JSON
 - every `lean-beam run-at` request is an isolated read-only probe against one on-disk document
-  version
+  snapshot
 - `lean-beam run-at-handle` is the same style of isolated probe, but asks Lean to retain follow-up
   state
 - `lean-beam run-with` preserves the current handle and branches from it
@@ -185,9 +196,9 @@ What is not a valid checkpoint target:
   `lean-beam run-at` only waits for the snapshot it needs
 - if the same document changes while a request or stored handle is pending, expect
   `contentModified` or handle invalidation instead of hidden reuse
-- when `contentModified` includes `error.data.reason = "documentVersionMismatch"`,
-  `error.data.acceptedVersion` names the broker-accepted version to retry with, and
-  `error.data.currentVersion` may echo the current tracked document version
+- after `contentModified`, read the source and resolve the intended target or code action again;
+  call `update` or `sync` for a fresh `snapshot` before retrying. `currentSnapshot` identifies
+  the observed replacement; it does not rebase old coordinates or actions
 - `lean-beam save` / `lean-beam close-save` checkpoint the current synced Lake module only; they do not
   rebuild reverse dependencies or make downstream files fresh by themselves
 
@@ -236,9 +247,9 @@ Treat `fileProgress` as observability, not as proof that every call is a full ba
 # with `lean-beam serve` running in another process
 sync_out="$(lean-beam sync "Foo.lean")"
 printf '%s\n' "$sync_out"
-version="$(printf '%s\n' "$sync_out" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["version"])')"
+snapshot="$(printf '%s\n' "$sync_out" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
 
-probe_out="$(lean-beam run-at "Foo.lean" "$version" 10 2 "exact trivial")"
+probe_out="$(lean-beam run-at "Foo.lean" "$snapshot" 10 2 "exact trivial")"
 printf '%s\n' "$probe_out"
 ```
 
@@ -335,8 +346,8 @@ itself to prove the dependency cone is fresh.
 # make a real edit in A.lean and save the source file to disk
 lean-beam sync "A.lean"
 b_update="$(lean-beam update "B.lean")"
-b_version="$(printf '%s\n' "$b_update" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["version"])')"
-lean-beam run-at "B.lean" "$b_version" 12 2 "#check someNameFromA"
+b_snapshot="$(printf '%s\n' "$b_update" | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["snapshot"])')"
+lean-beam run-at "B.lean" "$b_snapshot" 12 2 "#check someNameFromA"
 ```
 
 Rules:
@@ -379,9 +390,9 @@ lean-beam stats
 
 `lean-beam open-files` shows the files currently tracked by the Beam daemon for the current project,
 along with on-disk `diskStatus`, the daemon-recorded `checkpointed` marker, and the last compact
-`fileProgress` observed for that tracked version. `diskStatus` is `matchesTracked`,
+`fileProgress` observed for that tracked snapshot. `diskStatus` is `matchesTracked`,
 `differsFromTracked`, `missing`, or `unknown`. `checkpointed` means this daemon successfully saved
-the unchanged tracked version; it does not revalidate Lake artifacts. Run `lean-beam save` to
+the unchanged tracked snapshot; it does not revalidate Lake artifacts. Run `lean-beam save` to
 perform the authoritative Lake module, readiness, trace, and setup checks.
 
 Stats are in-memory only and scoped to the current project Beam daemon.
diff --git a/skills/rocq-beam/SKILL.md b/skills/rocq-beam/SKILL.md
index 7896e5da..55992a6e 100644
--- a/skills/rocq-beam/SKILL.md
+++ b/skills/rocq-beam/SKILL.md
@@ -223,7 +223,7 @@ lean-beam stats
 `lean-beam open-files` shows the files currently tracked by the Beam daemon for the current project. For
 tracked files the broker already knows about, the wrapper checks status incrementally against the
 current on-disk text, and `open-files` also reports the last compact `fileProgress` observed for
-that tracked version.
+that tracked snapshot.
 
 Stats are in-memory only and scoped to the current project Beam daemon.
 
diff --git a/tests/lean/BeamTest/Broker/CliDaemonTest.lean b/tests/lean/BeamTest/Broker/CliDaemonTest.lean
index a3078e56..7ff951ad 100644
--- a/tests/lean/BeamTest/Broker/CliDaemonTest.lean
+++ b/tests/lean/BeamTest/Broker/CliDaemonTest.lean
@@ -334,7 +334,7 @@ private def checkBrokerSendInterruption : IO Unit := do
       Beam.Broker.sendRequestWithCallbacksInterruptiblyResult endpoint {
         payload := .runAt {
           path := "Secret.lean"
-          version := 1
+          snapshot := ⟨"test-session", 1⟩
           line := 0
           character := 0
           text := largeText
@@ -389,7 +389,7 @@ private def checkWrongGreetingProtectsRequest : IO Unit := do
         (projectDaemonClientForTest endpoint (System.FilePath.mk "/tmp")) {
           payload := .runAt {
             path := "Secret.lean"
-            version := 1
+            snapshot := ⟨"test-session", 1⟩
             line := 0
             character := 0
             text := "secret speculative text"
@@ -584,15 +584,15 @@ private def checkSyncWaitSpecs : IO Unit := do
   let okResp :=
     (Beam.Broker.Response.success <| toJson ({
       path := "Demo.lean"
-      version := 5
+      snapshot := ⟨"test-session", 5⟩
       : Beam.Broker.SyncFileResult
     })).withFileProgress { updates := 2, done := true }
-  require "sync complete message should include version and progress"
+  require "sync complete message should include snapshot and progress"
     ((Beam.Cli.syncWaitSpec "Demo.lean").completeMsg okResp ==
-      "beam: sync complete for Demo.lean (version 5, fp updates=2)")
+      "beam: sync complete for Demo.lean (snapshot test-session/5, fp updates=2)")
   require "refresh complete message should share sync-like formatting"
     ((Beam.Cli.refreshWaitSpec "Demo.lean").completeMsg okResp ==
-      "beam: refresh complete for Demo.lean (version 5, fp updates=2)")
+      "beam: refresh complete for Demo.lean (snapshot test-session/5, fp updates=2)")
   let publicTodoSpec := Beam.Cli.leanTodoWaitSpec "Demo.lean" 1 0 2 3 "todo"
   require "todo wait action should accept public wrapper label"
     (publicTodoSpec.action == "todo")
@@ -629,7 +629,7 @@ private def checkSyncWaitSpecs : IO Unit := do
 
   let notReadyResp := Beam.Broker.Response.success <| toJson ({
       path := "Demo.lean"
-      version := 6
+      snapshot := ⟨"test-session", 6⟩
       readiness := {
         blockingErrorCount := 1
         saveReady := false
@@ -713,52 +713,53 @@ private def checkLeanOperationRequests : IO Unit := do
 
   let runAtInput : Beam.Lean.RunAtInput := {
     path
-    version := 12
+    snapshot := ⟨"test-session", 12⟩
     line := 4
     character := 2
     text := "exact h"
   }
   requireRequestJson "runAt request should share the Lean operation adapter"
-    (Beam.Cli.leanRunAtRequest path 12 4 2 "exact h")
+    (Beam.Cli.leanRunAtRequest runAtInput.toPositionInput "exact h")
     runAtInput.toBrokerRequest
   requireRequestJson "runAt handle request should share the Lean operation adapter"
-    (Beam.Cli.leanRunAtRequest path 12 4 2 "exact h" (storeHandle := true))
+    (Beam.Cli.leanRunAtRequest runAtInput.toPositionInput "exact h" (storeHandle := true))
     (runAtInput.toBrokerRequest (storeHandle := true))
   expectIoErrorContains "runAt missing text should fail at the CLI boundary"
-    "usage: lean-beam" (Beam.Cli.parseTextArg "run-at Demo.lean 12 4 2" [])
-
-  let positionInput : Beam.Lean.PositionInput := {
-    path
-    version := 13
-    line := 7
-    character := 3
-  }
+    "usage: lean-beam" (Beam.Cli.parseTextArg "run-at Demo.lean test-session/12 4 2" [])
+
+  let positionInput ← Beam.Cli.parseLeanPositionArgs path "test-session/13" "7" "3"
+  require "position parsing keeps the source token and coordinates"
+    (positionInput.snapshot == ⟨"test-session", 13⟩ && positionInput.line == 7 && positionInput.character == 3)
+  expectIoErrorContains "position parsing rejects a numeric token" "opaque token"
+    (Beam.Cli.parseLeanPositionArgs path "13" "7" "3")
+  expectIoErrorContains "position parsing rejects invalid coordinates" "invalid line"
+    (Beam.Cli.parseLeanPositionArgs path "test-session/13" "bad" "3")
   requireRequestJson "hover request should share the Lean operation adapter"
-    (Beam.Cli.leanHoverRequest path 13 7 3)
+    (Beam.Cli.leanHoverRequest positionInput)
     positionInput.toHoverBrokerRequest
   requireRequestJson "signature-help request should share the Lean operation adapter"
-    (Beam.Cli.leanSignatureHelpRequest path 13 7 3)
+    (Beam.Cli.leanSignatureHelpRequest positionInput)
     positionInput.toSignatureHelpBrokerRequest
   requireRequestJson "definition request should share the Lean operation adapter"
-    (Beam.Cli.leanDefinitionRequest path 13 7 3)
+    (Beam.Cli.leanDefinitionRequest positionInput)
     positionInput.toDefinitionBrokerRequest
   let referencesInput : Beam.Lean.ReferencesInput := {
     path
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
     line := 7
     character := 3
     includeDeclaration? := some false
   }
   requireRequestJson "references request should share the Lean operation adapter"
-    (Beam.Cli.leanReferencesRequest path 13 7 3 false)
+    (Beam.Cli.leanReferencesRequest positionInput false)
     referencesInput.toBrokerRequest
-  let documentSymbolsInput : Beam.Lean.DocumentSymbolsInput := {
+  let documentSymbolsInput : Beam.Lean.DocumentInput := {
     path
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
   }
   requireRequestJson "document-symbols request should share the Lean operation adapter"
-    (Beam.Cli.leanDocumentSymbolsRequest path 13)
-    documentSymbolsInput.toBrokerRequest
+    (Beam.Cli.leanDocumentSymbolsRequest documentSymbolsInput)
+    documentSymbolsInput.toDocumentSymbolsBrokerRequest
   let workspaceSymbolsInput : Beam.Lean.WorkspaceSymbolsInput := {
     query := "Demo"
   }
@@ -766,7 +767,7 @@ private def checkLeanOperationRequests : IO Unit := do
     (Beam.Cli.leanWorkspaceSymbolsRequest "Demo")
     workspaceSymbolsInput.toBrokerRequest
   requireRequestJson "goals request should share the Lean operation adapter"
-    (Beam.Cli.leanGoalsRequest path 13 7 3 .before)
+    (Beam.Cli.leanGoalsRequest positionInput .before)
     (positionInput.toGoalsBrokerRequest .before)
 
   let runWithInput : Beam.Lean.RunWithInput := {
diff --git a/tests/lean/BeamTest/Broker/DocumentStateTest.lean b/tests/lean/BeamTest/Broker/DocumentStateTest.lean
index 6cb9e33a..5f486dcf 100644
--- a/tests/lean/BeamTest/Broker/DocumentStateTest.lean
+++ b/tests/lean/BeamTest/Broker/DocumentStateTest.lean
@@ -54,9 +54,9 @@ private def mkSnapshot
 private def checkSyncFileDecisionOpen : IO Unit := do
   let uri := "file:///workspace/Foo.lean"
   let decision := DocumentState.syncFileDecision {} uri
-    (mkSnapshot 10)
+    (mkSnapshot 10) 17
   require "syncFileDecision opens unknown doc" (decision.action == .open)
-  require "syncFileDecision open starts at version 1" (decision.version == 1)
+  require "open consumes the session allocator" (decision.version == 17 && decision.nextVersion == 18)
   let some doc := decision.docs.get? uri
     | throw <| IO.userError "syncFileDecision open did not insert doc"
   require "syncFileDecision open records hash" (doc.textHash == 10)
@@ -72,7 +72,8 @@ private def checkSyncFileDecisionUnchanged : IO Unit := do
       fileProgress? := some { updates := 2, done := true }
       lastSyncEventSeq := 8
     }
-  let decision := DocumentState.syncFileDecision docs uri (mkSnapshot 10 (some "Foo"))
+  let decision := DocumentState.syncFileDecision docs uri (mkSnapshot 10 (some "Foo")) 11
+  require "unchanged preserves the allocator" (decision.nextVersion == 11)
   require "syncFileDecision unchanged has no LSP action" (decision.action == .unchanged)
   require "syncFileDecision unchanged preserves version" (decision.version == 5)
   let some doc := decision.docs.get? uri
@@ -93,9 +94,9 @@ private def checkSyncFileDecisionChange : IO Unit := do
       fileProgress? := some { updates := 2, done := true }
       lastSyncEventSeq := 8
     }
-  let decision := DocumentState.syncFileDecision docs uri (mkSnapshot 11 (some "Foo"))
+  let decision := DocumentState.syncFileDecision docs uri (mkSnapshot 11 (some "Foo")) 11
   require "syncFileDecision changed emits change action" (decision.action == .change)
-  require "syncFileDecision changed bumps version" (decision.version == 6)
+  require "change consumes the session allocator" (decision.version == 11 && decision.nextVersion == 12)
   let some doc := decision.docs.get? uri
     | throw <| IO.userError "syncFileDecision changed erased doc"
   require "syncFileDecision changed records hash" (doc.textHash == 11)
@@ -104,6 +105,31 @@ private def checkSyncFileDecisionChange : IO Unit := do
   require "syncFileDecision changed clears progress" (doc.fileProgress?.isNone)
   require "syncFileDecision changed preserves sync event seq" (doc.lastSyncEventSeq == 8)
 
+private def checkInterleavedDocumentRevisions : IO Unit := do
+  let a := "file:///workspace/A.lean"
+  let b := "file:///workspace/B.lean"
+  let openedA := DocumentState.syncFileDecision {} a { mkSnapshot 10 with readSeq := 1 } 1
+  let openedB := DocumentState.syncFileDecision openedA.docs b
+    { mkSnapshot 10 with readSeq := 2 } openedA.nextVersion
+  let changedA := DocumentState.syncFileDecision openedB.docs a
+    { mkSnapshot 20 with readSeq := 3 } openedB.nextVersion
+  require "files share one revision allocator"
+    ([openedA.version, openedB.version, changedA.version] == [1, 2, 3])
+  let superseded := DocumentState.syncFileDecision changedA.docs a
+    { mkSnapshot 10 with readSeq := 1 } changedA.nextVersion
+  require "an older read neither rolls back source nor consumes a revision"
+    (superseded.action == .unchanged && superseded.version == changedA.version &&
+      superseded.nextVersion == changedA.nextVersion &&
+      (superseded.docs.get? a).any (fun doc => doc.textHash == 20 && doc.syncSnapshotSeq == 3))
+  let unchanged := DocumentState.syncFileDecision superseded.docs b
+    { mkSnapshot 10 with readSeq := 4 } superseded.nextVersion
+  require "another file's unchanged read preserves its token and the allocator"
+    (unchanged.version == openedB.version && unchanged.nextVersion == changedA.nextVersion)
+  let reopened := DocumentState.syncFileDecision (unchanged.docs.erase a) a
+    { mkSnapshot 20 with readSeq := 5 } unchanged.nextVersion
+  require "closing and reopening does not reuse a document revision"
+    (reopened.version == 4 && reopened.nextVersion == 5)
+
 private def checkMarkSyncedVersion : IO Unit := do
   let uri := "file:///workspace/Foo.lean"
   let docs : DocumentState.Docs := Std.TreeMap.empty.insert uri (mkDoc 3 (some "Foo"))
@@ -181,6 +207,7 @@ def main : IO Unit := do
   checkSyncFileDecisionOpen
   checkSyncFileDecisionUnchanged
   checkSyncFileDecisionChange
+  checkInterleavedDocumentRevisions
   checkMarkSyncedVersion
   checkMarkSavedVersion
 
diff --git a/tests/lean/BeamTest/Broker/McpProjectionTest.lean b/tests/lean/BeamTest/Broker/McpProjectionTest.lean
index d4a5f307..c48adf93 100644
--- a/tests/lean/BeamTest/Broker/McpProjectionTest.lean
+++ b/tests/lean/BeamTest/Broker/McpProjectionTest.lean
@@ -246,7 +246,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
 
   let runAtInput : Beam.Mcp.RunAtInput := {
     path := "Demo.lean"
-    version := 12
+    snapshot := ⟨"test-session", 12⟩
     line := 4
     character := 2
     text := "exact h"
@@ -259,7 +259,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
   require "runAt op" (runAtReq.op == .runAt)
   require "runAt backend" (runAt.backend == .lean)
   require "runAt path" (runAt.path == "Demo.lean")
-  require "runAt version" (runAt.version == 12)
+  require "runAt snapshot" (runAt.snapshot == ⟨"test-session", 12⟩)
   require "runAt line" (runAt.line == 4)
   require "runAt character" (runAt.character == 2)
   require "runAt text" (runAt.text == "exact h")
@@ -283,7 +283,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
 
   let positionInput : Beam.Mcp.PositionInput := {
     path := "Demo.lean"
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
     line := 7
     character := 3
   }
@@ -293,7 +293,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | .hover request => some request
     | _ => none
   require "hover op" (hoverReq.op == .hover)
-  require "hover version" (hover.version == 13)
+  require "hover snapshot" (hover.snapshot == ⟨"test-session", 13⟩)
 
   let signatureHelpReq ← expectOk "signature-help tool request" <|
     Beam.Mcp.leanOperationToBrokerRequest .signatureHelp workspaceId
@@ -303,7 +303,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | _ => none
   require "signature-help op" (signatureHelpReq.op == .signatureHelp)
   require "signature-help backend" (signatureHelp.backend == .lean)
-  require "signature-help version" (signatureHelp.version == 13)
+  require "signature-help snapshot" (signatureHelp.snapshot == ⟨"test-session", 13⟩)
 
   let definitionReq ← expectOk "definition tool request" <|
     Beam.Mcp.leanOperationToBrokerRequest .definition workspaceId
@@ -313,11 +313,11 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | _ => none
   require "definition op" (definitionReq.op == .definition)
   require "definition backend" (definition.backend == .lean)
-  require "definition version" (definition.version == 13)
+  require "definition snapshot" (definition.snapshot == ⟨"test-session", 13⟩)
 
   let referencesInput : Beam.Mcp.ReferencesInput := {
     path := "Demo.lean"
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
     line := 7
     character := 3
     includeDeclaration? := some false
@@ -329,7 +329,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | .references request => some request
     | _ => none
   require "references op" (referencesReq.op == .references)
-  require "references version" (references.version == 13)
+  require "references snapshot" (references.snapshot == ⟨"test-session", 13⟩)
   require "references include declaration" (references.includeDeclaration? == some false)
   let referencesJson := toJson referencesInput
   requireJsonBool "references input json" "include_declaration" false referencesJson
@@ -338,9 +338,9 @@ private def checkBrokerRequestAdapters : IO Unit := do
     fromJson? (α := Beam.Mcp.ReferencesInput) referencesJson
   require "decoded references include declaration" (decodedReferences.includeDeclaration? == some false)
 
-  let documentSymbolsInput : Beam.Mcp.DocumentSymbolsInput := {
+  let documentSymbolsInput : Beam.Mcp.DocumentInput := {
     path := "Demo.lean"
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
   }
   let documentSymbolsReq ← expectOk "document-symbols tool request" <|
     Beam.Mcp.leanOperationToBrokerRequest .documentSymbols workspaceId
@@ -350,7 +350,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | _ => none
   require "document-symbols op" (documentSymbolsReq.op == .documentSymbols)
   require "document-symbols path" (documentSymbols.path == "Demo.lean")
-  require "document-symbols version" (documentSymbols.version == 13)
+  require "document-symbols snapshot" (documentSymbols.snapshot == ⟨"test-session", 13⟩)
 
   let workspaceSymbolsInput : Beam.Mcp.WorkspaceSymbolsInput := {
     query := "Demo"
@@ -366,7 +366,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
 
   let goalsBeforeInput : Beam.Mcp.GoalsInput := {
     path := "Demo.lean"
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
     line := 7
     character := 3
     mode := .before
@@ -384,7 +384,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
 
   let goalsAfterInput : Beam.Mcp.GoalsInput := {
     path := "Demo.lean"
-    version := 13
+    snapshot := ⟨"test-session", 13⟩
     line := 7
     character := 3
     mode := .after
@@ -401,7 +401,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
 
   let todoInput : Beam.Mcp.TodoInput := {
     path := "Demo.lean"
-    version := 14
+    snapshot := ⟨"test-session", 14⟩
     startLine := 1
     startCharacter := 0
     endLine := 8
@@ -416,7 +416,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | _ => none
   require "todo op" (todoReq.op == .todo)
   require "todo backend" (todo.backend == .lean)
-  require "todo version" (todo.version == 14)
+  require "todo snapshot" (todo.snapshot == ⟨"test-session", 14⟩)
   require "todo start line" (todo.line == 1)
   require "todo start character" (todo.character == 0)
   require "todo end line" (todo.endLine == 8)
@@ -435,7 +435,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
   }
   let codeActionResolveInput : Beam.Mcp.CodeActionResolveInput := {
     path := "Demo.lean"
-    version := 15
+    snapshot := ⟨"test-session", 15⟩
     codeAction
   }
   let codeActionResolveReq ← expectOk "code-action-resolve tool request" <|
@@ -447,7 +447,7 @@ private def checkBrokerRequestAdapters : IO Unit := do
     | _ => none
   require "code-action-resolve op" (codeActionResolveReq.op == .codeActionResolve)
   require "code-action-resolve backend" (codeActionResolve.backend == .lean)
-  require "code-action-resolve version" (codeActionResolve.version == 15)
+  require "code-action-resolve snapshot" (codeActionResolve.snapshot == ⟨"test-session", 15⟩)
   require "code-action-resolve title" (codeActionResolve.codeAction.title == codeAction.title)
   let codeActionResolveJson := toJson codeActionResolveInput
   discard <| requireObjVal "code-action-resolve input json" "code_action" codeActionResolveJson
@@ -572,13 +572,13 @@ private def checkRunAtNormalization : IO Unit := do
 
 private def sampleSyncResult : Beam.Broker.SyncFileResult := {
   path := "Demo.lean"
-  version := 7
+  snapshot := ⟨"test-session", 7⟩
   diagnostics := {
     counts := { error := 1, warning := 1 }
     items? := some #[{
       path := "Demo.lean"
       uri := "file:///repo/Demo.lean"
-      version? := some 7
+      snapshot? := some ⟨"test-session", 7⟩
       severity? := some .warning
       range := { start := { line := 1, character := 2 }, «end» := { line := 1, character := 5 } }
       message := "unused variable"
@@ -605,7 +605,7 @@ private def checkSyncAndSaveNormalization : IO Unit := do
         rangeEndLine? := some 20
       }
   requireJsonString "sync result" "path" "Demo.lean" normalizedSync
-  requireJsonInt "sync result" "version" 7 normalizedSync
+  requireJsonString "sync result" "snapshot" "test-session/7" normalizedSync
   let diagnostics ← requireObjVal "sync result" "diagnostics" normalizedSync
   let counts ← requireObjVal "sync diagnostics" "counts" diagnostics
   requireJsonInt "sync diagnostic counts" "error" 1 counts
@@ -630,7 +630,7 @@ private def checkSyncAndSaveNormalization : IO Unit := do
   let rawSave := Json.mkObj [
     ("path", toJson "Demo.lean"),
     ("module", toJson "Demo"),
-    ("version", toJson (7 : Nat)),
+    ("snapshot", toJson "test-session/7"),
     ("sourceHash", toJson "abc"),
     ("olean", toJson "/tmp/Demo.olean"),
     ("ilean", toJson "/tmp/Demo.ilean"),
@@ -678,7 +678,7 @@ private def checkTransportErrorNormalization : IO Unit := do
 
 private def checkTodoNormalization : IO Unit := do
   let rawTodo := Json.mkObj [
-    ("version", toJson (1 : Nat)),
+    ("snapshot", toJson "test-session/1"),
     ("range", toJson ({ start := { line := 0, character := 0 }, «end» := { line := 2, character := 0 } } : Lean.Lsp.Range)),
     ("items", Json.arr #[
       Json.mkObj [
@@ -728,7 +728,7 @@ private def checkTodoNormalization : IO Unit := do
 
 private def checkCodeActionResolveNormalization : IO Unit := do
   let rawResult := Json.mkObj [
-    ("version", toJson (15 : Nat)),
+    ("snapshot", toJson "test-session/15"),
     ("codeAction", Json.mkObj [
       ("title", toJson ("Replace fixture hole with zero" : String)),
       ("kind", toJson ("quickfix" : String))
diff --git a/tests/lean/BeamTest/Broker/McpProtocolTest.lean b/tests/lean/BeamTest/Broker/McpProtocolTest.lean
index 3848ccc0..f2e58cd0 100644
--- a/tests/lean/BeamTest/Broker/McpProtocolTest.lean
+++ b/tests/lean/BeamTest/Broker/McpProtocolTest.lean
@@ -377,17 +377,17 @@ private def checkToolsListShape : IO Unit := do
     ("beam_stats", #[]),
     ("beam_feedback_report", Beam.Feedback.requiredInputFields.push "workspace"),
     ("lean_drop_workspace", #["workspace"]),
-    ("lean_run_at", #["path", "version", "line", "character", "text", "workspace"]),
-    ("lean_run_at_handle", #["path", "version", "line", "character", "text", "workspace"]),
-    ("lean_hover", #["path", "version", "line", "character", "workspace"]),
-    ("lean_signature_help", #["path", "version", "line", "character", "workspace"]),
-    ("lean_definition", #["path", "version", "line", "character", "workspace"]),
-    ("lean_references", #["path", "version", "line", "character", "workspace"]),
-    ("lean_document_symbols", #["path", "version", "workspace"]),
+    ("lean_run_at", #["path", "snapshot", "line", "character", "text", "workspace"]),
+    ("lean_run_at_handle", #["path", "snapshot", "line", "character", "text", "workspace"]),
+    ("lean_hover", #["path", "snapshot", "line", "character", "workspace"]),
+    ("lean_signature_help", #["path", "snapshot", "line", "character", "workspace"]),
+    ("lean_definition", #["path", "snapshot", "line", "character", "workspace"]),
+    ("lean_references", #["path", "snapshot", "line", "character", "workspace"]),
+    ("lean_document_symbols", #["path", "snapshot", "workspace"]),
     ("lean_workspace_symbols", #["query", "workspace"]),
-    ("lean_goals", #["path", "version", "line", "character", "mode", "workspace"]),
-    ("lean_todo", #["path", "version", "start_line", "start_character", "end_line", "end_character", "workspace"]),
-    ("lean_code_action_resolve", #["path", "version", "code_action", "workspace"]),
+    ("lean_goals", #["path", "snapshot", "line", "character", "mode", "workspace"]),
+    ("lean_todo", #["path", "snapshot", "start_line", "start_character", "end_line", "end_character", "workspace"]),
+    ("lean_code_action_resolve", #["path", "snapshot", "code_action", "workspace"]),
     ("lean_run_with", #["path", "handle", "text", "workspace"]),
     ("lean_run_with_linear", #["path", "handle", "text", "workspace"]),
     ("lean_release", #["path", "handle", "workspace"]),
@@ -1371,7 +1371,7 @@ private def checkServerBasics : IO Unit := do
   let relativeWorkspaceResp ← handleRpcRequest state opts "relative workspace rejection" 32
       "tools/call" <| some <| toolCallParams "lean_run_at" <| Json.mkObj [
         ("path", toJson "Demo.lean"),
-        ("version", toJson (0 : Nat)),
+        ("snapshot", toJson "stale/1"),
         ("line", toJson (0 : Nat)),
         ("character", toJson (0 : Nat)),
         ("text", toJson "rfl"),
@@ -1622,7 +1622,7 @@ private def checkDiagnosticLogForwarding : IO Unit := do
     let data ← requireObjVal "warning log params" "data" params
     discard <| requireObjVal "warning log data" "range" data
     discard <| requireObjVal "warning log data" "uri" data
-    discard <| requireObjVal "warning log data" "version" data
+    discard <| requireObjVal "warning log data" "snapshot" data
     requireJsonBool "warning log data" "completion_blocking" false data
     requireFieldAbsent "warning log data" "save_blocking" data
     let message ← IO.ofExcept <| data.getObjValAs? String "message"
@@ -1669,7 +1669,7 @@ private def checkDiagnosticLogForwarding : IO Unit := do
     let refreshResult ← requireObjVal "lean_refresh response" "result" refreshResp
     requireJsonBool "lean_refresh result" "isError" false refreshResult
     let refreshStructured ← requireObjVal "lean_refresh result" "structuredContent" refreshResult
-    discard <| IO.ofExcept <| refreshStructured.getObjValAs? Nat "version"
+    discard <| IO.ofExcept <| refreshStructured.getObjValAs? Beam.SnapshotRef "snapshot"
     discard <| requireObjVal "lean_refresh structured result" "readiness" refreshStructured
     let refreshDiagnostics ← requireObjVal "lean_refresh structured result" "diagnostics" refreshStructured
     discard <| requireObjVal "lean_refresh diagnostics" "counts" refreshDiagnostics
@@ -1686,7 +1686,7 @@ private def checkDiagnosticLogForwarding : IO Unit := do
     let closeSaveStructured ← requireObjVal "lean_close_save result" "structuredContent" closeSaveResult
     requireJsonBool "lean_close_save structured result" "closed" true closeSaveStructured
     let saved ← requireObjVal "lean_close_save structured result" "saved" closeSaveStructured
-    discard <| IO.ofExcept <| saved.getObjValAs? Nat "version"
+    discard <| IO.ofExcept <| saved.getObjValAs? Beam.SnapshotRef "snapshot"
     discard <| requireObjVal "lean_close_save saved result" "sync" saved
     let closeSaveWorkspace ←
       requireObjVal "lean_close_save structured result" "workspace" closeSaveStructured
diff --git a/tests/lean/BeamTest/Broker/OpenDocsTest.lean b/tests/lean/BeamTest/Broker/OpenDocsTest.lean
index 88e39a1f..34f57702 100644
--- a/tests/lean/BeamTest/Broker/OpenDocsTest.lean
+++ b/tests/lean/BeamTest/Broker/OpenDocsTest.lean
@@ -59,6 +59,7 @@ private def checkDocProjection : IO Unit := do
         fileProgress? := some { updates := 3, done := true }
       }
     let session : OpenDocs.SessionView := {
+      sessionToken := "test-session"
       root
       docs
     }
@@ -67,6 +68,7 @@ private def checkDocProjection : IO Unit := do
     let file ← requireOnlyFile "open docs saved session" sessionJson
     requireJsonString "open docs file" "uri" uri file
     requireJsonString "open docs file" "path" "Demo.lean" file
+    requireJsonString "open docs file" "snapshot" "test-session/2" file
     requireJsonString "open docs file" "diskStatus" "matchesTracked" file
     requireFieldAbsent "open docs file" "status" file
     requireJsonBool "open docs file" "checkpointed" true file
@@ -92,6 +94,7 @@ private def checkDocProjection : IO Unit := do
 
     let nonFileUri := "https://example.invalid/Demo.lean"
     let nonFileSession : OpenDocs.SessionView := {
+      sessionToken := "test-session"
       root
       docs := Std.TreeMap.empty.insert nonFileUri {
         (mkDoc text 2) with checkpointedVersion? := some 2
diff --git a/tests/lean/BeamTest/Broker/PendingTest.lean b/tests/lean/BeamTest/Broker/PendingTest.lean
index a098855e..8e0e6b80 100644
--- a/tests/lean/BeamTest/Broker/PendingTest.lean
+++ b/tests/lean/BeamTest/Broker/PendingTest.lean
@@ -415,8 +415,9 @@ private def checkDiagnosticLineCanExceedProgressRange : IO Unit := do
   let pending ← mkPending
     (progress? := some finished)
     (tracked? := some ("file:///workspace/Foo.lean", 1))
-  PendingRequest.observeDiagnostics
+  PendingRequest.observePublishDiagnostics
     (System.FilePath.mk ".")
+    "test-session"
     pending
     (mkPublishDiagnostics #[farDiagnostic])
   require "diagnostic publication does not rewrite fileProgress range"
@@ -436,8 +437,9 @@ private def observeStreamedDiagnostics
     (diagnosticScope := diagnosticScope)
     (emitDiagnostic? := some fun diagnostic =>
       streamedRef.modify (·.push diagnostic))
-  PendingRequest.observeDiagnostics
+  PendingRequest.observePublishDiagnostics
     (System.FilePath.mk "/workspace")
+    "test-session"
     pending
     (mkPublishDiagnostics diagnostics)
   streamedRef.get
@@ -449,8 +451,9 @@ private def checkDiagnosticEmitterFailureIsolation : IO Unit := do
     (diagnosticScope := .all)
     (emitDiagnostic? := some fun _ =>
       throw <| IO.userError "diagnostic sink failed")
-  PendingRequest.observeDiagnostics
+  PendingRequest.observePublishDiagnostics
     (System.FilePath.mk "/workspace")
+    "test-session"
     pending
     (mkPublishDiagnostics #[diagnostic])
   require "diagnostic sink failure still records the publication"
@@ -499,10 +502,40 @@ private def checkSetupFileProgressStreamsByScope : IO Unit := do
     (defaultStreamed.all (fun diagnostic => diagnostic.severity? == some .information))
 
   let allStreamed ← observeStreamedDiagnostics .all #[setupProgress, warning, goalsAccomplished]
+  require "streamed diagnostics carry their backend snapshot"
+    (allStreamed.all fun diagnostic => diagnostic.snapshot? == some ⟨"test-session", 1⟩)
   require "all diagnostic scope streams user-facing setup-file status and warning"
     (allStreamed.map (·.message) == #[setupProgress.message, warning.message])
 
+private def checkDiagnosticSnapshotIsolation : IO Unit := do
+  let uri := "file:///workspace/Foo.lean"
+  let diagnostic := mkDiagnosticWithSeverity (mkRange 1 0 1 4) .warning "same warning"
+  let streamed ← IO.mkRef (#[] : Array StreamDiagnostic)
+  let pending ← mkPending (tracked? := some (uri, 2)) (diagnosticScope := .all)
+    (emitDiagnostic? := some fun diagnostic => streamed.modify (·.push diagnostic))
+  -- Explicit revisions belong to one document lifetime, even when the URI matches.
+  for version in [1, 3, 0, -1] do
+    PendingRequest.observePublishDiagnostics (System.FilePath.mk "/workspace") "test-session" pending {
+      uri, version? := some version, diagnostics := #[diagnostic]
+    }
+  require "other revisions do not establish completion evidence" (!(← pending.diagnosticsSeenRef.get))
+  require "other revisions do not replace current diagnostics" ((← pending.diagnosticsRef.get).isEmpty)
+  require "other revisions do not stream diagnostics" ((← streamed.get).isEmpty)
+  -- Unversioned observations remain best effort, but cannot consume a versioned stream event.
+  for version? in [none, some 2, some 2] do
+    PendingRequest.observePublishDiagnostics (System.FilePath.mk "/workspace") "test-session" pending {
+      uri, version?, diagnostics := #[diagnostic]
+    }
+  require "matching diagnostics establish completion evidence" (← pending.diagnosticsSeenRef.get)
+  require "deduplication preserves a newly identified snapshot"
+    ((← streamed.get).map (·.snapshot?) == #[none, some ⟨"test-session", 2⟩])
+  PendingRequest.observePublishDiagnostics (System.FilePath.mk "/workspace") "test-session" pending {
+    uri, version? := some 2, diagnostics := #[]
+  }
+  require "a current empty publication clears current diagnostics" ((← pending.diagnosticsRef.get).isEmpty)
+
 def main : IO Unit := do
+  checkDiagnosticSnapshotIsolation
   checkActiveRegistry
   checkActiveRegistryCloseDrain
   checkPendingCancellationIdentity
diff --git a/tests/lean/BeamTest/Broker/ProtocolTest.lean b/tests/lean/BeamTest/Broker/ProtocolTest.lean
index 9f9d9396..2702c60a 100644
--- a/tests/lean/BeamTest/Broker/ProtocolTest.lean
+++ b/tests/lean/BeamTest/Broker/ProtocolTest.lean
@@ -154,31 +154,31 @@ private def sampleRequest : Op → Request
   | .refreshFile => { payload := .refreshFile { path := "Demo.lean" } }
   | .close => { payload := .close { path := "Demo.lean" } }
   | .runAt => { payload := .runAt {
-      path := "Demo.lean", version := 7, line := 1, character := 2, text := "exact trivial"
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2, text := "exact trivial"
     } }
   | .hover => { payload := .hover {
-      path := "Demo.lean", version := 7, line := 1, character := 2
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2
     } }
   | .signatureHelp => { payload := .signatureHelp {
-      path := "Demo.lean", version := 7, line := 1, character := 2
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2
     } }
   | .definition => { payload := .definition {
-      path := "Demo.lean", version := 7, line := 1, character := 2
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2
     } }
   | .references => { payload := .references {
-      path := "Demo.lean", version := 7, line := 1, character := 2
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2
     } }
-  | .documentSymbols => { payload := .documentSymbols { path := "Demo.lean", version := 7 } }
+  | .documentSymbols => { payload := .documentSymbols { path := "Demo.lean", snapshot := ⟨"test-session", 7⟩ } }
   | .workspaceSymbols => { payload := .workspaceSymbols { query := "Demo" } }
   | .codeActionResolve => { payload := .codeActionResolve {
-      path := "Demo.lean", version := 7, codeAction := { title := "Resolve" }
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, codeAction := { title := "Resolve" }
     } }
   | .saveOlean => { payload := .saveOlean { path := "Demo.lean" } }
   | .goals => { payload := .goals {
-      path := "Demo.lean", version := 7, line := 1, character := 2
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2
     } }
   | .todo => { payload := .todo {
-      path := "Demo.lean", version := 7, line := 1, character := 2,
+      path := "Demo.lean", snapshot := ⟨"test-session", 7⟩, line := 1, character := 2,
       endLine := 3, endCharacter := 4
     } }
   | .runWith => { payload := .runWith {
@@ -207,13 +207,13 @@ private def diagnostic (severity : DiagnosticSeverity) (message : String) : Diag
   }
 
 private def syncResultFor
-    (version : Nat)
+    (snapshot : Nat)
     (saveReady : Bool := true)
     (reason : String := "ok")
     (blockingErrorCount : Nat := 0)
     (warningCount : Nat := 0) : SyncFileResult := {
   path := "Demo.lean"
-  version
+  snapshot := ⟨"test-session", snapshot⟩
   diagnostics := { counts := { warning := warningCount } }
   readiness := {
     saveReady
@@ -241,14 +241,26 @@ private def syncReadinessJson (saveReady : Bool := true) : Json :=
     ("blockingMessages", toJson (#[] : Array SyncBlockingCommandMessage))
   ]
 
-private def syncFileResultJson (version : Nat) (readiness : Json) : Json :=
+private def syncFileResultJson (snapshot : Nat) (readiness : Json) : Json :=
   Json.mkObj [
     ("path", toJson "Demo.lean"),
-    ("version", toJson version),
+    ("snapshot", toJson (s!"test-session/{snapshot}")),
     ("diagnostics", Json.mkObj [("counts", syncDiagnosticCountsJson)]),
     ("readiness", readiness)
   ]
 
+private def checkSnapshotCodec : IO Unit := do
+  let snapshot : Beam.SnapshotRef := ⟨"session-a", 42⟩
+  require "snapshot is a JSON string" (toJson snapshot == toJson "session-a/42")
+  let decoded : Beam.SnapshotRef ← IO.ofExcept <| fromJson? (toJson snapshot)
+  require "snapshot codec round trips" (decoded == snapshot)
+  for invalid in [toJson (1 : Nat), Json.null, toJson "", toJson "session-a/0",
+      toJson "session-a/01", toJson "/1", toJson "session-a/1/2"] do
+    expectDecodeFailure Beam.SnapshotRef "malformed snapshot" invalid
+  let request := toJson <| sampleRequest .runAt
+  expectDecodeFailure Request "numeric snapshot" <| request.setObjVal! "snapshot" (toJson (7 : Nat))
+  expectDecodeFailure Request "removed version field" <| request.setObjVal! "version" (toJson (7 : Nat))
+
 private def checkResponseJsonShape : IO Unit := do
   let successJson := toJson <| Response.success (Json.mkObj [("value", toJson (1 : Nat))])
   requireJsonBool "success response" "ok" true successJson
@@ -300,7 +312,7 @@ private def checkStreamMessageDecode : IO Unit := do
   let diagnostic : StreamDiagnostic := {
     path := "Demo.lean"
     uri := "file:///repo/Demo.lean"
-    version? := some 3
+    snapshot? := some ⟨"test-session", 3⟩
     severity? := some .warning
     range := lspRange 0 0 1
     message := "unused variable"
@@ -400,10 +412,10 @@ private def checkSaveResultJsonDecode : IO Unit := do
     (decodedSave.sourceHash == saveResult.sourceHash)
   require "save result derives its path from nested sync"
     (decodedSave.path == "Demo.lean")
-  require "save result derives its version from nested sync"
-    (decodedSave.version == 7)
-  require "save result round-trip preserves nested sync version"
-    (decodedSave.sync.version == saveResult.sync.version)
+  require "save result derives its snapshot from nested sync"
+    (decodedSave.snapshot == ⟨"test-session", 7⟩)
+  require "save result round-trip preserves nested sync snapshot"
+    (decodedSave.sync.snapshot == saveResult.sync.snapshot)
 
   let closeSaveResult : CloseSaveResult := { saved := saveResult }
   let decodedCloseSave ← expectOk "close-save result round-trip" <|
@@ -419,8 +431,8 @@ private def checkSaveResultJsonDecode : IO Unit := do
 
   expectDecodeFailure SaveOleanResult "save result path does not match nested sync" <|
     (toJson saveResult).setObjVal! "path" (toJson "Other.lean")
-  expectDecodeFailure SaveOleanResult "save result version does not match nested sync" <|
-    (toJson saveResult).setObjVal! "version" (toJson (8 : Nat))
+  expectDecodeFailure SaveOleanResult "save result snapshot does not match nested sync" <|
+    (toJson saveResult).setObjVal! "snapshot" (toJson "test-session/8")
 
   let malformedNestedSave := Json.mkObj [
     ("closed", toJson true),
@@ -445,7 +457,7 @@ private def checkOrderedJsonPretty : IO Unit := do
     "  \"ok\": true,",
     "  \"result\": {",
     "    \"path\": \"Demo.lean\",",
-    "    \"version\": 3,",
+    "    \"snapshot\": \"test-session/3\",",
     "    \"diagnostics\": {",
     "      \"counts\": {",
     "        \"error\": 0,",
@@ -581,11 +593,11 @@ private def checkDocumentVersionMismatchErrorData : IO Unit := do
   let data := documentVersionMismatchErrorData 1 2
     (currentVersion? := some 2)
     (uri? := some "file:///A.lean")
-  requireJsonString "version mismatch data" "reason" "documentVersionMismatch" data
-  requireJsonInt "version mismatch data" "expectedVersion" 1 data
-  requireJsonInt "version mismatch data" "acceptedVersion" 2 data
-  requireJsonInt "version mismatch data" "currentVersion" 2 data
-  requireJsonString "version mismatch data" "uri" "file:///A.lean" data
+  requireJsonString "backend version mismatch data" "reason" "documentVersionMismatch" data
+  requireJsonInt "backend version mismatch data" "expectedVersion" 1 data
+  requireJsonInt "backend version mismatch data" "acceptedVersion" 2 data
+  requireJsonInt "backend version mismatch data" "currentVersion" 2 data
+  requireJsonString "backend version mismatch data" "uri" "file:///A.lean" data
 
 private def checkReadinessBoundary : IO Unit := do
   let uri := "file:///workspace/SaveSmoke/A.lean"
@@ -654,7 +666,7 @@ private def checkReadinessBoundary : IO Unit := do
   require "readiness success response should keep fileProgress"
     (successResp.fileProgress? == some { updates := 5, done := true })
   let successResult ← requireResponseResult "readiness success response" successResp
-  requireJsonInt "readiness success payload" "version" 9 successResult
+  requireJsonString "readiness success payload" "snapshot" "test-session/9" successResult
   requireJsonString "readiness success payload" "path" "Demo.lean" successResult
   requireFieldAbsent "readiness success payload" "warningCount" successResult
   requireFieldAbsent "readiness success payload" "stateErrorCount" successResult
@@ -753,7 +765,7 @@ private def checkStaleDirectDepHints : IO Unit := do
     noopSyncHints.isEmpty
 
 private def checkRequestBoundary : IO Unit := do
-  expectDecodeFailure Request "run_at request missing version" <| Json.mkObj [
+  expectDecodeFailure Request "run_at request missing snapshot" <| Json.mkObj [
     ("op", toJson "run_at"),
     ("backend", toJson "lean"),
     ("path", toJson "Demo.lean"),
@@ -765,7 +777,7 @@ private def checkRequestBoundary : IO Unit := do
     ("op", toJson "run_at"),
     ("backend", toJson "lean"),
     ("path", toJson "Demo.lean"),
-    ("version", toJson 7),
+    ("snapshot", toJson "test-session/7"),
     ("line", toJson 1),
     ("character", toJson 2)
   ]
@@ -779,7 +791,7 @@ private def checkRequestBoundary : IO Unit := do
     ("op", toJson "code_action_resolve"),
     ("backend", toJson "lean"),
     ("path", toJson "Demo.lean"),
-    ("version", toJson 7)
+    ("snapshot", toJson "test-session/7")
   ]
 
   expectMethodError
@@ -1459,6 +1471,138 @@ private partial def waitForWorkspaceRoot
     IO.sleep 10
     waitForWorkspaceRoot runtime workspaceId expected (tries - 1)
 
+private def pendingDocument (runtime : ServerRuntime) (session : Session) : IO DocState := do
+  let doc? ← runtime.state.atomically do
+    let state ← get
+    pure <| state.workspaces.get? session.workspaceId |>.bind (·.lean.session?)
+      |>.bind (fun current => current.docs.get? (sessionUri (session.root / "Demo.lean")))
+  let some doc := doc? | throw <| IO.userError "missing pending test document"
+  pure doc
+
+private def withPendingDocument
+    (act : ServerRuntime → Session → IO Unit) : IO Unit := do
+  let root := System.FilePath.mk s!"/tmp/beam-pending-document-{← IO.monoNanosNow}"
+  IO.FS.createDirAll root
+  let root ← IO.FS.realPath root
+  IO.FS.writeFile (root / "Demo.lean") "def demo : Nat := 1\n"
+  let exit := root / "exit-backend"
+  let workspaceId := "pending-document"
+  let runtime ← ServerRuntime.create { root } workspaceId
+  let session ← pendingOnlySession workspaceId root exit
+  runtime.state.atomically do
+    modify fun state => { state with workspaces := state.workspaces.modify workspaceId fun workspace =>
+      { workspace with lean := { nextEpoch := 2, session? := some session } } }
+  try
+    let first ← runtime.dispatchRequest {
+      payload := .updateFile { path := "Demo.lean" }, workspaceId? := some workspaceId
+    }
+    require "initial update succeeds" first.ok
+    act runtime session
+  finally
+    IO.FS.writeFile exit "exit"
+    runtime.close
+    try
+      discard <| session.proc.wait
+    catch _ => pure ()
+    IO.FS.removeDirAll root
+
+private inductive PendingDocumentChange where
+  | unchanged | edit | close | reopen
+  deriving BEq, Repr
+
+private def checkCompletedDocumentIsolation : IO Unit := do
+  for sync in [false, true] do
+    for change in [PendingDocumentChange.unchanged, .edit, .close, .reopen] do
+      withPendingDocument fun runtime session => do
+        let label := s!"{if sync then "sync" else "hover"} completion after {repr change}"
+        let first ← pendingDocument runtime session
+        let snapshot : Beam.SnapshotRef := ⟨session.sessionToken, first.version⟩
+        let payload := if sync then RequestPayload.syncFile { path := "Demo.lean" }
+          else .hover { path := "Demo.lean", snapshot, line := 0, character := 4 }
+        let task ← IO.asTask (prio := Task.Priority.dedicated) <| runtime.dispatchRequest {
+          payload, workspaceId? := some session.workspaceId
+        }
+        let requests ← takePendingRequests session.pending 1
+        if change == .close || change == .reopen then
+          let closed ← runtime.dispatchRequest {
+            payload := .close { path := "Demo.lean" }, workspaceId? := some session.workspaceId
+          }
+          require s!"{label}: close succeeds" closed.ok
+        if change == .edit then
+          IO.FS.writeFile (session.root / "Demo.lean") "def demo : Nat := 2\n"
+        let currentSnapshot? ←
+          if change == .close then pure none
+          else do
+            let updated ← runtime.dispatchRequest {
+              payload := .updateFile { path := "Demo.lean" }, workspaceId? := some session.workspaceId
+            }
+            let updated : UpdateFileResult ← IO.ofExcept <|
+              fromJson? (← requireResponseResult label updated)
+            pure (some updated.snapshot)
+        for request in requests do
+          request.progressRef.set (some { updates := 99, done := true })
+          let result := if sync then toJson ({
+              version := first.version
+              saveReadiness := { version := first.version, textHash := first.textHash }
+            } : DiagnosticsBarrierResult) else Json.mkObj []
+          PendingRequest.resolveResponse request result
+        let response ← IO.ofExcept <| ← IO.wait task
+        if change == .unchanged then
+          require s!"{label}: unchanged document succeeds" response.ok
+          require s!"{label}: unchanged token is preserved" (currentSnapshot? == some snapshot)
+        else
+          require s!"{label}: replaced document returns contentModified"
+            (response.error?.any fun err => err.code == "contentModified")
+          let some err := response.error? | throw <| IO.userError s!"{label}: missing error"
+          let data ← requireErrorData label err
+          requireJsonString label "reason" "snapshotMismatch" data
+          requireJsonString label "expectedSnapshot" snapshot.encode data
+          match currentSnapshot? with
+          | some current => requireJsonString label "currentSnapshot" current.encode data
+          | none => requireFieldAbsent label "currentSnapshot" data
+          if change != .close then
+            let current ← pendingDocument runtime session
+            require s!"{label}: old progress does not overwrite the replacement"
+              current.fileProgress?.isNone
+            require s!"{label}: old sync does not mark the replacement synced"
+              (current.lastSyncEventSeq == 0)
+
+private def checkStaleCompletionDiagnostic : IO Unit :=
+  withPendingDocument fun runtime session => do
+    let first ← pendingDocument runtime session
+    discard <| runtime.dispatchRequest {
+      payload := .close { path := "Demo.lean" }, workspaceId? := some session.workspaceId
+    }
+    discard <| runtime.dispatchRequest {
+      payload := .updateFile { path := "Demo.lean" }, workspaceId? := some session.workspaceId
+    }
+    let current ← pendingDocument runtime session
+    let task ← IO.asTask (prio := Task.Priority.dedicated) <| runtime.dispatchRequest {
+      payload := .syncFile { path := "Demo.lean" }, workspaceId? := some session.workspaceId
+    }
+    let requests ← takePendingRequests session.pending 1
+    for request in requests do
+      PendingRequest.observePublishDiagnostics session.root session.sessionToken request {
+        uri := sessionUri (session.root / "Demo.lean")
+        version? := some first.version
+        diagnostics := #[{
+          range := lspRange 0 0 1
+          severity? := some .error
+          message := "Failed to build module dependencies."
+        }]
+      }
+      request.progressRef.set (some { updates := 1, done := true })
+      PendingRequest.resolveResponse request <| toJson ({
+        version := current.version
+        saveReadiness := { version := current.version, textHash := current.textHash }
+      } : DiagnosticsBarrierResult)
+    let response ← IO.ofExcept <| ← IO.wait task
+    let result : SyncFileResult ← IO.ofExcept <|
+      fromJson? (← requireResponseResult "old diagnostic must not block the current barrier" response)
+    require "current barrier remains save-ready" result.readiness.saveReady
+    require "current barrier returns the current snapshot"
+      (result.snapshot == ⟨session.sessionToken, current.version⟩)
+
 private def checkCompletedRequestResetIsolation : IO Unit := do
   let nonce ← IO.monoNanosNow
   let workspaceId := s!"completed-reset-{nonce}"
@@ -1482,7 +1626,7 @@ private def checkCompletedRequestResetIsolation : IO Unit := do
   let documentTask ← IO.asTask (prio := Task.Priority.dedicated) <| runtime.dispatchRequest {
     payload := .runAt {
       path := "Demo.lean"
-      version := 1
+      snapshot := ⟨session.sessionToken, 1⟩
       line := 0
       character := 0
       text := "rfl"
@@ -1644,6 +1788,7 @@ private def checkWrapperDaemonAuthorization : IO Unit := do
 def main : IO Unit := do
   checkDaemonReadinessProtocol
   checkServerHelloProtocol
+  checkSnapshotCodec
   checkResponseJsonShape
   checkStreamMessageDecode
   checkResponseJsonDecode
@@ -1661,6 +1806,8 @@ def main : IO Unit := do
   checkLifecycleTeardownConcurrency
   checkDeadSessionCleanupReleasesStateMutex
   checkWorkspaceSnapshotResetIsolation
+  checkCompletedDocumentIsolation
+  checkStaleCompletionDiagnostic
   checkCompletedRequestResetIsolation
   checkSessionCloseAdmission
   checkBrokerConfigBoundary
diff --git a/tests/lean/BeamTest/Broker/RequestHandleTest.lean b/tests/lean/BeamTest/Broker/RequestHandleTest.lean
index 02f54887..8a911d4a 100644
--- a/tests/lean/BeamTest/Broker/RequestHandleTest.lean
+++ b/tests/lean/BeamTest/Broker/RequestHandleTest.lean
@@ -58,7 +58,7 @@ def checkCancellationAndLifetime : IO Unit := do
   let req : Beam.Broker.Request := {
     payload := .runAt {
       path := "Cancelled.lean"
-      version := 1
+      snapshot := ⟨"test-session", 1⟩
       line := 0
       character := 0
       text := "exact trivial"
diff --git a/tests/lean/BeamTest/Broker/RocqSmokeTest.lean b/tests/lean/BeamTest/Broker/RocqSmokeTest.lean
index c41cc083..7b601064 100644
--- a/tests/lean/BeamTest/Broker/RocqSmokeTest.lean
+++ b/tests/lean/BeamTest/Broker/RocqSmokeTest.lean
@@ -56,14 +56,14 @@ private def expectSurfacedError (resp : Beam.Broker.Response) : IO Unit := do
   if err.message.trimAscii.isEmpty then
     throw <| IO.userError s!"expected non-empty surfaced Rocq error, got {(toJson resp).compress}"
 
-private def updateVersion
+private def updateSnapshot
     (endpoint : Beam.Broker.Endpoint)
-    (path : String) : IO Nat := do
+    (path : String) : IO Beam.SnapshotRef := do
   let resp ← runClient endpoint {
     payload := .updateFile { backend := .rocq, path }
   }
-  let result ← requireUpdateFileResult s!"rocq update version for {path}" (← expectOk resp)
-  pure result.version
+  let result ← requireUpdateFileResult s!"rocq update snapshot for {path}" (← expectOk resp)
+  pure result.snapshot
 
 def main : IO Unit := do
   let endpoint ← freshTcpEndpoint
@@ -76,15 +76,15 @@ def main : IO Unit := do
       payload := .syncFile { backend := .rocq, path := "Demo.v" }
     }
     expectErrCode unsupportedSync "invalidParams"
-    let demoVersion ← updateVersion endpoint "Demo.v"
-    let semiVersion ← updateVersion endpoint "Semi.v"
-    let errorVersion ← updateVersion endpoint "Error.v"
-    let doneVersion ← updateVersion endpoint "Done.v"
+    let demoSnapshot ← updateSnapshot endpoint "Demo.v"
+    let semiSnapshot ← updateSnapshot endpoint "Semi.v"
+    let errorSnapshot ← updateSnapshot endpoint "Error.v"
+    let doneSnapshot ← updateSnapshot endpoint "Done.v"
     let goals ← expectOk <| ← runClient endpoint {
       payload := .goals {
         backend := .rocq
         path := "Demo.v"
-        version := demoVersion
+        snapshot := demoSnapshot
         line := 2
         character := 8
         mode? := some .after
@@ -97,7 +97,7 @@ def main : IO Unit := do
       payload := .goals {
         backend := .rocq
         path := "Semi.v"
-        version := semiVersion
+        snapshot := semiSnapshot
         line := 2
         character := 3
         mode? := some .before
@@ -111,7 +111,7 @@ def main : IO Unit := do
       payload := .goals {
         backend := .rocq
         path := "Error.v"
-        version := errorVersion
+        snapshot := errorSnapshot
         line := 2
         character := 8
         mode? := some .after
@@ -124,7 +124,7 @@ def main : IO Unit := do
       payload := .goals {
         backend := .rocq
         path := "Error.v"
-        version := errorVersion
+        snapshot := errorSnapshot
         line := 4
         character := 2
         mode? := some .after
@@ -137,7 +137,7 @@ def main : IO Unit := do
       payload := .goals {
         backend := .rocq
         path := "Done.v"
-        version := doneVersion
+        snapshot := doneSnapshot
         line := 3
         character := 0
         mode? := some .before
diff --git a/tests/lean/BeamTest/Broker/SaveStreamTest.lean b/tests/lean/BeamTest/Broker/SaveStreamTest.lean
index ce5403f4..fcb916dd 100644
--- a/tests/lean/BeamTest/Broker/SaveStreamTest.lean
+++ b/tests/lean/BeamTest/Broker/SaveStreamTest.lean
@@ -28,13 +28,13 @@ private def expectNoTrackedLeanDoc (payload : Json) (path : String) : IO Unit :=
 private def expectSyncVerdict
     (label : String)
     (payload : Json)
-    (expectedVersion : Nat)
+    (expectedSnapshot : Beam.SnapshotRef)
     (expectedSaveReady : Bool) : IO Beam.Broker.SyncFileResult := do
   let syncJson ← IO.ofExcept <| payload.getObjVal? "sync"
   let sync ← requireSyncFileResult label syncJson
-  if sync.version != expectedVersion then
+  if sync.snapshot != expectedSnapshot then
     throw <| IO.userError
-      s!"expected {label} sync.version = {expectedVersion}, got {(toJson sync).compress}"
+      s!"expected {label} sync.snapshot = {expectedSnapshot}, got {(toJson sync).compress}"
   if sync.readiness.saveReady != expectedSaveReady then
     throw <| IO.userError
       s!"expected {label} sync.readiness.saveReady = {expectedSaveReady}, got {(toJson sync).compress}"
@@ -68,10 +68,8 @@ def main : IO Unit := do
     }
     let defaultPayload ← expectOk defaultResp
     expectNoReplayDiagnosticsField "default save_olean" defaultPayload
-    let defaultVersion ← IO.ofExcept <| defaultPayload.getObjValAs? Nat "version"
-    if defaultVersion != 1 then
-      throw <| IO.userError s!"expected default save_olean version 1, got {defaultVersion}"
-    let defaultSyncVerdict ← expectSyncVerdict "default save_olean" defaultPayload defaultVersion true
+    let defaultSnapshot ← IO.ofExcept <| defaultPayload.getObjValAs? Beam.SnapshotRef "snapshot"
+    let defaultSyncVerdict ← expectSyncVerdict "default save_olean" defaultPayload defaultSnapshot true
     if defaultSyncVerdict.readiness.blockingErrorCount != 0 then
       throw <| IO.userError
         s!"expected default save_olean sync verdict to be clean, got {(toJson defaultSyncVerdict).compress}"
@@ -94,10 +92,10 @@ def main : IO Unit := do
     }
     let fullPayload ← expectOk fullResp
     expectNoReplayDiagnosticsField "full save_olean" fullPayload
-    let fullVersion ← IO.ofExcept <| fullPayload.getObjValAs? Nat "version"
-    if fullVersion != 2 then
-      throw <| IO.userError s!"expected full save_olean version 2 after a fresh edit, got {fullVersion}"
-    let fullSyncVerdict ← expectSyncVerdict "full save_olean" fullPayload fullVersion true
+    let fullSnapshot ← IO.ofExcept <| fullPayload.getObjValAs? Beam.SnapshotRef "snapshot"
+    if fullSnapshot == defaultSnapshot then
+      throw <| IO.userError s!"expected full save_olean a fresh snapshot after an edit, got {fullSnapshot}"
+    let fullSyncVerdict ← expectSyncVerdict "full save_olean" fullPayload fullSnapshot true
     if fullSyncVerdict.readiness.blockingErrorCount != 0 ||
         fullSyncVerdict.diagnostics.counts.warning == 0 then
       throw <| IO.userError
@@ -122,10 +120,10 @@ def main : IO Unit := do
     }
     let repeatPayload ← expectOk repeatResp
     expectNoReplayDiagnosticsField "unchanged full save_olean" repeatPayload
-    let repeatVersion ← IO.ofExcept <| repeatPayload.getObjValAs? Nat "version"
-    if repeatVersion != 2 then
-      throw <| IO.userError s!"expected unchanged full save_olean version 2, got {repeatVersion}"
-    discard <| expectSyncVerdict "unchanged full save_olean" repeatPayload repeatVersion true
+    let repeatSnapshot ← IO.ofExcept <| repeatPayload.getObjValAs? Beam.SnapshotRef "snapshot"
+    if repeatSnapshot != fullSnapshot then
+      throw <| IO.userError s!"expected unchanged full save_olean to preserve its snapshot, got {repeatSnapshot}"
+    discard <| expectSyncVerdict "unchanged full save_olean" repeatPayload repeatSnapshot true
     let repeatTop := ← requireFileProgress "unchanged full save_olean" repeatResp
     if !repeatTop.done then
       throw <| IO.userError
@@ -189,10 +187,10 @@ def main : IO Unit := do
     if !closeClosed then
       throw <| IO.userError s!"expected close-save payload to report closed = true, got {closePayload.compress}"
     let savedPayload ← IO.ofExcept <| closePayload.getObjVal? "saved"
-    let closeVersion ← IO.ofExcept <| savedPayload.getObjValAs? Nat "version"
-    if closeVersion != 4 then
-      throw <| IO.userError s!"expected close-save saved version 4 after a fresh edit, got {closeVersion}"
-    let closeSyncVerdict ← expectSyncVerdict "full close-save" savedPayload closeVersion true
+    let closeSnapshot ← IO.ofExcept <| savedPayload.getObjValAs? Beam.SnapshotRef "snapshot"
+    if closeSnapshot == fullSnapshot then
+      throw <| IO.userError s!"expected close-save saved a fresh snapshot after an edit, got {closeSnapshot}"
+    let closeSyncVerdict ← expectSyncVerdict "full close-save" savedPayload closeSnapshot true
     if closeSyncVerdict.readiness.blockingErrorCount != 0 ||
         closeSyncVerdict.diagnostics.counts.warning == 0 then
       throw <| IO.userError
diff --git a/tests/lean/BeamTest/Broker/SmokeTest.lean b/tests/lean/BeamTest/Broker/SmokeTest.lean
index 52297a65..c6d194b3 100644
--- a/tests/lean/BeamTest/Broker/SmokeTest.lean
+++ b/tests/lean/BeamTest/Broker/SmokeTest.lean
@@ -17,44 +17,41 @@ namespace BeamTest.Broker.SmokeTest
 open BeamTest.Broker.TestUtil
 open BeamTest.Broker.JsonAssert
 
-private def syncVersion
+private def syncSnapshot
     (endpoint : Beam.Broker.Endpoint)
-    (path : String) : IO Nat := do
+    (path : String) : IO Beam.SnapshotRef := do
   let resp ← runClient endpoint {
     payload := .syncFile { path }
   }
-  let result ← requireSyncFileResult s!"sync version for {path}" (← expectOk resp)
-  pure result.version
+  let result ← requireSyncFileResult s!"sync snapshot for {path}" (← expectOk resp)
+  pure result.snapshot
 
-private def updateVersion
+private def updateSnapshot
     (endpoint : Beam.Broker.Endpoint)
-    (path : String) : IO Nat := do
+    (path : String) : IO Beam.SnapshotRef := do
   let resp ← runClient endpoint {
     payload := .updateFile { path }
   }
-  let result ← requireUpdateFileResult s!"update version for {path}" (← expectOk resp)
-  pure result.version
+  let result ← requireUpdateFileResult s!"update snapshot for {path}" (← expectOk resp)
+  pure result.snapshot
 
-private def expectVersionMismatchData
+private def expectSnapshotMismatchData
     (label : String)
     (resp : Beam.Broker.Response)
-    (expectedVersion acceptedVersion : Nat) : IO Unit := do
+    (expectedSnapshot acceptedSnapshot : Beam.SnapshotRef) : IO Unit := do
   let some err := resp.error?
     | throw <| IO.userError s!"{label}: expected error response, got {(toJson resp).compress}"
   let some data := err.data?
     | throw <| IO.userError s!"{label}: expected error.data, got {(toJson resp).compress}"
   let reason ← IO.ofExcept <| data.getObjValAs? String "reason"
-  if reason != "documentVersionMismatch" then
-    throw <| IO.userError s!"{label}: expected documentVersionMismatch data, got {data.compress}"
-  let expected ← IO.ofExcept <| data.getObjValAs? Nat "expectedVersion"
-  if expected != expectedVersion then
-    throw <| IO.userError s!"{label}: expected expectedVersion={expectedVersion}, got {data.compress}"
-  let accepted ← IO.ofExcept <| data.getObjValAs? Nat "acceptedVersion"
-  if accepted != acceptedVersion then
-    throw <| IO.userError s!"{label}: expected acceptedVersion={acceptedVersion}, got {data.compress}"
-  let current ← IO.ofExcept <| data.getObjValAs? Nat "currentVersion"
-  if current != acceptedVersion then
-    throw <| IO.userError s!"{label}: expected currentVersion={acceptedVersion}, got {data.compress}"
+  if reason != "snapshotMismatch" then
+    throw <| IO.userError s!"{label}: expected snapshotMismatch data, got {data.compress}"
+  let expected ← IO.ofExcept <| data.getObjValAs? Beam.SnapshotRef "expectedSnapshot"
+  if expected != expectedSnapshot then
+    throw <| IO.userError s!"{label}: expected expectedSnapshot={expectedSnapshot}, got {data.compress}"
+  let current ← IO.ofExcept <| data.getObjValAs? Beam.SnapshotRef "currentSnapshot"
+  if current != acceptedSnapshot then
+    throw <| IO.userError s!"{label}: expected currentSnapshot={acceptedSnapshot}, got {data.compress}"
 
 private def runUpdateSmoke
     (endpoint : Beam.Broker.Endpoint)
@@ -68,24 +65,24 @@ private def runUpdateSmoke
     payload := .updateFile { path := relPath }
   }
   let first ← requireUpdateFileResult "initial update_file" (← expectOk firstResp)
-  if first.version != 1 || !first.changed then
-    throw <| IO.userError s!"expected initial update_file version 1 changed=true, got {(toJson first).compress}"
+  if !first.changed then
+    throw <| IO.userError s!"expected initial update_file changed=true, got {(toJson first).compress}"
   let unchangedResp ← runClient endpoint {
     payload := .updateFile { path := relPath }
   }
   let unchanged ← requireUpdateFileResult "unchanged update_file" (← expectOk unchangedResp)
-  if unchanged.version != first.version || unchanged.changed then
-    throw <| IO.userError s!"expected unchanged update_file to preserve version and report changed=false, got {(toJson unchanged).compress}"
+  if unchanged.snapshot != first.snapshot || unchanged.changed then
+    throw <| IO.userError s!"expected unchanged update_file to preserve snapshot and report changed=false, got {(toJson unchanged).compress}"
   let syncResp ← runClient endpoint {
     payload := .syncFile { path := relPath }
   }
   let syncRes ← requireSyncFileResult "sync after update_file" (← expectOk syncResp)
-  if syncRes.version != first.version then
-    throw <| IO.userError s!"expected sync_file after update_file to reuse version {first.version}, got {syncRes.version}"
+  if syncRes.snapshot != first.snapshot then
+    throw <| IO.userError s!"expected sync_file after update_file to reuse snapshot {first.snapshot}, got {syncRes.snapshot}"
   let runAtResp ← runClient endpoint {
     payload := .runAt {
       path := relPath
-      version := first.version
+      snapshot := first.snapshot
       line := 0
       character := 0
       text := "#check Nat"
@@ -93,32 +90,81 @@ private def runUpdateSmoke
   }
   let runAtRes ← expectOk runAtResp
   let .ok true := runAtRes.getObjValAs? Bool "success"
-    | throw <| IO.userError s!"expected run_at with update_file version to succeed, got {runAtRes.compress}"
+    | throw <| IO.userError s!"expected run_at with update_file snapshot to succeed, got {runAtRes.compress}"
 
   IO.FS.writeFile path "def updateSmokeVal : Nat := 2\n"
   let changedResp ← runClient endpoint {
     payload := .updateFile { path := relPath }
   }
   let changed ← requireUpdateFileResult "changed update_file" (← expectOk changedResp)
-  if changed.version != first.version + 1 || !changed.changed then
-    throw <| IO.userError s!"expected changed update_file to bump version and report changed=true, got {(toJson changed).compress}"
+  if changed.snapshot == first.snapshot || !changed.changed then
+    throw <| IO.userError s!"expected changed update_file to bump snapshot and report changed=true, got {(toJson changed).compress}"
   let syncChangedResp ← runClient endpoint {
     payload := .syncFile { path := relPath }
   }
   let syncChanged ← requireSyncFileResult "sync after changed update_file" (← expectOk syncChangedResp)
-  if syncChanged.version != changed.version then
-    throw <| IO.userError s!"expected sync_file after changed update_file to reuse version {changed.version}, got {syncChanged.version}"
+  if syncChanged.snapshot != changed.snapshot then
+    throw <| IO.userError s!"expected sync_file after changed update_file to reuse snapshot {changed.snapshot}, got {syncChanged.snapshot}"
   let staleRunAtResp ← runClient endpoint {
     payload := .runAt {
       path := relPath
-      version := first.version
+      snapshot := first.snapshot
       line := 0
       character := 0
       text := "#check Nat"
     }
   }
   expectErrCode staleRunAtResp "contentModified"
-  expectVersionMismatchData "stale run_at" staleRunAtResp first.version changed.version
+  expectSnapshotMismatchData "stale run_at" staleRunAtResp first.snapshot changed.snapshot
+
+private def runReopenedSnapshotSmoke
+    (endpoint : Beam.Broker.Endpoint)
+    (root : System.FilePath) : IO Unit := do
+  let dir := root / ".tmp" / s!"beam-snapshot-reopen-{← IO.monoNanosNow}"
+  IO.FS.createDirAll dir
+  let path := dir / "Snapshot.lean"
+  let relPath := Beam.pathRelativeToRootOrSelf root path
+  IO.FS.writeFile path "example : 1 = 1 := by\n  rfl\n"
+  let before ← updateSnapshot endpoint relPath
+  let probe := fun snapshot => runClient endpoint {
+    payload := .runAt {
+      path := relPath
+      snapshot
+      line := 1
+      character := 2
+      text := "rfl"
+    }
+  }
+  let initial ← expectOk (← probe before)
+  requireJsonBool "initial snapshot probe" "success" true initial
+  -- Inserting another valid proof leaves the old coordinate valid but moves the intended target.
+  IO.FS.writeFile path "example : 2 = 2 := by\n  rfl\n\nexample : 1 = 1 := by\n  rfl\n"
+  let refreshed ← requireSyncFileResult "refresh replacement snapshot" <| ← expectOk <| ← runClient endpoint {
+    payload := .refreshFile { path := relPath }
+  }
+  let current ← expectOk (← probe refreshed.snapshot)
+  requireJsonBool "replacement snapshot probe" "success" true current
+  let relocated ← expectOk <| ← runClient endpoint {
+    payload := .runAt {
+      path := relPath, snapshot := refreshed.snapshot, line := 4, character := 2, text := "rfl"
+    }
+  }
+  requireJsonBool "resolved target after insertion" "success" true relocated
+  let stale ← probe before
+  expectErrCode stale "contentModified"
+  expectSnapshotMismatchData "refresh rejects old snapshot" stale before refreshed.snapshot
+  require "refresh replaces snapshot" (before != refreshed.snapshot)
+  discard <| expectOk <| ← runClient endpoint { payload := .close { path := relPath } }
+  let reopened ← updateSnapshot endpoint relPath
+  require "close/reopen replaces snapshot" (reopened != refreshed.snapshot)
+  expectErrCode (← probe refreshed.snapshot) "contentModified"
+  requireJsonBool "reopened snapshot works" "success" true (← expectOk <| ← probe reopened)
+  let other := dir / "Other.lean"
+  IO.FS.writeFile other (← IO.FS.readFile path)
+  let otherSnapshot ← updateSnapshot endpoint (Beam.pathRelativeToRootOrSelf root other)
+  require "identical files have distinct snapshots" (otherSnapshot != reopened)
+  expectErrCode (← probe otherSnapshot) "contentModified"
+  require "unchanged update preserves snapshot" ((← updateSnapshot endpoint relPath) == reopened)
 
 private def runSyncSmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
@@ -130,8 +176,6 @@ private def runSyncSmoke
     clientRequestId? := syncRequestId
   }
   let syncRes ← requireSyncFileResult "sync_file" (← expectOk syncResp)
-  if syncRes.version != 1 then
-    throw <| IO.userError s!"expected sync_file version 1, got {syncRes.version}"
   if !syncRes.readiness.saveReady then
     throw <| IO.userError
       s!"expected sync_file saveReady = true for clean module, got {(toJson syncRes).compress}"
@@ -150,8 +194,8 @@ private def runSyncSmoke
     payload := .syncFile { path := "tests/scenario/docs/CommandA.lean" }
   }
   let syncResAgain ← requireSyncFileResult "unchanged sync_file" (← expectOk syncRespAgain)
-  if syncResAgain.version != 1 then
-    throw <| IO.userError s!"expected unchanged sync_file version 1, got {syncResAgain.version}"
+  if syncResAgain.snapshot != syncRes.snapshot then
+    throw <| IO.userError s!"expected unchanged sync_file to preserve its snapshot, got {syncResAgain.snapshot}"
   let syncTopAgain := ← requireFileProgress "unchanged sync_file" syncRespAgain
   if !syncTopAgain.done then
     throw <| IO.userError s!"expected unchanged sync_file fileProgress.done = true, got {(toJson syncTopAgain).compress}"
@@ -163,8 +207,8 @@ private def runSyncSmoke
     clientRequestId? := refreshRequestId
   }
   let refreshRes ← requireSyncFileResult "refresh_file" (← expectOk refreshResp)
-  if refreshRes.version != 1 then
-    throw <| IO.userError s!"expected refresh_file to reopen version 1, got {refreshRes.version}"
+  if refreshRes.snapshot == syncRes.snapshot then
+    throw <| IO.userError s!"expected refresh_file to return a fresh snapshot, got {refreshRes.snapshot}"
   let refreshTop := ← requireFileProgress "refresh_file" refreshResp
   if !refreshTop.done then
     throw <| IO.userError s!"expected top-level refresh_file fileProgress.done = true, got {(toJson refreshTop).compress}"
@@ -183,8 +227,6 @@ private def runErrorOnlySyncSmoke
     payload := .syncFile { path := errorPath.toString }
   }
   let errorRes ← requireSyncFileResult "error-only sync_file" (← expectOk errorResp)
-  if errorRes.version != 1 then
-    throw <| IO.userError s!"expected error-only sync_file version 1, got {errorRes.version}"
   if errorRes.readiness.saveReady then
     throw <| IO.userError
       s!"expected error-only sync_file saveReady = false, got {(toJson errorRes).compress}"
@@ -257,11 +299,11 @@ private def runInteractiveOnlyDiagnosticSmoke
 private def runTodoThenSyncDiagnosticSummarySmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let path := "tests/scenario/docs/InteractiveOnlyDiagnostic.lean"
-  let version ← syncVersion endpoint path
+  let snapshot ← syncSnapshot endpoint path
   let todoResp ← runClient endpoint {
     payload := .todo {
       path
-      version
+      snapshot
       line := 0
       character := 0
       endLine := 22
@@ -298,11 +340,11 @@ private def runTodoThenSyncDiagnosticSummarySmoke
 private def runTodoCodeActionResolveSmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let path := BeamTest.Fixtures.TodoFixture.codeActionRepoPath.toString
-  let version ← updateVersion endpoint path
+  let snapshot ← updateSnapshot endpoint path
   let todoResp ← runClient endpoint {
     payload := .todo {
       path
-      version
+      snapshot
       line := BeamTest.Fixtures.TodoFixture.codeActionLine
       character := BeamTest.Fixtures.TodoFixture.codeActionStartCharacter
       endLine := BeamTest.Fixtures.TodoFixture.codeActionLine
@@ -321,12 +363,12 @@ private def runTodoCodeActionResolveSmoke
     | throw <| IO.userError <|
       s!"todo/code_action_resolve composition: expected embedded codeAction, got {(toJson actionItem).compress}"
   let resolveResp ← runClient endpoint {
-    payload := .codeActionResolve { path, version, codeAction := action }
+    payload := .codeActionResolve { path, snapshot, codeAction := action }
   }
   let resolved : Beam.Broker.CodeActionResolveResult ← IO.ofExcept <| fromJson? (← expectOk resolveResp)
-  if resolved.version != version then
+  if resolved.snapshot != snapshot then
     throw <| IO.userError
-      s!"todo/code_action_resolve composition: expected resolved version {version}, got {resolved.version}"
+      s!"todo/code_action_resolve composition: expected resolved snapshot {snapshot}, got {resolved.snapshot}"
   if resolved.codeAction.title != action.title then
     throw <| IO.userError
       s!"todo/code_action_resolve composition: expected resolved action title {action.title}, got {resolved.codeAction.title}"
@@ -336,17 +378,17 @@ private def runTodoCodeActionResolveSmoke
   discard <| requireFileProgress "code_action_resolve" resolveResp
 
   let staleResp ← runClient endpoint {
-    payload := .codeActionResolve { path, version := 0, codeAction := action }
+    payload := .codeActionResolve { path, snapshot := { session := "stale", revision := 1 }, codeAction := action }
   }
   expectErrCode staleResp "contentModified"
-  expectVersionMismatchData "stale code_action_resolve" staleResp 0 version
+  expectSnapshotMismatchData "stale code_action_resolve" staleResp { session := "stale", revision := 1 } snapshot
 
   let otherPath := "tests/scenario/docs/CommandA.lean"
-  let otherVersion ← updateVersion endpoint otherPath
+  let otherSnapshot ← updateSnapshot endpoint otherPath
   let mismatchedSourceResp ← runClient endpoint {
     payload := .codeActionResolve {
       path := otherPath
-      version := otherVersion
+      snapshot := otherSnapshot
       codeAction := action
     }
   }
@@ -394,11 +436,11 @@ private def runPartialProgressSmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let partialRequestId := some "smoke-partial"
   let path := "tests/scenario/docs/PartialProgress.lean"
-  let version ← syncVersion endpoint path
+  let snapshot ← syncSnapshot endpoint path
   let (partialResp, partialEvents) ← runClientWithProgress endpoint {
     payload := .runAt {
       path
-      version
+      snapshot
       line := 7
       character := 2
       text := "#check partialProgressAnchor"
@@ -409,11 +451,11 @@ private def runPartialProgressSmoke
   let .ok true := partialRes.getObjValAs? Bool "success" | throw <| IO.userError "partial run_at did not succeed"
   let partialProgress := ← requireFileProgress "partial run_at" partialResp
   if !partialProgress.done then
-    throw <| IO.userError s!"expected versioned run_at fileProgress.done = true after sync, got {(toJson partialProgress).compress}"
+    throw <| IO.userError s!"expected snapshoted run_at fileProgress.done = true after sync, got {(toJson partialProgress).compress}"
   if let some partialLast := partialEvents.back? then
     expectClientRequestId "partial run_at progress" partialLast.clientRequestId? partialRequestId
     if !partialLast.progress.done then
-      throw <| IO.userError s!"expected final streamed versioned run_at progress to be complete, got {(toJson partialLast.progress).compress}"
+      throw <| IO.userError s!"expected final streamed snapshoted run_at progress to be complete, got {(toJson partialLast.progress).compress}"
 
 private def runConcurrentSmoke
     (endpoint : Beam.Broker.Endpoint)
@@ -422,7 +464,7 @@ private def runConcurrentSmoke
   let concurrentHoverId := some "concurrent-hover"
   let slowSyncPath ← writeSlowSyncFile root
   let hoverPath := "tests/scenario/docs/CommandA.lean"
-  let hoverVersion ← updateVersion endpoint hoverPath
+  let hoverSnapshot ← updateSnapshot endpoint hoverPath
   let syncTask ← IO.asTask (prio := Task.Priority.dedicated) <| runClientWithProgress endpoint {
     payload := .syncFile {
       path := slowSyncPath.toString
@@ -434,7 +476,7 @@ private def runConcurrentSmoke
   let (hoverResp, hoverEvents) ← runClientWithProgress endpoint {
     payload := .hover {
       path := hoverPath
-      version := hoverVersion
+      snapshot := hoverSnapshot
       line := 0
       character := 4
     }
@@ -456,13 +498,13 @@ private def runConcurrentSmoke
 private def runRequestAndGoalsSmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let commandPath := "tests/scenario/docs/CommandA.lean"
-  let commandVersion ← updateVersion endpoint commandPath
+  let commandSnapshot ← updateSnapshot endpoint commandPath
   let proofPath := "tests/scenario/docs/SimpleProof.lean"
-  let proofVersion ← updateVersion endpoint proofPath
+  let proofSnapshot ← updateSnapshot endpoint proofPath
   let cmdResp ← runClient endpoint {
     payload := .runAt {
       path := commandPath
-      version := commandVersion
+      snapshot := commandSnapshot
       line := 0
       character := 2
       text := "#check answerA"
@@ -474,7 +516,7 @@ private def runRequestAndGoalsSmoke
   let hoverResp ← runClient endpoint {
     payload := .hover {
       path := commandPath
-      version := commandVersion
+      snapshot := commandSnapshot
       line := 0
       character := 4
     }
@@ -486,11 +528,11 @@ private def runRequestAndGoalsSmoke
   expectStringContains "hover markdown" hoverValue "answerA : Nat"
 
   let signaturePath := "tests/scenario/docs/SignatureHelp.lean"
-  let signatureVersion ← updateVersion endpoint signaturePath
+  let signatureSnapshot ← updateSnapshot endpoint signaturePath
   let signatureHelpResp ← runClient endpoint {
     payload := .signatureHelp {
       path := signaturePath
-      version := signatureVersion
+      snapshot := signatureSnapshot
       line := 4
       character := 12
     }
@@ -502,7 +544,7 @@ private def runRequestAndGoalsSmoke
   let definitionResp ← runClient endpoint {
     payload := .definition {
       path := commandPath
-      version := commandVersion
+      snapshot := commandSnapshot
       line := 0
       character := 4
     }
@@ -514,7 +556,7 @@ private def runRequestAndGoalsSmoke
   let referencesResp ← runClient endpoint {
     payload := .references {
       path := commandPath
-      version := commandVersion
+      snapshot := commandSnapshot
       line := 0
       character := 4
       includeDeclaration? := some true
@@ -525,7 +567,7 @@ private def runRequestAndGoalsSmoke
   expectStringContains "references result" references.compress "CommandA.lean"
 
   let documentSymbolsResp ← runClient endpoint {
-    payload := .documentSymbols { path := commandPath, version := commandVersion }
+    payload := .documentSymbols { path := commandPath, snapshot := commandSnapshot }
   }
   let documentSymbols ← expectOk documentSymbolsResp
   discard <| requireFileProgress "document symbols" documentSymbolsResp
@@ -547,7 +589,7 @@ private def runRequestAndGoalsSmoke
   let goalsPrevResp ← runClient endpoint {
     payload := .goals {
       path := proofPath
-      version := proofVersion
+      snapshot := proofSnapshot
       line := 1
       character := 2
       mode? := some .before
@@ -566,7 +608,7 @@ private def runRequestAndGoalsSmoke
   let goalsAfterResp ← runClient endpoint {
     payload := .goals {
       path := proofPath
-      version := proofVersion
+      snapshot := proofSnapshot
       line := 1
       character := 2
       mode? := some .after
@@ -581,7 +623,7 @@ private def runRequestAndGoalsSmoke
   let speculativeGoalsResp ← runClient endpoint {
     payload := .goals {
       path := proofPath
-      version := proofVersion
+      snapshot := proofSnapshot
       line := 1
       character := 2
       text? := some "exact trivial"
@@ -600,11 +642,11 @@ private def runCancelSmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let slowRequestId := some "cancel-slow"
   let slowPath := "tests/scenario/docs/SlowPoll.lean"
-  let slowVersion ← updateVersion endpoint slowPath
+  let slowSnapshot ← updateSnapshot endpoint slowPath
   let slowTask ← IO.asTask (prio := Task.Priority.dedicated) <| runClientWithProgress endpoint {
     payload := .runAt {
       path := slowPath
-      version := slowVersion
+      snapshot := slowSnapshot
       line := 25
       character := 2
       text := "poll_sleep_cmd"
@@ -621,11 +663,11 @@ private def runCancelSmoke
   expectProgressIds "cancelled run_at progress" slowEvents slowRequestId
 
   let commandPath := "tests/scenario/docs/CommandA.lean"
-  let commandVersion ← updateVersion endpoint commandPath
+  let commandSnapshot ← updateSnapshot endpoint commandPath
   let postCancelHoverResp ← runClient endpoint {
     payload := .hover {
       path := commandPath
-      version := commandVersion
+      snapshot := commandSnapshot
       line := 0
       character := 4
     }
@@ -639,11 +681,11 @@ private def runWorkerExitSmoke
     (endpoint : Beam.Broker.Endpoint)
     (root : System.FilePath) : IO Unit := do
   let branchPath := "tests/scenario/docs/BranchProof.lean"
-  let branchVersion ← updateVersion endpoint branchPath
+  let branchSnapshot ← updateSnapshot endpoint branchPath
   let handleSeed ← expectOk <| ← runClient endpoint {
     payload := .runAt {
       path := branchPath
-      version := branchVersion
+      snapshot := branchSnapshot
       line := 0
       character := 27
       text := "constructor"
@@ -655,11 +697,11 @@ private def runWorkerExitSmoke
 
   let workerExitRequestId := some "worker-exit-slow"
   let slowPath := "tests/scenario/docs/SlowPoll.lean"
-  let slowVersion ← updateVersion endpoint slowPath
+  let slowSnapshot ← updateSnapshot endpoint slowPath
   let slowTask ← IO.asTask (prio := Task.Priority.dedicated) <| runClientWithProgress endpoint {
     payload := .runAt {
       path := slowPath
-      version := slowVersion
+      snapshot := slowSnapshot
       line := 25
       character := 2
       text := "poll_sleep_cmd"
@@ -678,12 +720,24 @@ private def runWorkerExitSmoke
     throw <| IO.userError s!"expected worker-exit stderr diagnostic, got {(toJson slowResp).compress}"
   expectProgressIds "worker-exit run_at progress" slowEvents workerExitRequestId
 
+  let restartedSnapshot ← updateSnapshot endpoint branchPath
+  require "backend restart replaces snapshot" (restartedSnapshot != branchSnapshot)
+  expectErrCode (← runClient endpoint {
+    payload := .runAt {
+      path := branchPath, snapshot := branchSnapshot, line := 0, character := 27, text := "constructor"
+    }
+  }) "contentModified"
+  requireJsonBool "restarted snapshot works" "success" true <| ← expectOk <| ← runClient endpoint {
+    payload := .runAt {
+      path := branchPath, snapshot := restartedSnapshot, line := 0, character := 27, text := "constructor"
+    }
+  }
   let commandPath := "tests/scenario/docs/CommandA.lean"
-  let commandVersion ← updateVersion endpoint commandPath
+  let commandSnapshot ← updateSnapshot endpoint commandPath
   let restartHoverResp ← runClient endpoint {
     payload := .hover {
       path := commandPath
-      version := commandVersion
+      snapshot := commandSnapshot
       line := 0
       character := 4
     }
@@ -705,11 +759,11 @@ private def runWorkerExitSmoke
 private def runHandleSmoke
     (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let branchPath := "tests/scenario/docs/BranchProof.lean"
-  let branchVersion ← updateVersion endpoint branchPath
+  let branchSnapshot ← updateSnapshot endpoint branchPath
   let proofRes ← expectOk <| ← runClient endpoint {
     payload := .runAt {
       path := branchPath
-      version := branchVersion
+      snapshot := branchSnapshot
       line := 0
       character := 27
       text := "constructor"
@@ -764,9 +818,7 @@ private def runSaveAndStatsSmoke
     payload := .saveOlean { path := "tests/lean/BeamTest/Fixtures/Deps/DepA.lean" }
   }
   let savePayload ← expectOk saveResp
-  let saveVersion ← IO.ofExcept <| savePayload.getObjValAs? Nat "version"
-  if saveVersion != 1 then
-    throw <| IO.userError s!"expected save_olean version = 1, got {saveVersion}"
+  discard <| IO.ofExcept <| savePayload.getObjValAs? Beam.SnapshotRef "snapshot"
   let saveHash ← IO.ofExcept <| savePayload.getObjValAs? String "sourceHash"
   if saveHash.isEmpty then
     throw <| IO.userError "expected save_olean sourceHash to be present"
@@ -855,12 +907,21 @@ private def runWorkspaceLifecycleSmoke
     workspaceId? := some workspaceId
   })
   let update ← requireUpdateFileResult "named workspace update" updatePayload
-  if update.version != 1 then
-    throw <| IO.userError s!"expected named workspace update version 1, got {update.version}"
+  let wrongFile ← runClient endpoint {
+    payload := .runAt {
+      path := "GoalSmoke.lean", snapshot := update.snapshot, line := 1, character := 2, text := "trivial"
+    }
+    workspaceId? := some workspaceId
+  }
+  expectErrCode wrongFile "contentModified"
+  let proofUpdate ← requireUpdateFileResult "proof snapshot" <| ← expectOk <| ← runClient endpoint {
+    payload := .updateFile { path := "GoalSmoke.lean" }
+    workspaceId? := some workspaceId
+  }
   let proofHandleSeed ← expectOk <| ← runClient endpoint {
     payload := .runAt {
       path := "GoalSmoke.lean"
-      version := update.version
+      snapshot := proofUpdate.snapshot
       line := 1
       character := 2
       text := "trivial"
@@ -901,10 +962,17 @@ private def runWorkspaceLifecycleSmoke
     workspaceId? := some workspaceId
   })
   let updateAfterReset ← requireUpdateFileResult "named workspace update after reset" updateAfterResetPayload
+  require "workspace reset replaces snapshot" (updateAfterReset.snapshot != proofUpdate.snapshot)
+  expectErrCode (← runClient endpoint {
+    payload := .runAt {
+      path := "GoalSmoke.lean", snapshot := proofUpdate.snapshot, line := 1, character := 2, text := "trivial"
+    }
+    workspaceId? := some workspaceId
+  }) "contentModified"
   let postResetHandleSeed ← expectOk <| ← runClient endpoint {
     payload := .runAt {
       path := "GoalSmoke.lean"
-      version := updateAfterReset.version
+      snapshot := updateAfterReset.snapshot
       line := 1
       character := 2
       text := "trivial"
@@ -965,6 +1033,36 @@ private def runWorkspaceLifecycleSmoke
     workspaceId? := some workspaceId
   }
   expectErrCode droppedEnsure "invalidParams"
+  discard <| expectOk <| ← runClient endpoint {
+    payload := .initWorkspace {
+      root := otherRoot.toString
+      lean? := some { command := leanCmd, plugin := plugin.toString }
+    }
+    workspaceId? := some workspaceId
+  }
+  let recreated ← requireUpdateFileResult "recreated workspace snapshot" <| ← expectOk <| ← runClient endpoint {
+    payload := .updateFile { path := "GoalSmoke.lean" }
+    workspaceId? := some workspaceId
+  }
+  require "workspace recreation reuses the native revision in this regression"
+    (recreated.snapshot.revision == updateAfterReset.snapshot.revision)
+  require "workspace recreation replaces snapshot" (recreated.snapshot != updateAfterReset.snapshot)
+  for snapshot in [proofUpdate.snapshot, updateAfterReset.snapshot] do
+    expectErrCode (← runClient endpoint {
+      payload := .runAt {
+        path := "GoalSmoke.lean", snapshot, line := 1, character := 2, text := "trivial"
+      }
+      workspaceId? := some workspaceId
+    }) "contentModified"
+  requireJsonBool "recreated workspace snapshot works" "success" true <| ← expectOk <| ← runClient endpoint {
+    payload := .runAt {
+      path := "GoalSmoke.lean", snapshot := recreated.snapshot, line := 1, character := 2, text := "trivial"
+    }
+    workspaceId? := some workspaceId
+  }
+  discard <| expectOk <| ← runClient endpoint {
+    Beam.Broker.Request.dropWorkspace with workspaceId? := some workspaceId
+  }
 
 private def runInitialWorkspaceDropDebugPayloadSmoke (endpoint : Beam.Broker.Endpoint) : IO Unit := do
   let drop ← expectOk (← runClient endpoint {
@@ -991,6 +1089,7 @@ def smokeMain : IO Unit := do
   try
     waitForBrokerReadyForRoot endpoint root
     discard <| expectOk (← runClient endpoint Beam.Broker.Request.ensure)
+    runReopenedSnapshotSmoke endpoint root
     runWorkspaceLifecycleSmoke endpoint otherRoot plugin leanCmd
     runUpdateSmoke endpoint root
     runSyncSmoke endpoint
diff --git a/tests/lean/BeamTest/Broker/StreamContractTest.lean b/tests/lean/BeamTest/Broker/StreamContractTest.lean
index c2c82c89..dca2b64b 100644
--- a/tests/lean/BeamTest/Broker/StreamContractTest.lean
+++ b/tests/lean/BeamTest/Broker/StreamContractTest.lean
@@ -44,14 +44,14 @@ private def expectTodoKindOnly
     throw <| IO.userError s!"expected {label} to contain only todo kind {kind.key}, got {(toJson result).compress}"
   pure item
 
-private def syncVersion
+private def syncSnapshot
     (endpoint : Beam.Broker.Endpoint)
-    (path : String) : IO Nat := do
+    (path : String) : IO Beam.SnapshotRef := do
   let resp ← runClient endpoint {
     payload := .syncFile { path }
   }
-  let result ← requireSyncFileResult s!"sync version for {path}" (← expectOk resp)
-  pure result.version
+  let result ← requireSyncFileResult s!"sync snapshot for {path}" (← expectOk resp)
+  pure result.snapshot
 
 private partial def waitForBrokerExit
     (broker : IO.Process.Child nullBrokerStdio)
@@ -132,11 +132,11 @@ def main : IO Unit := do
         throw <| IO.userError s!"daemon root mismatch was classified as {repr status}"
     discard <| expectOk (← runClient endpoint Beam.Broker.Request.ensure)
 
-    let todoVersion ← syncVersion endpoint BeamTest.Fixtures.TodoFixture.brokerPath
+    let todoSnapshot ← syncSnapshot endpoint BeamTest.Fixtures.TodoFixture.brokerPath
     let todoMessages ← requireSuccessStream "todo" <| ← runBrokerStream endpoint {
       payload := .todo {
         path := BeamTest.Fixtures.TodoFixture.brokerPath
-        version := todoVersion
+        snapshot := todoSnapshot
         line := BeamTest.Fixtures.TodoFixture.startLine
         character := BeamTest.Fixtures.TodoFixture.startCharacter
         endLine := BeamTest.Fixtures.TodoFixture.endLine
@@ -168,8 +168,6 @@ def main : IO Unit := do
     let syncPayload ← expectOk syncResp
     expectNoReplayDiagnosticsField "sync_file" syncPayload
     let syncResult ← requireSyncFileResult "sync_file" syncPayload
-    if syncResult.version != 1 then
-      throw <| IO.userError s!"expected sync_file version 1, got {syncResult.version}"
     if !syncResult.readiness.saveReady then
       throw <| IO.userError s!"expected sync_file saveReady = true, got {(toJson syncResult).compress}"
     if syncResult.readiness.blockingErrorCount != 0 then
@@ -211,9 +209,9 @@ def main : IO Unit := do
     let saveResp ← requireFinalStreamResponse "save_olean" saveMessages
     let savePayload ← expectOk saveResp
     expectNoReplayDiagnosticsField "save_olean" savePayload
-    let saveVersion ← IO.ofExcept <| savePayload.getObjValAs? Nat "version"
-    if saveVersion != 2 then
-      throw <| IO.userError s!"expected save_olean version 2, got {saveVersion}"
+    let saveSnapshot ← IO.ofExcept <| savePayload.getObjValAs? Beam.SnapshotRef "snapshot"
+    if saveSnapshot == syncResult.snapshot then
+      throw <| IO.userError s!"expected save_olean a fresh snapshot, got {saveSnapshot}"
     let saveDiagnostics ← requireAnyStreamDiagnostics "save_olean" saveMessages
     expectNonErrorDiagnosticsForPath "save_olean" "SaveSmoke/B.lean" saveDiagnostics
 
@@ -232,9 +230,9 @@ def main : IO Unit := do
     if !closed then
       throw <| IO.userError s!"expected close-save payload to report closed = true, got {closePayload.compress}"
     let savedPayload ← IO.ofExcept <| closePayload.getObjVal? "saved"
-    let closeVersion ← IO.ofExcept <| savedPayload.getObjValAs? Nat "version"
-    if closeVersion != 3 then
-      throw <| IO.userError s!"expected close-save saved version 3, got {closeVersion}"
+    let closeSnapshot ← IO.ofExcept <| savedPayload.getObjValAs? Beam.SnapshotRef "snapshot"
+    if closeSnapshot == saveSnapshot then
+      throw <| IO.userError s!"expected close-save saved a fresh snapshot, got {closeSnapshot}"
     let closeDiagnostics ← requireAnyStreamDiagnostics "close-save" closeMessages
     expectNonErrorDiagnosticsForPath "close-save" "SaveSmoke/B.lean" closeDiagnostics
 
diff --git a/tests/lean/BeamTest/Broker/StreamDedupTest.lean b/tests/lean/BeamTest/Broker/StreamDedupTest.lean
index c386a61c..6e265637 100644
--- a/tests/lean/BeamTest/Broker/StreamDedupTest.lean
+++ b/tests/lean/BeamTest/Broker/StreamDedupTest.lean
@@ -146,6 +146,7 @@ private def fakeSessionWithSyncedDoc
     root
     epoch := 1
     sessionToken := "fake-run-at-session"
+    nextDocumentVersion := version + 1
     proc
     stdin := IO.FS.Stream.ofHandle proc.stdin
     stdout := IO.FS.Stream.ofHandle proc.stdout
@@ -194,7 +195,7 @@ def checkRunAtStreamsSetupDiagnostics : IO Unit := do
     let resp ← server.dispatchRequest {
       payload := .runAt {
         path := "Tracked.lean"
-        version := 1
+        snapshot := ⟨session.sessionToken, 1⟩
         line := 0
         character := 2
         text := "#check tracked"
diff --git a/tests/lean/BeamTest/Broker/SyncConcurrencyProbe.lean b/tests/lean/BeamTest/Broker/SyncConcurrencyProbe.lean
index c1bf042e..8af760bc 100644
--- a/tests/lean/BeamTest/Broker/SyncConcurrencyProbe.lean
+++ b/tests/lean/BeamTest/Broker/SyncConcurrencyProbe.lean
@@ -148,7 +148,7 @@ private def runSyncOutcome
                 ok := true
                 saveReady? := some result.readiness.saveReady
                 errorCount? := some result.readiness.blockingErrorCount
-                detail := s!"ok version={result.version} saveReady={result.readiness.saveReady} elapsedMs={elapsedMs}"
+                detail := s!"ok snapshot={result.snapshot} saveReady={result.readiness.saveReady} elapsedMs={elapsedMs}"
               }
           | .error err =>
               pure {
diff --git a/tests/lean/BeamTest/Broker/SyncResultTest.lean b/tests/lean/BeamTest/Broker/SyncResultTest.lean
index c7527c48..0eb31ff1 100644
--- a/tests/lean/BeamTest/Broker/SyncResultTest.lean
+++ b/tests/lean/BeamTest/Broker/SyncResultTest.lean
@@ -53,9 +53,9 @@ private def checkFirstSyncResult : IO Unit := do
     saveReady := true
     saveReadyReason := "ok"
   }
-  let result := mkSyncFileResult "Demo.lean" 1 #[warning] readiness
+  let result := mkSyncFileResult "Demo.lean" ⟨"test-session", 1⟩ #[warning] readiness
 
-  require "first sync path and version" (result.path == "Demo.lean" && result.version == 1)
+  require "first sync path and snapshot" (result.path == "Demo.lean" && result.snapshot == ⟨"test-session", 1⟩)
   require "first sync records warning count"
     (result.diagnostics.counts.warning == 1 && result.diagnostics.counts.total == 1)
   require "first sync readiness is current verdict"
@@ -70,7 +70,7 @@ private def checkCurrentCountsAndReadinessEvidence : IO Unit := do
     blockingDiagnostics := #[blockingEvidence added]
     blockingCommandMessages := #[commandEvidence "new error"]
   }
-  let result := mkSyncFileResult "Demo.lean" 3 #[duplicate, duplicate, added] readiness
+  let result := mkSyncFileResult "Demo.lean" ⟨"test-session", 3⟩ #[duplicate, duplicate, added] readiness
 
   require "duplicate diagnostic current counts"
     (result.diagnostics.counts.warning == 2 &&
@@ -90,7 +90,7 @@ private def checkEffectiveSeverityCounts : IO Unit := do
     saveReadyReason := "documentErrors"
     blockingDiagnostics := #[blockingEvidence currentDiagnostic]
   }
-  let result := mkSyncFileResult "Demo.lean" 5 #[currentDiagnostic] readiness
+  let result := mkSyncFileResult "Demo.lean" ⟨"test-session", 5⟩ #[currentDiagnostic] readiness
 
   require "effective severity counts incomplete-barrier diagnostic as error"
     (result.diagnostics.counts.error == 1 &&
@@ -102,7 +102,7 @@ private def checkDiagnosticErrorsDoNotOverrideReadiness : IO Unit := do
     saveReady := true
     saveReadyReason := "ok"
   }
-  let result := mkSyncFileResult "Demo.lean" 6 #[interactiveDiagnostic] readiness
+  let result := mkSyncFileResult "Demo.lean" ⟨"test-session", 6⟩ #[interactiveDiagnostic] readiness
 
   require "diagnostic severity counts report current Lean diagnostics"
     (result.diagnostics.counts.error == 1 &&
@@ -123,7 +123,7 @@ private def checkSaveBlockingEvidenceProjection : IO Unit := do
     blockingDiagnostics := #[blockingEvidence blockingDiagnostic]
     blockingCommandMessages := #[commandEvidence "save-blocking command message"]
   }
-  let result := mkSyncFileResult "Demo.lean" 7 #[blockingDiagnostic] readiness
+  let result := mkSyncFileResult "Demo.lean" ⟨"test-session", 7⟩ #[blockingDiagnostic] readiness
 
   require "save-blocking evidence appears in readiness result"
     (result.readiness.blockingDiagnostics.size == 1 &&
diff --git a/tests/lib/beam-wrapper-common.sh b/tests/lib/beam-wrapper-common.sh
index ffb1f012..b9cb3c10 100644
--- a/tests/lib/beam-wrapper-common.sh
+++ b/tests/lib/beam-wrapper-common.sh
@@ -142,7 +142,7 @@ json_file_array_len() {
   BEAM_JSON_PAYLOAD="$(cat "$payload_file")" read_json_array_len "$field"
 }
 
-beam_wrapper_command_version() {
+beam_wrapper_command_snapshot() {
   local kind="$1"
   shift
   local label="$1"
@@ -157,28 +157,28 @@ beam_wrapper_command_version() {
     printf '%s\n' "$out" >&2
     return 1
   fi
-  local version
-  version="$(json_text_field "$out" result.version)"
-  case "$version" in
-    ""|*[!0-9]*)
-      echo "expected $label $kind response to include numeric result.version" >&2
+  local snapshot
+  snapshot="$(json_text_field "$out" result.snapshot)"
+  case "$snapshot" in
+    "")
+      echo "expected $label $kind response to include a nonempty result.snapshot token" >&2
       printf '%s\n' "$out" >&2
       return 1
       ;;
   esac
-  printf '%s\n' "$version"
+  printf '%s\n' "$snapshot"
 }
 
-beam_wrapper_sync_version() {
+beam_wrapper_sync_snapshot() {
   local label="$1"
   shift
-  beam_wrapper_command_version sync "$label" "$@"
+  beam_wrapper_command_snapshot sync "$label" "$@"
 }
 
-beam_wrapper_update_version() {
+beam_wrapper_update_snapshot() {
   local label="$1"
   shift
-  beam_wrapper_command_version update "$label" "$@"
+  beam_wrapper_command_snapshot update "$label" "$@"
 }
 
 print_json_file_assertion_context() {
diff --git a/tests/mcp-modern-sdk-client.mjs b/tests/mcp-modern-sdk-client.mjs
index 5f58c5d5..cfa574d5 100755
--- a/tests/mcp-modern-sdk-client.mjs
+++ b/tests/mcp-modern-sdk-client.mjs
@@ -138,7 +138,7 @@ try {
     ),
     "lean_sync",
   );
-  require(typeof sync.version === "number", `lean_sync omitted its document version: ${JSON.stringify(sync)}`);
+  require(typeof sync.snapshot === "string", `lean_sync omitted its source snapshot: ${JSON.stringify(sync)}`);
   require(progress.length > 0, "the SDK did not receive lean_sync progress notifications");
   for (let index = 1; index < progress.length; index += 1) {
     require(
diff --git a/tests/test-beam-fast.sh b/tests/test-beam-fast.sh
index 7e263c40..d51e4518 100644
--- a/tests/test-beam-fast.sh
+++ b/tests/test-beam-fast.sh
@@ -437,9 +437,9 @@ tools = request({"jsonrpc": "2.0", "id": 2, "method": "tools/list"})
 server_version = request({"jsonrpc": "2.0", "id": 7, "method": "tools/call", "params": {"name": "beam_version", "arguments": {}}})
 update = request({"jsonrpc": "2.0", "id": 3, "method": "tools/call", "params": {"name": "lean_update", "arguments": {"path": "TodoSmoke.lean", "workspace": workspace}}})
 update_content = update.get("result", {}).get("structuredContent", {})
-version = update_content.get("version")
-if not isinstance(version, int):
-    print(f"expected lean_update MCP smoke to return a document version: {update}", file=sys.stderr)
+snapshot = update_content.get("snapshot")
+if not isinstance(snapshot, str):
+    print(f"expected lean_update MCP smoke to return a document snapshot: {update}", file=sys.stderr)
     proc.kill()
     sys.exit(1)
 todo = request({
@@ -450,7 +450,7 @@ todo = request({
         "name": "lean_todo",
         "arguments": {
             "path": "TodoSmoke.lean",
-            "version": version,
+            "snapshot": snapshot,
             "start_line": 13,
             "start_character": 0,
             "end_line": 14,
diff --git a/tests/test-beam-save-olean.sh b/tests/test-beam-save-olean.sh
index e9163878..4e0e492e 100755
--- a/tests/test-beam-save-olean.sh
+++ b/tests/test-beam-save-olean.sh
@@ -427,10 +427,10 @@ beam_start_owner "$tmp2"
   save_json="$(beam --root "$tmp2" close-save SaveSmoke/B.lean)"
   if [ "$(BEAM_JSON_PAYLOAD="$save_json" python3 - <<'PY'
 import json, os
-print(json.loads(os.environ["BEAM_JSON_PAYLOAD"])["result"]["saved"]["version"])
+print(json.loads(os.environ["BEAM_JSON_PAYLOAD"])["result"]["saved"]["snapshot"])
 PY
-)" != "1" ]; then
-    echo "expected close-save to report saved version 1" >&2
+)" = "" ]; then
+    echo "expected close-save to report its saved snapshot" >&2
     printf '%s\n' "$save_json" >&2
     exit 1
   fi
diff --git a/tests/test-beam-wrapper-daemon.sh b/tests/test-beam-wrapper-daemon.sh
index 4fa19958..004c11aa 100644
--- a/tests/test-beam-wrapper-daemon.sh
+++ b/tests/test-beam-wrapper-daemon.sh
@@ -48,11 +48,11 @@ start_slow_request() {
   local root="$1"
   local label="$2"
   local request_id="$3"
-  local version
-  version="$(beam_wrapper_update_version "$label SlowPoll" \
+  local snapshot
+  snapshot="$(beam_wrapper_update_snapshot "$label SlowPoll" \
     "$beam_script" --root "$root" update tests/scenario/docs/SlowPoll.lean)"
   BEAM_PROGRESS=1 BEAM_REQUEST_ID="$request_id" "$beam_script" --root "$root" \
-    run-at tests/scenario/docs/SlowPoll.lean "$version" 25 2 poll_sleep_cmd \
+    run-at tests/scenario/docs/SlowPoll.lean "$snapshot" 25 2 poll_sleep_cmd \
     >"$root/$label.out" 2>"$root/$label.err" &
   active_request_pid="$!"
   if ! wait_for_file_text "$root/$label.err" "running run-at" \
@@ -1288,7 +1288,9 @@ if ! grep -Fq "existing mode is 0755, expected 0700" "$tmp2/changed-mode.err"; t
   exit 1
 fi
 explicit_stop_command="lean-beam --root '$resolved_tmp2' --session-dir '$(beam_test_realpath "$explicit_control")' stop"
-if ! grep -Fq "$explicit_stop_command" "$tmp2/explicit-control-owner.err"; then
+# Descriptor publication precedes backend initialization and the foreground owner's message.
+if ! wait_for_file_text "$tmp2/explicit-control-owner.err" "$explicit_stop_command" \
+    "foreground owner stop command" 600; then
   echo "expected the foreground owner to print its exact stop command" >&2
   cat "$tmp2/explicit-control-owner.err" >&2
   exit 1
diff --git a/tests/test-beam-wrapper-diagnostics.sh b/tests/test-beam-wrapper-diagnostics.sh
index a3784afb..62ac8ff2 100755
--- a/tests/test-beam-wrapper-diagnostics.sh
+++ b/tests/test-beam-wrapper-diagnostics.sh
@@ -345,7 +345,7 @@ set_option linter.unusedVariables true in
 theorem warnOnly (n : Nat) : True := by
   trivial
 
--- close-save fresh version
+-- close-save fresh snapshot
 EOF
 
   cat > SaveSmoke/B.lean <<'EOF'
diff --git a/tests/test-beam-wrapper-handle.sh b/tests/test-beam-wrapper-handle.sh
index 7a611525..9813784f 100644
--- a/tests/test-beam-wrapper-handle.sh
+++ b/tests/test-beam-wrapper-handle.sh
@@ -22,9 +22,9 @@ beam_wrapper_start_owner "$handle_root"
 example : True ∧ True := by
 EOF
 
-  handle_version="$(beam_wrapper_update_version HandleSmoke "$beam_script" update HandleSmoke.lean)"
+  handle_snapshot="$(beam_wrapper_update_snapshot HandleSmoke "$beam_script" update HandleSmoke.lean)"
 
-  mint_handle_stdin="$(printf 'constructor' | "$beam_script" run-at-handle HandleSmoke.lean "$handle_version" 0 27 --stdin)"
+  mint_handle_stdin="$(printf 'constructor' | "$beam_script" run-at-handle HandleSmoke.lean "$handle_snapshot" 0 27 --stdin)"
   if [ "$(BEAM_JSON_PAYLOAD="$mint_handle_stdin" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper handle mint via --stdin to succeed" >&2
     printf '%s\n' "$mint_handle_stdin" >&2
@@ -38,7 +38,7 @@ EOF
 
   handle_mint_file="handle-mint.txt"
   printf 'constructor' > "$handle_mint_file"
-  mint_handle_file="$("$beam_script" run-at-handle HandleSmoke.lean "$handle_version" 0 27 --text-file "$handle_mint_file")"
+  mint_handle_file="$("$beam_script" run-at-handle HandleSmoke.lean "$handle_snapshot" 0 27 --text-file "$handle_mint_file")"
   if [ "$(BEAM_JSON_PAYLOAD="$mint_handle_file" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper handle mint via --text-file to succeed" >&2
     printf '%s\n' "$mint_handle_file" >&2
@@ -52,7 +52,7 @@ EOF
   branch_handle_file="branch-handle.json"
   printf '%s\n' "$mint_handle_file" > "$branch_handle_file"
 
-  mint_handle="$("$beam_script" run-at-handle HandleSmoke.lean "$handle_version" 0 27 "constructor")"
+  mint_handle="$("$beam_script" run-at-handle HandleSmoke.lean "$handle_snapshot" 0 27 "constructor")"
   if [ "$(BEAM_JSON_PAYLOAD="$mint_handle" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper handle mint to succeed" >&2
     printf '%s\n' "$mint_handle" >&2
@@ -132,7 +132,7 @@ EOF
     exit 1
   fi
 
-  mint_linear="$("$beam_script" run-at-handle HandleSmoke.lean "$handle_version" 0 27 "constructor")"
+  mint_linear="$("$beam_script" run-at-handle HandleSmoke.lean "$handle_snapshot" 0 27 "constructor")"
   if [ "$(BEAM_JSON_PAYLOAD="$mint_linear" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper linear handle mint to succeed" >&2
     printf '%s\n' "$mint_linear" >&2
@@ -220,8 +220,8 @@ EOF
     exit 1
   fi
 
-  portable_helper_version="$(beam_wrapper_update_version "portable HandleSmoke" "$beam_script" update HandleSmoke.lean)"
-  portable_helper_root="$(PATH="$portable_wrapper_bin:$PATH" "$portable_wrapper_bin/lean-beam-search" mint HandleSmoke.lean "$portable_helper_version" 0 27 "constructor")"
+  portable_helper_snapshot="$(beam_wrapper_update_snapshot "portable HandleSmoke" "$beam_script" update HandleSmoke.lean)"
+  portable_helper_root="$(PATH="$portable_wrapper_bin:$PATH" "$portable_wrapper_bin/lean-beam-search" mint HandleSmoke.lean "$portable_helper_snapshot" 0 27 "constructor")"
   if [ "$(BEAM_JSON_PAYLOAD="$portable_helper_root" read_json_text_field ok)" != "true" ]; then
     echo "expected symlinked helper to work when readlink -f is unavailable" >&2
     printf '%s\n' "$portable_helper_root" >&2
@@ -262,7 +262,7 @@ EOF
     exit 1
   fi
 
-  helper_root="$("$search_helper" mint HandleSmoke.lean "$portable_helper_version" 0 27 "constructor")"
+  helper_root="$("$search_helper" mint HandleSmoke.lean "$portable_helper_snapshot" 0 27 "constructor")"
   if [ "$(BEAM_JSON_PAYLOAD="$helper_root" read_json_text_field ok)" != "true" ]; then
     echo "expected helper mint to succeed" >&2
     printf '%s\n' "$helper_root" >&2
diff --git a/tests/test-beam-wrapper-probe.sh b/tests/test-beam-wrapper-probe.sh
index 07a662e6..51cce969 100644
--- a/tests/test-beam-wrapper-probe.sh
+++ b/tests/test-beam-wrapper-probe.sh
@@ -38,15 +38,15 @@ fi
 (
   cd "$project_root"
   "$beam_script" stats > /dev/null
-  command_version="$(beam_wrapper_update_version CommandA "$beam_script" update CommandA.lean)"
-  signature_version="$(beam_wrapper_update_version SignatureHelp "$beam_script" update SignatureHelp.lean)"
-  position_empty_version="$(beam_wrapper_update_version PositionEmptyLine "$beam_script" update PositionEmptyLine.lean)"
-  position_utf16_version="$(beam_wrapper_update_version PositionUtf16 "$beam_script" update PositionUtf16.lean)"
-  goal_version="$(beam_wrapper_update_version GoalSmoke "$beam_script" update GoalSmoke.lean)"
-  todo_version="$(beam_wrapper_update_version TodoSmoke "$beam_script" update TodoSmoke.lean)"
+  command_snapshot="$(beam_wrapper_update_snapshot CommandA "$beam_script" update CommandA.lean)"
+  signature_snapshot="$(beam_wrapper_update_snapshot SignatureHelp "$beam_script" update SignatureHelp.lean)"
+  position_empty_snapshot="$(beam_wrapper_update_snapshot PositionEmptyLine "$beam_script" update PositionEmptyLine.lean)"
+  position_utf16_snapshot="$(beam_wrapper_update_snapshot PositionUtf16 "$beam_script" update PositionUtf16.lean)"
+  goal_snapshot="$(beam_wrapper_update_snapshot GoalSmoke "$beam_script" update GoalSmoke.lean)"
+  todo_snapshot="$(beam_wrapper_update_snapshot TodoSmoke "$beam_script" update TodoSmoke.lean)"
 
   cmd_err="$(beam_wrapper_mktemp_file progress)"
-  cmd_out="$(BEAM_PROGRESS=1 "$beam_script" run-at CommandA.lean "$command_version" 0 2 "#check answerA" 2>"$cmd_err")"
+  cmd_out="$(BEAM_PROGRESS=1 "$beam_script" run-at CommandA.lean "$command_snapshot" 0 2 "#check answerA" 2>"$cmd_err")"
   if [ "$(BEAM_JSON_PAYLOAD="$cmd_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper run-at to succeed" >&2
     printf '%s\n' "$cmd_out" >&2
@@ -88,40 +88,38 @@ fi
     exit 1
   fi
 
-  stale_command_version="$command_version"
-  printf '\n-- wrapper stale-version probe\n' >> CommandA.lean
-  command_version="$(beam_wrapper_update_version CommandA-changed "$beam_script" update CommandA.lean)"
-  stale_version_out="$(beam_wrapper_mktemp_file stale-version-out)"
-  stale_version_err="$(beam_wrapper_mktemp_file stale-version-err)"
-  if "$beam_script" run-at CommandA.lean "$stale_command_version" 0 2 "#check answerA" \
-      >"$stale_version_out" 2>"$stale_version_err"; then
-    echo "expected wrapper run-at with a stale version to fail" >&2
-    cat "$stale_version_out" >&2
-    cat "$stale_version_err" >&2
-    exit 1
-  fi
-  assert_json_file_field_equals "stale wrapper run-at" "$stale_version_out" \
-    error.code contentModified "$stale_version_err"
-  assert_json_file_field_equals "stale wrapper run-at" "$stale_version_out" \
-    error.data.reason documentVersionMismatch "$stale_version_err"
-  assert_json_file_field_equals "stale wrapper run-at" "$stale_version_out" \
-    error.data.expectedVersion "$stale_command_version" "$stale_version_err"
-  assert_json_file_field_equals "stale wrapper run-at" "$stale_version_out" \
-    error.data.acceptedVersion "$command_version" "$stale_version_err"
-  assert_json_file_field_equals "stale wrapper run-at" "$stale_version_out" \
-    error.data.currentVersion "$command_version" "$stale_version_err"
-  stale_version_uri="$(json_file_text_field "$stale_version_out" error.data.uri)"
-  case "$stale_version_uri" in
+  stale_command_snapshot="$command_snapshot"
+  printf '\n-- wrapper stale-snapshot probe\n' >> CommandA.lean
+  command_snapshot="$(beam_wrapper_update_snapshot CommandA-changed "$beam_script" update CommandA.lean)"
+  stale_snapshot_out="$(beam_wrapper_mktemp_file stale-snapshot-out)"
+  stale_snapshot_err="$(beam_wrapper_mktemp_file stale-snapshot-err)"
+  if "$beam_script" run-at CommandA.lean "$stale_command_snapshot" 0 2 "#check answerA" \
+      >"$stale_snapshot_out" 2>"$stale_snapshot_err"; then
+    echo "expected wrapper run-at with a stale snapshot to fail" >&2
+    cat "$stale_snapshot_out" >&2
+    cat "$stale_snapshot_err" >&2
+    exit 1
+  fi
+  assert_json_file_field_equals "stale wrapper run-at" "$stale_snapshot_out" \
+    error.code contentModified "$stale_snapshot_err"
+  assert_json_file_field_equals "stale wrapper run-at" "$stale_snapshot_out" \
+    error.data.reason snapshotMismatch "$stale_snapshot_err"
+  assert_json_file_field_equals "stale wrapper run-at" "$stale_snapshot_out" \
+    error.data.expectedSnapshot "$stale_command_snapshot" "$stale_snapshot_err"
+  assert_json_file_field_equals "stale wrapper run-at" "$stale_snapshot_out" \
+    error.data.currentSnapshot "$command_snapshot" "$stale_snapshot_err"
+  stale_snapshot_uri="$(json_file_text_field "$stale_snapshot_out" error.data.uri)"
+  case "$stale_snapshot_uri" in
     */CommandA.lean)
       ;;
     *)
-      echo "expected stale wrapper run-at to report a CommandA.lean uri, got ${stale_version_uri:-<empty>}" >&2
-      print_json_file_assertion_context "$stale_version_out" "$stale_version_err"
+      echo "expected stale wrapper run-at to report a CommandA.lean uri, got ${stale_snapshot_uri:-<empty>}" >&2
+      print_json_file_assertion_context "$stale_snapshot_out" "$stale_snapshot_err"
       exit 1
       ;;
   esac
 
-  multiline_stdin_out="$(printf 'def stdinProbe : Nat :=\n  42' | "$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 0 --stdin)"
+  multiline_stdin_out="$(printf 'def stdinProbe : Nat :=\n  42' | "$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 0 --stdin)"
   if [ "$(BEAM_JSON_PAYLOAD="$multiline_stdin_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper run-at --stdin probe to succeed" >&2
     printf '%s\n' "$multiline_stdin_out" >&2
@@ -140,7 +138,7 @@ fi
 
   probe_text_file="multiline-probe.lean"
   printf 'def fileProbe : Nat :=\n  42' > "$probe_text_file"
-  multiline_file_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 0 --text-file "$probe_text_file")"
+  multiline_file_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 0 --text-file "$probe_text_file")"
   if [ "$(BEAM_JSON_PAYLOAD="$multiline_file_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper run-at --text-file probe to succeed" >&2
     printf '%s\n' "$multiline_file_out" >&2
@@ -157,7 +155,7 @@ fi
     exit 1
   fi
 
-  delimiter_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 0 -- $'--stdin\n#check answer')"
+  delimiter_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 0 -- $'--stdin\n#check answer')"
   if [ "$(BEAM_JSON_PAYLOAD="$delimiter_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper run-at -- delimiter path to treat leading --stdin as text" >&2
     printf '%s\n' "$delimiter_out" >&2
@@ -170,7 +168,7 @@ fi
   fi
 
   debug_text_err="$(beam_wrapper_mktemp_file debug-text)"
-  debug_text_out="$(printf 'def debugProbe : Nat :=\n  42' | BEAM_DEBUG_TEXT=1 "$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 0 --stdin 2>"$debug_text_err")"
+  debug_text_out="$(printf 'def debugProbe : Nat :=\n  42' | BEAM_DEBUG_TEXT=1 "$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 0 --stdin 2>"$debug_text_err")"
   if [ "$(BEAM_JSON_PAYLOAD="$debug_text_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper debug-text probe to succeed" >&2
     printf '%s\n' "$debug_text_out" >&2
@@ -204,7 +202,7 @@ fi
   fi
 
   literal_newline_err="$(beam_wrapper_mktemp_file literal-newline)"
-  literal_newline_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 0 'def _probe_tmp : Nat := 0\n' 2>"$literal_newline_err")"
+  literal_newline_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 0 'def _probe_tmp : Nat := 0\n' 2>"$literal_newline_err")"
   if [ "$(BEAM_JSON_PAYLOAD="$literal_newline_out" read_json_text_field ok)" != "true" ]; then
     printf '%s\n' "expected wrapper literal-\\n probe to stay a payload failure, not a transport error" >&2
     printf '%s\n' "$literal_newline_out" >&2
@@ -239,7 +237,7 @@ fi
     exit 1
   fi
 
-  blank_ok_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 0 "#check answer")"
+  blank_ok_out="$("$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 0 "#check answer")"
   if [ "$(BEAM_JSON_PAYLOAD="$blank_ok_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper blank-line probe at character 0 to succeed" >&2
     printf '%s\n' "$blank_ok_out" >&2
@@ -252,7 +250,7 @@ fi
   fi
 
   blank_err="$(beam_wrapper_mktemp_file empty-line)"
-  if "$beam_script" run-at PositionEmptyLine.lean "$position_empty_version" 1 1 "#check answer" >"$blank_err" 2>&1; then
+  if "$beam_script" run-at PositionEmptyLine.lean "$position_empty_snapshot" 1 1 "#check answer" >"$blank_err" 2>&1; then
     echo "expected wrapper blank-line probe at character 1 to be rejected" >&2
     cat "$blank_err" >&2
     exit 1
@@ -268,7 +266,7 @@ fi
     exit 1
   fi
 
-  utf16_ok_out="$("$beam_script" run-at PositionUtf16.lean "$position_utf16_version" 1 5 "#check Nat")"
+  utf16_ok_out="$("$beam_script" run-at PositionUtf16.lean "$position_utf16_snapshot" 1 5 "#check Nat")"
   if [ "$(BEAM_JSON_PAYLOAD="$utf16_ok_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper UTF-16 boundary probe to succeed" >&2
     printf '%s\n' "$utf16_ok_out" >&2
@@ -281,7 +279,7 @@ fi
   fi
 
   utf16_err="$(beam_wrapper_mktemp_file utf16)"
-  if "$beam_script" run-at PositionUtf16.lean "$position_utf16_version" 1 6 "#check Nat" >"$utf16_err" 2>&1; then
+  if "$beam_script" run-at PositionUtf16.lean "$position_utf16_snapshot" 1 6 "#check Nat" >"$utf16_err" 2>&1; then
     echo "expected wrapper UTF-16 out-of-range probe to be rejected" >&2
     cat "$utf16_err" >&2
     exit 1
@@ -305,7 +303,7 @@ fi
     exit 1
   fi
 
-  hover_out="$("$beam_script" hover CommandA.lean "$command_version" 0 4)"
+  hover_out="$("$beam_script" hover CommandA.lean "$command_snapshot" 0 4)"
   if [ "$(BEAM_JSON_PAYLOAD="$hover_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper hover probe to succeed" >&2
     printf '%s\n' "$hover_out" >&2
@@ -317,7 +315,7 @@ fi
     exit 1
   fi
 
-  signature_help_out="$("$beam_script" signature-help SignatureHelp.lean "$signature_version" 4 12)"
+  signature_help_out="$("$beam_script" signature-help SignatureHelp.lean "$signature_snapshot" 4 12)"
   if [ "$(BEAM_JSON_PAYLOAD="$signature_help_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper signature-help probe to succeed" >&2
     printf '%s\n' "$signature_help_out" >&2
@@ -329,7 +327,7 @@ fi
     exit 1
   fi
 
-  definition_out="$("$beam_script" definition CommandA.lean "$command_version" 0 4)"
+  definition_out="$("$beam_script" definition CommandA.lean "$command_snapshot" 0 4)"
   if [ "$(BEAM_JSON_PAYLOAD="$definition_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper definition probe to succeed" >&2
     printf '%s\n' "$definition_out" >&2
@@ -341,7 +339,7 @@ fi
     exit 1
   fi
 
-  references_nav_out="$("$beam_script" references CommandA.lean "$command_version" 0 4)"
+  references_nav_out="$("$beam_script" references CommandA.lean "$command_snapshot" 0 4)"
   if [ "$(BEAM_JSON_PAYLOAD="$references_nav_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper references probe to succeed" >&2
     printf '%s\n' "$references_nav_out" >&2
@@ -353,7 +351,7 @@ fi
     exit 1
   fi
 
-  document_symbols_out="$("$beam_script" document-symbols CommandA.lean "$command_version")"
+  document_symbols_out="$("$beam_script" document-symbols CommandA.lean "$command_snapshot")"
   if [ "$(BEAM_JSON_PAYLOAD="$document_symbols_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper document-symbols probe to succeed" >&2
     printf '%s\n' "$document_symbols_out" >&2
@@ -373,7 +371,7 @@ fi
   fi
   BEAM_JSON_PAYLOAD="$workspace_symbols_out" read_json_array_len result > /dev/null
 
-  goals_prev_out="$("$beam_script" goals before GoalSmoke.lean "$goal_version" 1 2)"
+  goals_prev_out="$("$beam_script" goals before GoalSmoke.lean "$goal_snapshot" 1 2)"
   if [ "$(BEAM_JSON_PAYLOAD="$goals_prev_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper goals before probe to succeed" >&2
     printf '%s\n' "$goals_prev_out" >&2
@@ -385,7 +383,7 @@ fi
     exit 1
   fi
 
-  goals_after_out="$("$beam_script" goals after GoalSmoke.lean "$goal_version" 1 2)"
+  goals_after_out="$("$beam_script" goals after GoalSmoke.lean "$goal_snapshot" 1 2)"
   if [ "$(BEAM_JSON_PAYLOAD="$goals_after_out" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper goals after probe to succeed" >&2
     printf '%s\n' "$goals_after_out" >&2
@@ -397,7 +395,7 @@ fi
     exit 1
   fi
 
-  todo_out="$("$beam_script" todo TodoSmoke.lean "$todo_version" 13 0 14 0 --kind sorry --suggest none)"
+  todo_out="$("$beam_script" todo TodoSmoke.lean "$todo_snapshot" 13 0 14 0 --kind sorry --suggest none)"
   assert_json_field_equals "wrapper todo" "$todo_out" ok true
   assert_json_array_len_equals "wrapper todo" "$todo_out" result.items 1
   assert_json_field_equals "wrapper todo" "$todo_out" result.items.0.kind sorry
diff --git a/tests/test-beam-wrapper-runtime.sh b/tests/test-beam-wrapper-runtime.sh
index bd3cb874..4d81a43c 100644
--- a/tests/test-beam-wrapper-runtime.sh
+++ b/tests/test-beam-wrapper-runtime.sh
@@ -18,20 +18,20 @@ signal_root="$(beam_wrapper_prepare_project_root_with_scenario_docs runtime-sign
 
 run_sigint_probe() {
   local project_root="$1"
-  local version="$2"
+  local snapshot="$2"
   local out_path="$3"
   local err_path="$4"
   local progress_enabled="$5"
   local request_id="$6"
   local wait_mode="$7"
-  python3 - "$beam_script" "$project_root" "$version" "$out_path" "$err_path" "$progress_enabled" "$request_id" "$wait_mode" <<'PY'
+  python3 - "$beam_script" "$project_root" "$snapshot" "$out_path" "$err_path" "$progress_enabled" "$request_id" "$wait_mode" <<'PY'
 import os
 import signal
 import subprocess
 import sys
 import time
 
-beam_script, project_root, version, out_path, err_path, progress_enabled, request_id, wait_mode = sys.argv[1:]
+beam_script, project_root, snapshot, out_path, err_path, progress_enabled, request_id, wait_mode = sys.argv[1:]
 env = os.environ.copy()
 if progress_enabled == "1":
     env["BEAM_PROGRESS"] = "1"
@@ -64,7 +64,7 @@ with open(out_path, "wb") as out, open(err_path, "wb") as err:
             project_root,
             "run-at",
             "tests/scenario/docs/SlowPoll.lean",
-            version,
+            snapshot,
             "25",
             "2",
             "poll_sleep_cmd",
@@ -147,12 +147,12 @@ beam_wrapper_start_owner "$signal_root"
 signal_owner_pid="$beam_wrapper_last_owner_pid"
 (
   cd "$signal_root"
-  slow_version="$(beam_wrapper_update_version "signal SlowPoll" "$beam_script" --root "$signal_root" update tests/scenario/docs/SlowPoll.lean)"
-  command_version="$(beam_wrapper_update_version "signal CommandA" "$beam_script" --root "$signal_root" update tests/scenario/docs/CommandA.lean)"
+  slow_snapshot="$(beam_wrapper_update_snapshot "signal SlowPoll" "$beam_script" --root "$signal_root" update tests/scenario/docs/SlowPoll.lean)"
+  command_snapshot="$(beam_wrapper_update_snapshot "signal CommandA" "$beam_script" --root "$signal_root" update tests/scenario/docs/CommandA.lean)"
 
   interrupt_out="$(beam_wrapper_mktemp_file interrupt-out)"
   interrupt_err="$(beam_wrapper_mktemp_file interrupt-err)"
-  interrupt_status="$(run_sigint_probe "$signal_root" "$slow_version" "$interrupt_out" "$interrupt_err" 1 wrapper-sigint stderr)"
+  interrupt_status="$(run_sigint_probe "$signal_root" "$slow_snapshot" "$interrupt_out" "$interrupt_err" 1 wrapper-sigint stderr)"
   if [ "$interrupt_status" = "timeout" ] || [ "$interrupt_status" = "early-exit" ]; then
     cat "$interrupt_out" >&2
     cat "$interrupt_err" >&2
@@ -168,7 +168,7 @@ signal_owner_pid="$beam_wrapper_last_owner_pid"
 
   interrupt_anon_out="$(beam_wrapper_mktemp_file interrupt-anon-out)"
   interrupt_anon_err="$(beam_wrapper_mktemp_file interrupt-anon-err)"
-  interrupt_anon_status="$(run_sigint_probe "$signal_root" "$slow_version" "$interrupt_anon_out" "$interrupt_anon_err" 1 "" stderr)"
+  interrupt_anon_status="$(run_sigint_probe "$signal_root" "$slow_snapshot" "$interrupt_anon_out" "$interrupt_anon_err" 1 "" stderr)"
   if [ "$interrupt_anon_status" = "timeout" ] || [ "$interrupt_anon_status" = "early-exit" ]; then
     cat "$interrupt_anon_out" >&2
     cat "$interrupt_anon_err" >&2
@@ -182,7 +182,7 @@ signal_owner_pid="$beam_wrapper_last_owner_pid"
   fi
   expect_sigint_aborted "anonymous wrapper SIGINT path" "$interrupt_anon_out" "$interrupt_anon_err" ""
 
-  post_interrupt_hover="$("$beam_script" --root "$signal_root" hover tests/scenario/docs/CommandA.lean "$command_version" 0 4)"
+  post_interrupt_hover="$("$beam_script" --root "$signal_root" hover tests/scenario/docs/CommandA.lean "$command_snapshot" 0 4)"
   if [ "$(BEAM_JSON_PAYLOAD="$post_interrupt_hover" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper SIGINT interruption to preserve the isolated Beam daemon session" >&2
     printf '%s\n' "$post_interrupt_hover" >&2
@@ -191,14 +191,14 @@ signal_owner_pid="$beam_wrapper_last_owner_pid"
 
   interrupt_quiet_out="$(beam_wrapper_mktemp_file interrupt-quiet-out)"
   interrupt_quiet_err="$(beam_wrapper_mktemp_file interrupt-quiet-err)"
-  interrupt_quiet_status="$(python3 - "$beam_script" "$signal_root" "$slow_version" "$command_version" "$interrupt_quiet_out" "$interrupt_quiet_err" <<'PY'
+  interrupt_quiet_status="$(python3 - "$beam_script" "$signal_root" "$slow_snapshot" "$command_snapshot" "$interrupt_quiet_out" "$interrupt_quiet_err" <<'PY'
 import os
 import signal
 import subprocess
 import sys
 import time
 
-beam_script, project_root, slow_version, command_version, out_path, err_path = sys.argv[1:]
+beam_script, project_root, slow_snapshot, command_snapshot, out_path, err_path = sys.argv[1:]
 base_request_id = "wrapper-sigint-quiet"
 max_attempts = 5
 setup_race_count = 0
@@ -242,7 +242,7 @@ for attempt in range(1, max_attempts + 1):
                 project_root,
                 "run-at",
                 "tests/scenario/docs/SlowPoll.lean",
-                slow_version,
+                slow_snapshot,
                 "25",
                 "2",
                 "poll_sleep_cmd",
@@ -267,7 +267,7 @@ for attempt in range(1, max_attempts + 1):
                 project_root,
                 "hover",
                 "tests/scenario/docs/CommandA.lean",
-                command_version,
+                command_snapshot,
                 "0",
                 "4",
             ],
@@ -337,7 +337,7 @@ PY
 
   interrupt_quiet_anon_out="$(beam_wrapper_mktemp_file interrupt-quiet-anon-out)"
   interrupt_quiet_anon_err="$(beam_wrapper_mktemp_file interrupt-quiet-anon-err)"
-  interrupt_quiet_anon_status="$(run_sigint_probe "$signal_root" "$slow_version" "$interrupt_quiet_anon_out" "$interrupt_quiet_anon_err" 0 "" sleep)"
+  interrupt_quiet_anon_status="$(run_sigint_probe "$signal_root" "$slow_snapshot" "$interrupt_quiet_anon_out" "$interrupt_quiet_anon_err" 0 "" sleep)"
   if [ "$interrupt_quiet_anon_status" = "timeout" ] || [ "$interrupt_quiet_anon_status" = "early-exit" ]; then
     cat "$interrupt_quiet_anon_out" >&2
     cat "$interrupt_quiet_anon_err" >&2
@@ -361,21 +361,21 @@ beam_wrapper_start_owner "$signal_root"
 signal_owner_pid="$beam_wrapper_last_owner_pid"
 (
   cd "$signal_root"
-  slow_version="$(beam_wrapper_update_version "duplicate SlowPoll" "$beam_script" --root "$signal_root" update tests/scenario/docs/SlowPoll.lean)"
-  command_version="$(beam_wrapper_update_version "duplicate CommandA" "$beam_script" --root "$signal_root" update tests/scenario/docs/CommandA.lean)"
+  slow_snapshot="$(beam_wrapper_update_snapshot "duplicate SlowPoll" "$beam_script" --root "$signal_root" update tests/scenario/docs/SlowPoll.lean)"
+  command_snapshot="$(beam_wrapper_update_snapshot "duplicate CommandA" "$beam_script" --root "$signal_root" update tests/scenario/docs/CommandA.lean)"
 
   duplicate_slow_out="$(beam_wrapper_mktemp_file duplicate-slow-out)"
   duplicate_slow_err="$(beam_wrapper_mktemp_file duplicate-slow-err)"
   duplicate_out="$(beam_wrapper_mktemp_file duplicate-out)"
   duplicate_err="$(beam_wrapper_mktemp_file duplicate-err)"
   BEAM_PROGRESS=1 BEAM_REQUEST_ID=wrapper-duplicate-active \
-    "$beam_script" --root "$signal_root" run-at tests/scenario/docs/SlowPoll.lean "$slow_version" 25 2 "poll_sleep_cmd" \
+    "$beam_script" --root "$signal_root" run-at tests/scenario/docs/SlowPoll.lean "$slow_snapshot" 25 2 "poll_sleep_cmd" \
     >"$duplicate_slow_out" 2>"$duplicate_slow_err" &
   duplicate_slow_pid=$!
   sleep 1
 
   if BEAM_REQUEST_ID=wrapper-duplicate-active \
-      "$beam_script" --root "$signal_root" hover tests/scenario/docs/CommandA.lean "$command_version" 0 4 \
+      "$beam_script" --root "$signal_root" hover tests/scenario/docs/CommandA.lean "$command_snapshot" 0 4 \
       >"$duplicate_out" 2>"$duplicate_err"; then
     echo "expected duplicate active BEAM_REQUEST_ID wrapper request to fail" >&2
     cat "$duplicate_out" >&2
diff --git a/tests/test-beam-wrapper-sync-save.sh b/tests/test-beam-wrapper-sync-save.sh
index ea412e27..ae794876 100755
--- a/tests/test-beam-wrapper-sync-save.sh
+++ b/tests/test-beam-wrapper-sync-save.sh
@@ -28,8 +28,8 @@ beam_wrapper_start_owner "$standalone_root"
     exit 1
   fi
 
-  probe_before_version="$(beam_wrapper_update_version "initial SaveSmoke/B.lean" "$beam_script" update SaveSmoke/B.lean)"
-  probe_before="$("$beam_script" run-at SaveSmoke/B.lean "$probe_before_version" 0 2 "#eval bVal")"
+  probe_before_snapshot="$(beam_wrapper_update_snapshot "initial SaveSmoke/B.lean" "$beam_script" update SaveSmoke/B.lean)"
+  probe_before="$("$beam_script" run-at SaveSmoke/B.lean "$probe_before_snapshot" 0 2 "#eval bVal")"
   if [ "$(BEAM_JSON_PAYLOAD="$probe_before" read_json_text_field ok)" != "true" ]; then
     echo "expected initial wrapper probe to succeed" >&2
     printf '%s\n' "$probe_before" >&2
@@ -71,8 +71,8 @@ beam_wrapper_start_owner "$standalone_root"
     printf '%s\n' "$sync_out" >&2
     exit 1
   fi
-  if [ "$(BEAM_JSON_PAYLOAD="$sync_out" read_json_text_field result.version)" != "2" ]; then
-    echo "expected sync after first edit to report version 2" >&2
+  if [ "$(BEAM_JSON_PAYLOAD="$sync_out" read_json_text_field result.snapshot)" = "$probe_before_snapshot" ]; then
+    echo "expected sync after first edit to return a fresh snapshot" >&2
     printf '%s\n' "$sync_out" >&2
     exit 1
   fi
@@ -96,8 +96,8 @@ beam_wrapper_start_owner "$standalone_root"
     exit 1
   fi
 
-  probe_after_version="$(json_text_field "$sync_out" result.version)"
-  probe_after="$("$beam_script" run-at SaveSmoke/B.lean "$probe_after_version" 0 2 "#eval bVal")"
+  probe_after_snapshot="$(json_text_field "$sync_out" result.snapshot)"
+  probe_after="$("$beam_script" run-at SaveSmoke/B.lean "$probe_after_snapshot" 0 2 "#eval bVal")"
   if [ "$(BEAM_JSON_PAYLOAD="$probe_after" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper probe after sync to succeed" >&2
     printf '%s\n' "$probe_after" >&2
@@ -116,13 +116,13 @@ beam_wrapper_start_owner "$standalone_root"
     exit 1
   fi
   assert_json_completed_file_progress "save after synced edit" "$save_out" fileProgress
-  if [ "$(BEAM_JSON_PAYLOAD="$save_out" read_json_text_field result.version)" != "2" ]; then
-    echo "expected save to report saved version 2" >&2
+  if [ "$(BEAM_JSON_PAYLOAD="$save_out" read_json_text_field result.snapshot)" != "$probe_after_snapshot" ]; then
+    echo "expected save to report the saved snapshot" >&2
     printf '%s\n' "$save_out" >&2
     exit 1
   fi
-  if [ "$(BEAM_JSON_PAYLOAD="$save_out" read_json_text_field result.sync.version)" != "2" ]; then
-    echo "expected save to include a sync verdict for version 2" >&2
+  if [ "$(BEAM_JSON_PAYLOAD="$save_out" read_json_text_field result.sync.snapshot)" != "$probe_after_snapshot" ]; then
+    echo "expected save to include a sync verdict for the saved snapshot" >&2
     printf '%s\n' "$save_out" >&2
     exit 1
   fi
@@ -163,8 +163,8 @@ beam_wrapper_start_owner "$standalone_root"
     printf '%s\n' "$sync_second" >&2
     exit 1
   fi
-  if [ "$(BEAM_JSON_PAYLOAD="$sync_second" read_json_text_field result.version)" != "3" ]; then
-    echo "expected second sync to report version 3" >&2
+  if [ "$(BEAM_JSON_PAYLOAD="$sync_second" read_json_text_field result.snapshot)" = "$probe_after_snapshot" ]; then
+    echo "expected second sync to return a fresh snapshot" >&2
     printf '%s\n' "$sync_second" >&2
     exit 1
   fi
@@ -185,8 +185,8 @@ beam_wrapper_start_owner "$standalone_root"
     printf '%s\n' "$sync_third" >&2
     exit 1
   fi
-  if [ "$(BEAM_JSON_PAYLOAD="$sync_third" read_json_text_field result.version)" != "3" ]; then
-    echo "expected unchanged third sync to preserve version 3" >&2
+  if [ "$(BEAM_JSON_PAYLOAD="$sync_third" read_json_text_field result.snapshot)" != "$(json_text_field "$sync_second" result.snapshot)" ]; then
+    echo "expected unchanged third sync to preserve the snapshot" >&2
     printf '%s\n' "$sync_third" >&2
     exit 1
   fi
@@ -213,8 +213,8 @@ beam_wrapper_start_owner "$standalone_root"
     exit 1
   fi
 
-  probe_second_version="$(json_text_field "$refresh_out" result.version)"
-  probe_second="$("$beam_script" run-at SaveSmoke/B.lean "$probe_second_version" 0 2 "#eval bVal")"
+  probe_second_snapshot="$(json_text_field "$refresh_out" result.snapshot)"
+  probe_second="$("$beam_script" run-at SaveSmoke/B.lean "$probe_second_snapshot" 0 2 "#eval bVal")"
   if [ "$(BEAM_JSON_PAYLOAD="$probe_second" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper probe after refresh to succeed" >&2
     printf '%s\n' "$probe_second" >&2
@@ -240,8 +240,8 @@ beam_wrapper_start_owner "$standalone_root"
     exit 1
   fi
 
-  probe_reopen_version="$(beam_wrapper_update_version "reopened SaveSmoke/B.lean" "$beam_script" update SaveSmoke/B.lean)"
-  probe_reopen="$("$beam_script" run-at SaveSmoke/B.lean "$probe_reopen_version" 0 2 "#eval bVal")"
+  probe_reopen_snapshot="$(beam_wrapper_update_snapshot "reopened SaveSmoke/B.lean" "$beam_script" update SaveSmoke/B.lean)"
+  probe_reopen="$("$beam_script" run-at SaveSmoke/B.lean "$probe_reopen_snapshot" 0 2 "#eval bVal")"
   if [ "$(BEAM_JSON_PAYLOAD="$probe_reopen" read_json_text_field ok)" != "true" ]; then
     echo "expected wrapper probe after close to reopen the document successfully" >&2
     printf '%s\n' "$probe_reopen" >&2
diff --git a/tests/test-mcp-http-bridge.py b/tests/test-mcp-http-bridge.py
index 29822ae6..de875421 100644
--- a/tests/test-mcp-http-bridge.py
+++ b/tests/test-mcp-http-bridge.py
@@ -395,8 +395,8 @@ def main():
             require(sync.get("isError") is not True, f"lean_sync returned tool error: {sync}")
             structured = sync.get("structuredContent")
             require(isinstance(structured, dict), f"sync missing structuredContent: {sync}")
-            version = structured.get("version")
-            require(isinstance(version, int), f"sync missing version: {sync}")
+            snapshot = structured.get("snapshot")
+            require(isinstance(snapshot, str), f"sync missing snapshot: {sync}")
             require_document_progress_range(structured, "lean_sync")
 
             probe = expect_result(http_json(
@@ -409,7 +409,7 @@ def main():
                         "name": "lean_run_at",
                         "arguments": {
                             "path": "PositionEmptyLine.lean",
-                            "version": version,
+                            "snapshot": snapshot,
                             "line": 1,
                             "character": 0,
                             "text": "def mcpHttpProbe : Nat := 1",
diff --git a/tests/test-mcp-stdio.py b/tests/test-mcp-stdio.py
index c85c7727..1f74b70a 100644
--- a/tests/test-mcp-stdio.py
+++ b/tests/test-mcp-stdio.py
@@ -743,7 +743,7 @@ def expect_diagnostic_log(client, *, level, severity, path):
             and data.get("path") == path
         ):
             require(isinstance(data.get("uri"), str), f"diagnostic log missing uri: {notification}")
-            require(isinstance(data.get("version"), int), f"diagnostic log missing version: {notification}")
+            require(isinstance(data.get("snapshot"), str), f"diagnostic log missing snapshot: {notification}")
             require(isinstance(data.get("range"), dict), f"diagnostic log missing range: {notification}")
             require(isinstance(data.get("message"), str) and data["message"], f"diagnostic log missing message: {notification}")
             return notification
@@ -760,7 +760,7 @@ def expect_reply_diagnostic(sync, *, severity, path):
             and diagnostic.get("path") == path
         ):
             require(isinstance(diagnostic.get("uri"), str), f"reply diagnostic missing uri: {diagnostic}")
-            require(isinstance(diagnostic.get("version"), int), f"reply diagnostic missing version: {diagnostic}")
+            require(isinstance(diagnostic.get("snapshot"), str), f"reply diagnostic missing snapshot: {diagnostic}")
             require(isinstance(diagnostic.get("range"), dict), f"reply diagnostic missing range: {diagnostic}")
             require(isinstance(diagnostic.get("message"), str) and diagnostic["message"], f"reply diagnostic missing message: {diagnostic}")
             return diagnostic
@@ -824,24 +824,20 @@ def beam_cli_mcp_config(repo_root, root, timeout):
     return config
 
 
-def require_version_mismatch_data(error, expected_version, accepted_version, label, *, expected_uri_suffix=None):
+def require_snapshot_mismatch_data(error, expected_snapshot, accepted_snapshot, label, *, expected_uri_suffix=None):
     data = error.get("data")
     require(isinstance(data, dict), f"{label}: tool error missing data: {error}")
     require(
-        data.get("reason") == "documentVersionMismatch",
-        f"{label}: expected documentVersionMismatch data, got {error}",
+        data.get("reason") == "snapshotMismatch",
+        f"{label}: expected snapshotMismatch data, got {error}",
     )
     require(
-        data.get("expectedVersion") == expected_version,
-        f"{label}: expected expectedVersion={expected_version}, got {error}",
+        data.get("expectedSnapshot") == expected_snapshot,
+        f"{label}: expected expectedSnapshot={expected_snapshot}, got {error}",
     )
     require(
-        data.get("acceptedVersion") == accepted_version,
-        f"{label}: expected acceptedVersion={accepted_version}, got {error}",
-    )
-    require(
-        data.get("currentVersion") == accepted_version,
-        f"{label}: expected currentVersion={accepted_version}, got {error}",
+        data.get("currentSnapshot") == accepted_snapshot,
+        f"{label}: expected currentSnapshot={accepted_snapshot}, got {error}",
     )
     if expected_uri_suffix is not None:
         uri = data.get("uri")
@@ -966,27 +962,27 @@ def run_iteration(client, suffix):
         result_workspace_root(update, "lean_update").resolve() == client.project_root.resolve(),
         f"update returned wrong workspace descriptor: {update}",
     )
-    version = update.get("version")
-    require(isinstance(version, int), f"update did not return a document version: {update}")
+    snapshot = update.get("snapshot")
+    require(isinstance(snapshot, str), f"update did not return a document snapshot: {update}")
     changed = update.get("changed")
     require(isinstance(changed, bool), f"update did not return changed flag: {update}")
 
     command_update = client.call_tool("lean_update", {"path": "CommandA.lean"})
-    command_version = command_update.get("version")
-    require(isinstance(command_version, int), f"CommandA update did not return a version: {command_update}")
+    command_snapshot = command_update.get("snapshot")
+    require(isinstance(command_snapshot, str), f"CommandA update did not return a snapshot: {command_update}")
     command_path = client.project_root / "CommandA.lean"
     command_text = command_path.read_text(encoding="utf-8")
-    command_path.write_text(f"{command_text}\n-- mcp stale-version {suffix}\n", encoding="utf-8")
+    command_path.write_text(f"{command_text}\n-- mcp stale-snapshot {suffix}\n", encoding="utf-8")
     command_changed = client.call_tool("lean_update", {"path": "CommandA.lean"})
-    accepted_version = command_changed.get("version")
-    require(isinstance(accepted_version, int), f"CommandA changed update did not return a version: {command_changed}")
+    accepted_snapshot = command_changed.get("snapshot")
+    require(isinstance(accepted_snapshot, str), f"CommandA changed update did not return a snapshot: {command_changed}")
     stale_response = client.request(
         "tools/call",
         {
             "name": "lean_run_at",
             "arguments": {
                 "path": "CommandA.lean",
-                "version": command_version,
+                "snapshot": command_snapshot,
                 "line": 0,
                 "character": 2,
                 "text": "#check answerA",
@@ -994,10 +990,10 @@ def run_iteration(client, suffix):
         },
     )
     stale_error = expect_tool_error_code(stale_response, "contentModified")
-    require_version_mismatch_data(
+    require_snapshot_mismatch_data(
         stale_error,
-        command_version,
-        accepted_version,
+        command_snapshot,
+        accepted_snapshot,
         "stale MCP lean_run_at",
         expected_uri_suffix="/CommandA.lean",
     )
@@ -1006,7 +1002,7 @@ def run_iteration(client, suffix):
         "lean_run_at",
         {
             "path": "PositionEmptyLine.lean",
-            "version": version,
+            "snapshot": snapshot,
             "line": 1,
             "character": 0,
             "text": f"def mcpProbe{suffix} : Nat :=\n  42",
@@ -1019,7 +1015,7 @@ def run_iteration(client, suffix):
         "lean_run_at",
         {
             "path": "PositionEmptyLine.lean",
-            "version": version,
+            "snapshot": snapshot,
             "line": 1,
             "character": 0,
             "text": f"def mcpBroken{suffix} : Nat := \"bad\"",
@@ -1032,7 +1028,7 @@ def run_iteration(client, suffix):
         "lean_run_at_handle",
         {
             "path": "PositionEmptyLine.lean",
-            "version": version,
+            "snapshot": snapshot,
             "line": 1,
             "character": 0,
             "text": f"def mcpBase{suffix} : Nat := 1",
@@ -1070,14 +1066,14 @@ def run_iteration(client, suffix):
     client.call_tool("lean_release", {"path": "PositionEmptyLine.lean", "handle": base_handle})
 
     goal_update = client.call_tool("lean_update", {"path": "GoalSmoke.lean"})
-    goal_version = goal_update.get("version")
-    require(isinstance(goal_version, int), f"GoalSmoke update did not return a version: {goal_update}")
+    goal_snapshot = goal_update.get("snapshot")
+    require(isinstance(goal_snapshot, str), f"GoalSmoke update did not return a snapshot: {goal_update}")
 
     ascription = client.call_tool(
         "lean_run_at_handle",
         {
             "path": "GoalSmoke.lean",
-            "version": goal_version,
+            "snapshot": goal_snapshot,
             "line": 1,
             "character": 2,
             "text": "have htest := (Nat.succ : Nat)",
@@ -1092,7 +1088,7 @@ def run_iteration(client, suffix):
 
     goals_prev = client.call_tool(
         "lean_goals",
-        {"path": "GoalSmoke.lean", "version": goal_version, "line": 1, "character": 2, "mode": "before"},
+        {"path": "GoalSmoke.lean", "snapshot": goal_snapshot, "line": 1, "character": 2, "mode": "before"},
     )
     prev_goals = goals_prev.get("goals")
     require(isinstance(prev_goals, list) and prev_goals, f"goals before returned no goals: {goals_prev}")
@@ -1100,13 +1096,13 @@ def run_iteration(client, suffix):
 
     goals_after = client.call_tool(
         "lean_goals",
-        {"path": "GoalSmoke.lean", "version": goal_version, "line": 1, "character": 2, "mode": "after"},
+        {"path": "GoalSmoke.lean", "snapshot": goal_snapshot, "line": 1, "character": 2, "mode": "after"},
     )
     require(goals_after.get("goals") == [], f"goals after should return no goals: {goals_after}")
 
     client.call_tool("lean_close", {"path": "PositionEmptyLine.lean"})
     refreshed = client.call_tool("lean_refresh", {"path": "PositionEmptyLine.lean"})
-    require(isinstance(refreshed.get("version"), int), f"lean_refresh did not return a version: {refreshed}")
+    require(isinstance(refreshed.get("snapshot"), str), f"lean_refresh did not return a snapshot: {refreshed}")
     require("diagnostics" in refreshed, f"lean_refresh did not return diagnostic counts: {refreshed}")
     require("readiness" in refreshed, f"lean_refresh did not return readiness: {refreshed}")
     client.call_tool("lean_close", {"path": "PositionEmptyLine.lean"})
@@ -1765,8 +1761,8 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
         try:
             client.initialize()
             update = client.call_tool("lean_update", {"path": "McpConcurrency.lean"})
-            version = update.get("version")
-            require(isinstance(version, int), f"concurrency update missing version: {update}")
+            snapshot = update.get("snapshot")
+            require(isinstance(snapshot, str), f"concurrency update missing snapshot: {update}")
             other_update = client.call_tool(
                 "lean_update",
                 {
@@ -1774,10 +1770,10 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
                     "path": "McpConcurrency.lean",
                 },
             )
-            other_version = other_update.get("version")
+            other_snapshot = other_update.get("snapshot")
             require(
-                isinstance(other_version, int),
-                f"cross-workspace concurrency update missing version: {other_update}",
+                isinstance(other_snapshot, str),
+                f"cross-workspace concurrency update missing snapshot: {other_update}",
             )
             source_lines = (project_root / "McpConcurrency.lean").read_text(encoding="utf-8").splitlines()
             line = source_lines.index("  trivial")
@@ -1785,7 +1781,7 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
                 "name": "lean_run_at",
                 "arguments": {
                     "path": "McpConcurrency.lean",
-                    "version": version,
+                    "snapshot": snapshot,
                     "line": line,
                     "character": 2,
                     "text": "mcp_concurrency_gate",
@@ -1795,7 +1791,7 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
                 "name": "lean_run_at",
                 "arguments": {
                     "path": "McpConcurrency.lean",
-                    "version": version,
+                    "snapshot": snapshot,
                     "line": line,
                     "character": 2,
                     "text": "exact trivial",
@@ -1806,7 +1802,7 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
                 "arguments": {
                     "workspace": workspace_descriptor(other_project_root),
                     "path": "McpConcurrency.lean",
-                    "version": other_version,
+                    "snapshot": other_snapshot,
                     "line": line,
                     "character": 2,
                     "text": "exact trivial",
@@ -2077,12 +2073,12 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
                 isinstance(post_drop_update, dict),
                 f"post-drop concurrency update missing structured content: {post_drop_result}",
             )
-            version = post_drop_update.get("version")
+            snapshot = post_drop_update.get("snapshot")
             require(
-                isinstance(version, int),
-                f"post-drop concurrency update missing version: {post_drop_update}",
+                isinstance(snapshot, str),
+                f"post-drop concurrency update missing snapshot: {post_drop_update}",
             )
-            slow_params["arguments"]["version"] = version
+            slow_params["arguments"]["snapshot"] = snapshot
 
             started_path.unlink()
             release_path.unlink()
@@ -2163,14 +2159,14 @@ def run_concurrent_dispatch(repo_root, fixture_root, timeout, server_trace=False
             require_modern_result_envelope(update_result, "modern cancellation update")
             update = update_result.get("structuredContent")
             require(isinstance(update, dict), f"modern cancellation update has no result: {update_result}")
-            version = update.get("version")
-            require(isinstance(version, int), f"modern cancellation update missing version: {update}")
+            snapshot = update.get("snapshot")
+            require(isinstance(snapshot, str), f"modern cancellation update missing snapshot: {update}")
             modern_slow_params = with_modern_metadata(
                 {
                     "name": "lean_run_at",
                     "arguments": {
                         "path": "McpConcurrency.lean",
-                        "version": version,
+                        "snapshot": snapshot,
                         "line": line,
                         "character": 2,
                         "text": "mcp_concurrency_gate",
@@ -2318,8 +2314,8 @@ def run_concurrent_first_use(repo_root, fixture_root, timeout, server_trace=Fals
                 structured = result.get("structuredContent")
                 require(isinstance(structured, dict), f"concurrent first-use update missing content: {result}")
                 require(
-                    isinstance(structured.get("version"), int),
-                    f"concurrent first-use update missing version: {structured}",
+                    isinstance(structured.get("snapshot"), str),
+                    f"concurrent first-use update missing snapshot: {structured}",
                 )
             stats = client.call_tool("beam_stats")
             lean_stats = (
@@ -2362,8 +2358,8 @@ def run_concurrent_workspace_updates(client, roots, label):
             f"{label} request crossed workspace descriptors: {structured}",
         )
         require(
-            isinstance(structured.get("version"), int),
-            f"{label} update returned no version: {structured}",
+            isinstance(structured.get("snapshot"), str),
+            f"{label} update returned no snapshot: {structured}",
         )
 
 
@@ -2710,8 +2706,8 @@ def run_stateless_workspace_matrix(repo_root, fixture_root, timeout):
                 result_workspace_root(first_b, "first workspace B sync").resolve() == root_b.resolve(),
                 f"independent request did not lazily select workspace B: {first_b}",
             )
-            version_b = first_b.get("version")
-            require(isinstance(version_b, int), f"workspace B sync returned no version: {first_b}")
+            version_b = first_b.get("snapshot")
+            require(isinstance(version_b, str), f"workspace B sync returned no snapshot: {first_b}")
 
             stats = client.call_tool("beam_stats").get("workspaces", {})
             require(
@@ -2748,7 +2744,7 @@ def run_stateless_workspace_matrix(repo_root, fixture_root, timeout):
                 "lean_run_at_handle",
                 {
                     "path": "PositionEmptyLine.lean",
-                    "version": version_b,
+                    "snapshot": version_b,
                     "line": 1,
                     "character": 0,
                     "text": "def statelessWorkspaceBase : Nat := 1",
@@ -2946,13 +2942,13 @@ def run_cross_process_handle_rejection(repo_root, fixture_root, timeout):
         try:
             first.initialize()
             update = first.call_tool("lean_update", {"path": "PositionEmptyLine.lean"})
-            version = update.get("version")
-            require(isinstance(version, int), f"cross-process handle update returned no version: {update}")
+            snapshot = update.get("snapshot")
+            require(isinstance(snapshot, str), f"cross-process handle update returned no snapshot: {update}")
             minted = first.call_tool(
                 "lean_run_at_handle",
                 {
                     "path": "PositionEmptyLine.lean",
-                    "version": version,
+                    "snapshot": snapshot,
                     "line": 1,
                     "character": 0,
                     "text": "def crossProcessHandleBase : Nat := 1",