diff --git a/Beam/Broker/Backend/Lean.lean b/Beam/Broker/Backend/Lean.lean
index c6e35c21..4b55be08 100644
--- a/Beam/Broker/Backend/Lean.lean
+++ b/Beam/Broker/Backend/Lean.lean
@@ -30,7 +30,7 @@ def command (config : BrokerConfig) : IO (String × Array String × Array (Strin
   let some cmd := config.leanCmd?
     | throw <| IO.userError "missing Beam daemon --lean-cmd configuration"
   let plugin := ← pluginPath config
-  let lakeEnv ← leanServerLakeEnv config.root config.leanCmd?
+  let lakeEnv ← leanServerLakeEnv config.root config.leanCmd? config.leanLakeHelper?
   pure (
     cmd,
     #["--server"] ++ lakeEnv.moreServerArgs ++
diff --git a/Beam/Broker/Config.lean b/Beam/Broker/Config.lean
index 70c22b19..0f1efba1 100644
--- a/Beam/Broker/Config.lean
+++ b/Beam/Broker/Config.lean
@@ -12,6 +12,7 @@ structure BrokerConfig where
   root : System.FilePath
   leanCmd? : Option String := none
   leanPlugin? : Option System.FilePath := none
+  leanLakeHelper? : Option System.FilePath := none
   rocqCmd? : Option String := none
   deriving Inhabited, Repr
 
diff --git a/Beam/Broker/LakeEnv.lean b/Beam/Broker/LakeEnv.lean
index 5ccd2908..7e193594 100644
--- a/Beam/Broker/LakeEnv.lean
+++ b/Beam/Broker/LakeEnv.lean
@@ -8,9 +8,11 @@ import Lake.Config.Env
 import Lake.Config.InstallPath
 import Lake.CLI.Serve
 import Lake.Load.Workspace
+import Beam.Broker.LakeHelper
 
 open System
 open Std
+open Lean
 
 namespace Beam.Broker
 
@@ -41,6 +43,10 @@ private def computeLakeEnv (leanCmd? : Option String) : IO Lake.Env := do
   | .ok env => pure env
   | .error err => throw <| IO.userError s!"failed to compute Lake environment: {err}"
 
+/-- A `Workspace` contains live Lean values, so only load it across an exact Lean ABI match. -/
+private def canLoadWorkspaceInProcess (lakeEnv : Lake.Env) : Bool :=
+  !lakeEnv.lean.githash.isEmpty && lakeEnv.lean.githash == Lean.githash
+
 private def detectConfigFile? (root : FilePath) : IO (Option (FilePath × FilePath)) := do
   let leanConfig := root / "lakefile.lean"
   if ← leanConfig.pathExists then
@@ -74,31 +80,46 @@ private def loadWorkspaceWithConfig (root : FilePath) (lakeEnv : Lake.Env)
 
 private def loadWorkspaceFailureMessage
     (root : FilePath)
-    (messages : Array String)
-    (extra : Array String := #[]) : String :=
+    (messages : Array String) : String :=
   let lines :=
     #[s!"failed to load Lake workspace at {root}"] ++
-    (if messages.isEmpty then #[] else #["Lake log:"] ++ messages) ++
-    extra
+    (if messages.isEmpty then #[] else #["Lake log:"] ++ messages)
   String.intercalate "\n" lines.toList
 
-def loadWorkspaceForRoot (root : FilePath) (leanCmd? : Option String) : IO Workspace := do
+inductive WorkspaceLoadResult where
+  | loaded (workspace : Workspace)
+  | leanBuildMismatch
+
+def loadWorkspaceForRoot (root : FilePath) (leanCmd? : Option String) : IO WorkspaceLoadResult := do
   let (relConfigFile, configFile) ← detectConfigFile root
   let lakeEnv ← computeLakeEnv leanCmd?
+  unless canLoadWorkspaceInProcess lakeEnv do
+    return .leanBuildMismatch
   let (ws?, messages) ← loadWorkspaceWithConfig root lakeEnv relConfigFile configFile
   if let some ws := ws? then
-    pure ws
+    pure <| .loaded ws
   else
     throw <| IO.userError <| loadWorkspaceFailureMessage root messages
 
 structure LeanServerLakeEnv where
-  env : Array (String × Option String) := #[]
-  moreServerArgs : Array String := #[]
+  env : Array (String × Option String)
+  moreServerArgs : Array String
+  deriving FromJson, ToJson
 
-def leanServerLakeEnv (root : FilePath) (leanCmd? : Option String) : IO LeanServerLakeEnv := do
-  let some (relConfigFile, configFile) ← detectConfigFile? root
-    | pure {}
+private def leanServerLakeEnvInProcess
+    (root : FilePath)
+    (leanCmd? : Option String) : IO LeanServerLakeEnv := do
   let lakeEnv ← computeLakeEnv leanCmd?
+  -- Always preserve the target runtime environment: the Beam plugin links against target Lean/Lake
+  -- libraries even when there is no Lake configuration or this Lake version cannot load it.
+  let fallback : LeanServerLakeEnv := {
+    env := lakeEnv.vars
+    moreServerArgs := #[]
+  }
+  if !canLoadWorkspaceInProcess lakeEnv then
+    return fallback
+  let some (relConfigFile, configFile) ← detectConfigFile? root
+    | pure fallback
   let (ws?, messages) ← loadWorkspaceWithConfig root lakeEnv relConfigFile configFile
   if let some ws := ws? then
     pure {
@@ -107,8 +128,28 @@ def leanServerLakeEnv (root : FilePath) (leanCmd? : Option String) : IO LeanServ
     }
   else
     pure {
-      env := lakeEnv.baseVars.push (Lake.invalidConfigEnvVar, some <| String.intercalate "\n" messages.toList)
+      env := lakeEnv.vars.push
+        (Lake.invalidConfigEnvVar, some <| String.intercalate "\n" messages.toList)
       moreServerArgs := #[]
     }
 
+def leanServerLakeEnv
+    (root : FilePath)
+    (leanCmd? : Option String)
+    (lakeHelper? : Option FilePath := none) : IO LeanServerLakeEnv := do
+  match lakeHelper?, leanCmd? with
+  | some helper, some leanCmd =>
+      match ← runLakeHelper helper "server-env" <| toJson ({
+          root := root.toString
+          leanCmd
+        } : LakeHelperEnvRequest) with
+      | .ok result =>
+          match fromJson? result with
+          | .ok serverEnv => pure serverEnv
+          | .error err =>
+              throw <| IO.userError s!"target Lake helper returned an invalid server environment: {err}"
+      | .error failure => throw <| IO.userError failure.message
+  | _, _ =>
+      leanServerLakeEnvInProcess root leanCmd?
+
 end Beam.Broker
diff --git a/Beam/Broker/LakeHelper.lean b/Beam/Broker/LakeHelper.lean
new file mode 100644
index 00000000..86d483e3
--- /dev/null
+++ b/Beam/Broker/LakeHelper.lean
@@ -0,0 +1,100 @@
+/-
+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
+import Beam.Broker.Errors
+
+open Lean
+
+namespace Beam.Broker
+
+structure LakeHelperEnvRequest where
+  root : String
+  leanCmd : String
+  deriving FromJson, ToJson
+
+structure LakeHelperSaveRequest where
+  root : String
+  path : String
+  leanCmd : String
+  sourceHash : String
+  sourceMTimeSec : Int
+  sourceMTimeNsec : Nat
+  deriving FromJson, ToJson
+
+structure LakeHelperWriteTraceRequest where
+  oleanPath : String
+  oleanServerPath? : Option String := none
+  oleanPrivatePath? : Option String := none
+  ileanPath : String
+  irPath? : Option String := none
+  cPath : String
+  bcPath? : Option String := none
+  tracePath : String
+  traceMetadata : Json
+  deriving FromJson, ToJson
+
+structure LakeHelperSaveSpec extends LakeHelperWriteTraceRequest where
+  relPath : String
+  moduleName : String
+  unsupportedSetupReason? : Option String := none
+  deriving FromJson, ToJson
+
+def BrokerFailureCode.ofName? (name : String) : Option BrokerFailureCode :=
+  if name == "invalidParams" then some .invalidParams
+  else if name == "requestCancelled" then some .requestCancelled
+  else if name == "contentModified" then some .contentModified
+  else if name == "workerExited" then some .workerExited
+  else if name == syncBarrierIncompleteCode then some .syncBarrierIncomplete
+  else if name == saveTraceStaleCode then some .saveTraceStale
+  else if name == saveUnsupportedSetupCode then some .saveUnsupportedSetup
+  else if name == saveTargetNotModuleCode then some .saveTargetNotModule
+  else if name == "internalError" then some .internalError
+  else none
+
+private def helperOutputSummary (stdout stderr : String) : String :=
+  let stderr := stderr.trimAscii.toString
+  let stdout := stdout.trimAscii.toString
+  if !stderr.isEmpty then stderr else if !stdout.isEmpty then stdout else "(no output)"
+
+/-- Invoke a target-built helper without a shell and keep its structured failures typed. -/
+def runLakeHelper
+    (helper : System.FilePath)
+    (operation : String)
+    (request : Json) : IO (Except BrokerFailure Json) := do
+  let out ← IO.Process.output {
+    cmd := helper.toString
+    args := #["lake-helper", operation]
+  } (some request.compress)
+  if out.exitCode != 0 then
+    return .error {
+      code := .internalError
+      message :=
+        s!"target Lake helper '{operation}' exited with code {out.exitCode}: " ++
+          helperOutputSummary out.stdout out.stderr
+    }
+  let response ←
+    match Json.parse out.stdout >>= fromJson? (α := Response) with
+    | .ok response => pure response
+    | .error err =>
+        return .error {
+          code := .internalError
+          message :=
+            s!"target Lake helper '{operation}' returned invalid JSON: {err}: " ++
+              helperOutputSummary out.stdout out.stderr
+        }
+  match response with
+  | .successResult result _ => pure <| .ok result
+  | .errorResult failure =>
+      let error := failure.error
+      let some code := BrokerFailureCode.ofName? error.code
+        | return .error {
+            code := .internalError
+            message := s!"target Lake helper '{operation}' returned unknown error code '{error.code}'"
+          }
+      pure <| .error { code, message := error.message, data? := error.data? }
+
+end Beam.Broker
diff --git a/Beam/Broker/LakeHelperMain.lean b/Beam/Broker/LakeHelperMain.lean
new file mode 100644
index 00000000..34b3d10d
--- /dev/null
+++ b/Beam/Broker/LakeHelperMain.lean
@@ -0,0 +1,52 @@
+/-
+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 Beam.Broker.LakeEnv
+import Beam.Broker.LakeSave
+
+open Lean
+
+namespace Beam.Broker.LakeHelperMain
+
+private def readRequest [FromJson α] : IO α := do
+  let input ← (← IO.getStdin).readToEnd
+  let json ← IO.ofExcept <| Json.parse input
+  IO.ofExcept <| fromJson? json
+
+private def writeResponse (response : Response) : IO Unit := do
+  IO.println (toJson response).compress
+
+private def runServerEnv : IO Unit := do
+  let request : LakeHelperEnvRequest ← readRequest
+  let serverEnv ← leanServerLakeEnv
+    (System.FilePath.mk request.root) (some request.leanCmd)
+  writeResponse <| Response.success (toJson serverEnv)
+
+private def runPrepareSave : IO Unit := do
+  let request : LakeHelperSaveRequest ← readRequest
+  match ← lakeHelperSaveSpec request with
+  | .ok spec => writeResponse <| Response.success (toJson spec)
+  | .error failure => writeResponse failure.toResponse
+
+private def runWriteSaveTrace : IO Unit := do
+  let request : LakeHelperWriteTraceRequest ← readRequest
+  lakeHelperWriteLeanSaveTrace request
+  writeResponse <| Response.success (Json.mkObj [])
+
+def main (args : List String) : IO Unit := do
+  try
+    match args with
+    | ["server-env"] => runServerEnv
+    | ["prepare-save"] => runPrepareSave
+    | ["write-save-trace"] => runWriteSaveTrace
+    | _ => throw <| IO.userError "invalid target Lake helper operation"
+  catch error =>
+    writeResponse <| BrokerFailure.toResponse {
+      code := .internalError
+      message := error.toString
+    }
+
+end Beam.Broker.LakeHelperMain
diff --git a/Beam/Broker/LakeSave.lean b/Beam/Broker/LakeSave.lean
index 9b1c5870..f0f6db0d 100644
--- a/Beam/Broker/LakeSave.lean
+++ b/Beam/Broker/LakeSave.lean
@@ -15,6 +15,7 @@ import Lean.Elab.Term
 import Beam.Broker.Config
 import Beam.Broker.Errors
 import Beam.Broker.LakeEnv
+import Beam.Broker.LakeHelper
 import Beam.Path
 
 open Lean
@@ -56,9 +57,13 @@ elab "mkModuleOutputDescrsCompat(" isModule:term ", " olean:term ", " oleanServe
       bc? := $bc
     } : ModuleOutputDescrs))) none
 
+inductive LeanSaveTracePlan where
+  | inProcess (depTrace : BuildTrace)
+  | targetProcess (helper : FilePath) (request : LakeHelperWriteTraceRequest)
+
 structure LeanSaveSpec where
   relPath : String
-  moduleName : Name
+  moduleName : String
   unsupportedSetupReason? : Option String := none
   oleanPath : FilePath
   oleanServerPath? : Option FilePath := none
@@ -68,7 +73,7 @@ structure LeanSaveSpec where
   cPath : FilePath
   bcPath? : Option FilePath := none
   tracePath : FilePath
-  depTrace : BuildTrace
+  tracePlan : LeanSaveTracePlan
 
 structure SourceSnapshot where
   hash : Hash
@@ -156,14 +161,23 @@ private def buildDepTrace
           message := e.toString
         }
 
-def mkLeanSaveSpec
+private def mkLeanSaveSpecInProcess
     (root path : FilePath)
     (snapshot : SourceSnapshot)
     (leanCmd? : Option String := none) : IO (Except BrokerFailure LeanSaveSpec) := do
   try
     let root ← Beam.resolveExistingPath root
     let path ← Beam.resolvePathAgainstRoot root path
-    let ws ← loadWorkspaceForRoot root leanCmd?
+    let ws ←
+      match ← loadWorkspaceForRoot root leanCmd? with
+      | .loaded ws => pure ws
+      | .leanBuildMismatch =>
+          return .error {
+            code := .saveUnsupportedSetup
+            message :=
+              "lean-beam save requires the target and broker to use the same Lean build; " ++
+              "use lake build instead"
+          }
     let some mod := ws.findModuleBySrc? path
       | return .error {
           code := .saveTargetNotModule
@@ -179,7 +193,7 @@ def mkLeanSaveSpec
     let relPath := Beam.pathRelativeToRootOrSelf root path
     pure <| .ok {
       relPath
-      moduleName := mod.name
+      moduleName := mod.name.toString
       unsupportedSetupReason?
       oleanPath := mod.oleanFile
       oleanServerPath? := if isModule then some mod.oleanServerFile else none
@@ -189,7 +203,7 @@ def mkLeanSaveSpec
       cPath := mod.cFile
       bcPath? := if Lean.Internal.hasLLVMBackend () then some mod.bcFile else none
       tracePath := mod.traceFile
-      depTrace
+      tracePlan := .inProcess depTrace
     }
   catch e =>
     pure <| .error {
@@ -197,33 +211,91 @@ def mkLeanSaveSpec
       message := e.toString
     }
 
+private def decodeLakeHelperSaveSpec
+    (helper : FilePath)
+    (result : Json) : Except String LeanSaveSpec := do
+  let spec : LakeHelperSaveSpec ← fromJson? result
+  pure {
+    relPath := spec.relPath
+    moduleName := spec.moduleName
+    unsupportedSetupReason? := spec.unsupportedSetupReason?
+    oleanPath := FilePath.mk spec.oleanPath
+    oleanServerPath? := spec.oleanServerPath?.map FilePath.mk
+    oleanPrivatePath? := spec.oleanPrivatePath?.map FilePath.mk
+    ileanPath := FilePath.mk spec.ileanPath
+    irPath? := spec.irPath?.map FilePath.mk
+    cPath := FilePath.mk spec.cPath
+    bcPath? := spec.bcPath?.map FilePath.mk
+    tracePath := FilePath.mk spec.tracePath
+    tracePlan := .targetProcess helper spec.toLakeHelperWriteTraceRequest
+  }
+
+private def mkLeanSaveSpecWithHelper
+    (helper root path : FilePath)
+    (snapshot : SourceSnapshot)
+    (leanCmd : String) : IO (Except BrokerFailure LeanSaveSpec) := do
+  let request : LakeHelperSaveRequest := {
+    root := root.toString
+    path := path.toString
+    leanCmd
+    sourceHash := snapshot.hash.toString
+    sourceMTimeSec := snapshot.mtime.sec
+    sourceMTimeNsec := snapshot.mtime.nsec.toNat
+  }
+  match ← runLakeHelper helper "prepare-save" (toJson request) with
+  | .error failure => pure <| .error failure
+  | .ok result =>
+      match decodeLakeHelperSaveSpec helper result with
+      | .ok spec => pure <| .ok spec
+      | .error err =>
+          pure <| .error {
+            code := .internalError
+            message := s!"target Lake helper returned an invalid save specification: {err}"
+          }
+
+def mkLeanSaveSpec
+    (root path : FilePath)
+    (snapshot : SourceSnapshot)
+    (leanCmd? : Option String := none)
+    (lakeHelper? : Option FilePath := none) : IO (Except BrokerFailure LeanSaveSpec) := do
+  match lakeHelper?, leanCmd? with
+  | some helper, some leanCmd =>
+      mkLeanSaveSpecWithHelper helper root path snapshot leanCmd
+  | _, _ =>
+      mkLeanSaveSpecInProcess root path snapshot leanCmd?
+
 private def hashDescr (path : FilePath) (ext : String) : IO ArtifactDescr :=
   return artifactWithExt (← computeHash path) ext
 
-/-- Remove metadata for the prior artifact family before a new family can be published. -/
-def invalidateLeanSaveTrace (spec : LeanSaveSpec) : IO Unit := do
-  if ← spec.tracePath.isDir then
-    throw <| IO.userError s!"Lake save trace path is a directory: {spec.tracePath}"
-  if ← spec.tracePath.pathExists then
-    IO.FS.removeFile spec.tracePath
+private def leanSaveOutputs
+    (oleanPath : FilePath)
+    (oleanServerPath? oleanPrivatePath? : Option FilePath)
+    (ileanPath : FilePath)
+    (irPath? : Option FilePath)
+    (cPath : FilePath)
+    (bcPath? : Option FilePath) : IO ModuleOutputDescrs := do
+  let isModule := oleanServerPath?.isSome
+  let olean ← hashDescr oleanPath "olean"
+  let oleanServer? ← oleanServerPath?.mapM (fun path => hashDescr path "olean.server")
+  let oleanPrivate? ← oleanPrivatePath?.mapM (fun path => hashDescr path "olean.private")
+  let ilean ← hashDescr ileanPath "ilean"
+  let ir? ← irPath?.mapM (fun path => hashDescr path "ir")
+  let c ← hashDescr cPath "c"
+  let bc? ← bcPath?.mapM (fun path => hashDescr path "bc")
+  pure <| mkModuleOutputDescrsCompat(
+    isModule, olean, oleanServer?, oleanPrivate?, ilean, ir?, c, bc?)
 
-def writeLeanSaveTrace (spec : LeanSaveSpec) : IO Unit := do
-  let isModule := spec.oleanServerPath?.isSome
-  let olean ← hashDescr spec.oleanPath "olean"
-  let oleanServer? ← spec.oleanServerPath?.mapM (fun path => hashDescr path "olean.server")
-  let oleanPrivate? ← spec.oleanPrivatePath?.mapM (fun path => hashDescr path "olean.private")
-  let ilean ← hashDescr spec.ileanPath "ilean"
-  let ir? ← spec.irPath?.mapM (fun path => hashDescr path "ir")
-  let c ← hashDescr spec.cPath "c"
-  let bc? ← spec.bcPath?.mapM (fun path => hashDescr path "bc")
-  let outputs : ModuleOutputDescrs :=
-    mkModuleOutputDescrsCompat(isModule, olean, oleanServer?, oleanPrivate?, ilean, ir?, c, bc?)
+private def stagedTracePath (tracePath : FilePath) : IO FilePath := do
   let pid ← IO.Process.getPID
-  let stagedTrace :=
-    FilePath.mk s!"{spec.tracePath}.beam-save-trace-tmp-{pid}-{← IO.monoNanosNow}"
+  pure <| FilePath.mk s!"{tracePath}.beam-save-trace-tmp-{pid}-{← IO.monoNanosNow}"
+
+private def writeTraceAtomically
+    (tracePath : FilePath)
+    (writeStaged : FilePath → IO Unit) : IO Unit := do
+  let stagedTrace ← stagedTracePath tracePath
   try
-    writeBuildTrace stagedTrace spec.depTrace outputs {}
-    IO.FS.rename stagedTrace spec.tracePath
+    writeStaged stagedTrace
+    IO.FS.rename stagedTrace tracePath
   catch e =>
     try
       if ← stagedTrace.pathExists then
@@ -232,4 +304,85 @@ def writeLeanSaveTrace (spec : LeanSaveSpec) : IO Unit := do
       pure ()
     throw e
 
+/-- Remove metadata for the prior artifact family before a new family can be published. -/
+def invalidateLeanSaveTrace (spec : LeanSaveSpec) : IO Unit := do
+  if ← spec.tracePath.isDir then
+    throw <| IO.userError s!"Lake save trace path is a directory: {spec.tracePath}"
+  if ← spec.tracePath.pathExists then
+    IO.FS.removeFile spec.tracePath
+
+private def writeLeanSaveTraceWithMetadata
+    (request : LakeHelperWriteTraceRequest) : IO Unit := do
+  let metadata : BuildMetadata ← IO.ofExcept <| fromJson? request.traceMetadata
+  let outputs ← leanSaveOutputs
+    (FilePath.mk request.oleanPath)
+    (request.oleanServerPath?.map FilePath.mk)
+    (request.oleanPrivatePath?.map FilePath.mk)
+    (FilePath.mk request.ileanPath)
+    (request.irPath?.map FilePath.mk)
+    (FilePath.mk request.cPath)
+    (request.bcPath?.map FilePath.mk)
+  let metadata := { metadata with outputs? := some <| toJson outputs }
+  let tracePath := FilePath.mk request.tracePath
+  writeTraceAtomically tracePath fun stagedTrace =>
+    BuildMetadata.writeFile stagedTrace metadata
+
+def writeLeanSaveTrace (spec : LeanSaveSpec) : IO Unit := do
+  match spec.tracePlan with
+  | .inProcess depTrace =>
+      let outputs ← leanSaveOutputs spec.oleanPath spec.oleanServerPath?
+        spec.oleanPrivatePath? spec.ileanPath spec.irPath? spec.cPath spec.bcPath?
+      writeTraceAtomically spec.tracePath fun stagedTrace =>
+        writeBuildTrace stagedTrace depTrace outputs {}
+  | .targetProcess helper request =>
+      match ← runLakeHelper helper "write-save-trace" (toJson request) with
+      | .ok _ => pure ()
+      | .error failure => throw <| IO.userError failure.message
+
+def lakeHelperSaveSpec
+    (request : LakeHelperSaveRequest) : IO (Except BrokerFailure LakeHelperSaveSpec) := do
+  let some sourceHash := Hash.ofString? request.sourceHash
+    | return .error {
+        code := .invalidParams
+        message := "target Lake helper received an invalid source hash"
+      }
+  unless request.sourceMTimeNsec < UInt32.size do
+    return .error {
+      code := .invalidParams
+      message := "target Lake helper received an invalid source modification time"
+    }
+  let snapshot : SourceSnapshot := {
+    hash := sourceHash
+    mtime := { sec := request.sourceMTimeSec, nsec := request.sourceMTimeNsec.toUInt32 }
+  }
+  match ← mkLeanSaveSpecInProcess
+      (FilePath.mk request.root) (FilePath.mk request.path) snapshot (some request.leanCmd) with
+  | .error failure => pure <| .error failure
+  | .ok spec =>
+      let traceMetadata ←
+        match spec.tracePlan with
+        | .inProcess depTrace => pure <| toJson (BuildMetadata.ofBuild depTrace Json.null {})
+        | .targetProcess .. =>
+            return .error {
+              code := .internalError
+              message := "target Lake helper unexpectedly produced a delegated save trace"
+            }
+      pure <| .ok {
+        relPath := spec.relPath
+        moduleName := spec.moduleName
+        unsupportedSetupReason? := spec.unsupportedSetupReason?
+        oleanPath := spec.oleanPath.toString
+        oleanServerPath? := spec.oleanServerPath?.map (·.toString)
+        oleanPrivatePath? := spec.oleanPrivatePath?.map (·.toString)
+        ileanPath := spec.ileanPath.toString
+        irPath? := spec.irPath?.map (·.toString)
+        cPath := spec.cPath.toString
+        bcPath? := spec.bcPath?.map (·.toString)
+        tracePath := spec.tracePath.toString
+        traceMetadata
+      }
+
+def lakeHelperWriteLeanSaveTrace (request : LakeHelperWriteTraceRequest) : IO Unit :=
+  writeLeanSaveTraceWithMetadata request
+
 end Beam.Broker
diff --git a/Beam/Broker/Server.lean b/Beam/Broker/Server.lean
index 3f59fe08..93893e8d 100644
--- a/Beam/Broker/Server.lean
+++ b/Beam/Broker/Server.lean
@@ -1115,6 +1115,7 @@ private def brokerConfigSame (left right : BrokerConfig) : Bool :=
   left.root == right.root &&
     left.leanCmd? == right.leanCmd? &&
     left.leanPlugin? == right.leanPlugin? &&
+    left.leanLakeHelper? == right.leanLakeHelper? &&
     left.rocqCmd? == right.rocqCmd?
 
 private def detachBackendSession
@@ -1828,9 +1829,9 @@ private def saveOleanCore
   liftFailureIO <| ensureRequestNotCancelled cancelRef?
   let started ← liftHandlerIO <| startTrackedDiagnosticsBarrierIO server req path emitProgress?
     emitDiagnostic? (cancelRef? := cancelRef?)
-  let leanCmd? ← liftHandlerIO <| server.withState do
+  let (leanCmd?, lakeHelper?) ← liftHandlerIO <| server.withState do
     let workspace ← requireWorkspace req.workspaceId
-    pure workspace.config.leanCmd?
+    pure (workspace.config.leanCmd?, workspace.config.leanLakeHelper?)
   liftHandlerIO <| propagatePendingCancellation started.session cancelRef?
   let barrier ← awaitWaitForDiagnosticsBarrier
     s!"save_olean sync barrier clientRequestId={optionLabel req.clientRequestId?} uri={started.uri} version={started.version}"
@@ -1858,7 +1859,7 @@ private def saveOleanCore
       barrierOutcome.completionDiagnostics barrierProgress?
   let spec ← withFailureProgress barrierProgress? <| liftBrokerFailureIO <|
     mkLeanSaveSpec started.session.root path
-      { hash := started.textTraceHash, mtime := started.textMTime } leanCmd?
+      { hash := started.textTraceHash, mtime := started.textMTime } leanCmd? lakeHelper?
   let syncResult :=
     mkSyncFileResult spec.relPath started.version currentDiagnostics saveReadiness
   withFailureProgress barrierProgress? <|
diff --git a/Beam/Broker/ServerMain.lean b/Beam/Broker/ServerMain.lean
index 5ff009e2..2f9a7b9a 100644
--- a/Beam/Broker/ServerMain.lean
+++ b/Beam/Broker/ServerMain.lean
@@ -5,5 +5,9 @@ Author: Emilio J. Gallego Arias
 -/
 
 import Beam.Broker.Server
+import Beam.Broker.LakeHelperMain
 
-def main := Beam.Broker.main
+def main (args : List String) : IO Unit :=
+  match args with
+  | "lake-helper" :: helperArgs => Beam.Broker.LakeHelperMain.main helperArgs
+  | _ => Beam.Broker.main args
diff --git a/Beam/Broker/SyncSaveSupport.lean b/Beam/Broker/SyncSaveSupport.lean
index 04553334..8f6a27a8 100644
--- a/Beam/Broker/SyncSaveSupport.lean
+++ b/Beam/Broker/SyncSaveSupport.lean
@@ -245,7 +245,7 @@ def leanSaveResult
     (spec : LeanSaveSpec)
     (sourceHash : Lake.Hash)
     (sync : SyncFileResult) : SaveOleanResult := {
-  module := spec.moduleName.toString
+  module := spec.moduleName
   sourceHash := sourceHash.toString
   olean := spec.oleanPath.toString
   ilean := spec.ileanPath.toString
diff --git a/Beam/Cli/Info.lean b/Beam/Cli/Info.lean
index 47d52f9a..e2c24183 100644
--- a/Beam/Cli/Info.lean
+++ b/Beam/Cli/Info.lean
@@ -248,6 +248,7 @@ def printMcpConfig (home : System.FilePath) (opts : CliOptions) : IO Unit := do
     ("root", toJson root.toString),
     ("lean_cmd", toJson leanCmd),
     ("lean_plugin", toJson plugin.toString),
+    ("lean_lake_helper", toJson desired.daemonBin.toString),
     ("toolchain", toJson desired.toolchain?),
     ("bundle_id", toJson desired.bundleId)
   ]
diff --git a/Beam/Mcp/Options.lean b/Beam/Mcp/Options.lean
index 3ea4ce0c..d324d000 100644
--- a/Beam/Mcp/Options.lean
+++ b/Beam/Mcp/Options.lean
@@ -15,8 +15,8 @@ structure Options where
 
 def usage : String :=
   String.intercalate "\n" [
-    "usage: lean-beam-mcp [--beam-cli PATH] [--lean-cmd CMD] [--lean-plugin PATH]",
-    "       lean-beam-mcp [--beam-cli PATH] --self-check <lean-file>",
+    "usage: lean-beam-mcp [--beam-cli PATH | --lean-cmd CMD --lean-plugin PATH]",
+    "       lean-beam-mcp [--beam-cli PATH | --lean-cmd CMD --lean-plugin PATH] --self-check <lean-file>",
     "       lean-beam-mcp --version",
     "",
     "Runs the experimental Lean Beam MCP server over newline-delimited JSON-RPC on stdio.",
diff --git a/Beam/Mcp/Runtime.lean b/Beam/Mcp/Runtime.lean
index a1b3ea2c..4777a58b 100644
--- a/Beam/Mcp/Runtime.lean
+++ b/Beam/Mcp/Runtime.lean
@@ -22,6 +22,19 @@ structure Options where
 private structure LeanRuntimeConfig where
   leanCmd : String
   leanPlugin : System.FilePath
+  leanLakeHelper : System.FilePath
+
+private def inferLakeHelper (leanPlugin : System.FilePath) : IO (Except String System.FilePath) := do
+  let some pluginDir := leanPlugin.parent
+    | return .error s!"--lean-plugin has no parent directory: {leanPlugin}"
+  let buildHelper? := pluginDir.parent.map fun buildDir => buildDir / "bin" / "beam-daemon"
+  let candidates := #[some (pluginDir / "beam-daemon"), buildHelper?].filterMap id
+  for candidate in candidates do
+    if ← candidate.pathExists then
+      return .ok (← Beam.resolveExistingPath candidate)
+  pure <| .error <|
+    s!"could not locate the target Lake helper for --lean-plugin {leanPlugin}; expected " ++
+      String.intercalate " or " (candidates.map (·.toString)).toList
 
 private def processOutputSummary (stdout stderr : String) : String :=
   let stderr := stderr.trimAscii.toString
@@ -37,7 +50,12 @@ private def parseCliMcpConfig (text : String) : Except String LeanRuntimeConfig
   let json ← Json.parse text
   let leanCmd ← json.getObjValAs? String "lean_cmd"
   let leanPluginText ← json.getObjValAs? String "lean_plugin"
-  pure { leanCmd, leanPlugin := System.FilePath.mk leanPluginText }
+  let leanLakeHelperText ← json.getObjValAs? String "lean_lake_helper"
+  pure {
+    leanCmd
+    leanPlugin := System.FilePath.mk leanPluginText
+    leanLakeHelper := System.FilePath.mk leanLakeHelperText
+  }
 
 private def resolveFromBeamCli (beamCli : String) (root : System.FilePath) : IO (Except String LeanRuntimeConfig) := do
   let out ← IO.Process.output {
@@ -50,30 +68,36 @@ private def resolveFromBeamCli (beamCli : String) (root : System.FilePath) : IO
     match parseCliMcpConfig out.stdout with
     | .error err => pure <| .error s!"{beamCli} mcp-config returned invalid JSON: {err}"
     | .ok config => do
-        let plugin ← Beam.resolveExistingPath config.leanPlugin
-        pure <| .ok { config with leanPlugin := plugin }
+        try
+          let plugin ← Beam.resolveExistingPath config.leanPlugin
+          let lakeHelper ← Beam.resolveExistingPath config.leanLakeHelper
+          pure <| .ok { config with leanPlugin := plugin, leanLakeHelper := lakeHelper }
+        catch e =>
+          pure <| .error s!"{beamCli} mcp-config returned an unusable runtime path: {e}"
 
 private def resolveLeanRuntime (opts : Options) (root : System.FilePath) : IO (Except RpcError LeanRuntimeConfig) := do
-  let explicitPlugin? ←
-    try
-      opts.leanPlugin?.mapM (fun path => Beam.resolveExistingPath <| System.FilePath.mk path)
-    catch e =>
-      return .error <| runtimeSetupError <| leanPluginSetupError e.toString
-  match opts.leanCmd?, explicitPlugin? with
-  | some leanCmd, some leanPlugin =>
-      pure <| .ok { leanCmd, leanPlugin }
-  | _, _ =>
-      match opts.beamCli? with
-      | none =>
-          pure <| .error <| runtimeSetupError runtimeSetupGuidance
-      | some beamCli =>
-          match ← resolveFromBeamCli beamCli root with
-          | .error err => pure <| .error <| runtimeSetupError err
-          | .ok resolved =>
-              pure <| .ok {
-                leanCmd := opts.leanCmd?.getD resolved.leanCmd
-                leanPlugin := explicitPlugin?.getD resolved.leanPlugin
-              }
+  match opts.beamCli?, opts.leanCmd?, opts.leanPlugin? with
+  | none, some leanCmd, some leanPluginText =>
+      let leanPlugin ←
+        try
+          Beam.resolveExistingPath <| System.FilePath.mk leanPluginText
+        catch e =>
+          return .error <| runtimeSetupError <| leanPluginSetupError e.toString
+      match ← inferLakeHelper leanPlugin with
+      | .ok leanLakeHelper =>
+          pure <| .ok { leanCmd, leanPlugin, leanLakeHelper }
+      | .error err =>
+          pure <| .error <| runtimeSetupError err
+  | some beamCli, none, none =>
+      match ← resolveFromBeamCli beamCli root with
+      | .error err => pure <| .error <| runtimeSetupError err
+      | .ok resolved => pure <| .ok resolved
+  | none, none, none =>
+      pure <| .error <| runtimeSetupError runtimeSetupGuidance
+  | _, _, _ =>
+      pure <| .error <| runtimeSetupError <|
+        "choose exactly one Lean runtime source: --beam-cli PATH, or " ++
+          "--lean-cmd CMD with --lean-plugin PATH"
 
 def mkBrokerConfig (opts : Options) (root : System.FilePath) : IO (Except RpcError Beam.Broker.BrokerConfig) := do
   let root ←
@@ -89,6 +113,7 @@ def mkBrokerConfig (opts : Options) (root : System.FilePath) : IO (Except RpcErr
         root := root
         leanCmd? := some runtime.leanCmd
         leanPlugin? := some runtime.leanPlugin
+        leanLakeHelper? := some runtime.leanLakeHelper
       }
 
 end Beam.Mcp.Runtime
diff --git a/docs/DEVELOPMENT.md b/docs/DEVELOPMENT.md
index c4775feb..17ae91f4 100644
--- a/docs/DEVELOPMENT.md
+++ b/docs/DEVELOPMENT.md
@@ -222,9 +222,10 @@ Keep these stdio invariants explicit:
 - JSON-RPC envelopes and current-method parameter objects reject undeclared fields; protocol
   extensions belong in `_meta` or in a deliberately versioned schema change
 
-The installed wrapper passes the matching `beam-cli`; on lazy first use, `Beam.Mcp.Runtime` runs
-`beam-cli` with the canonical root to obtain `mcp-config`. Keep bundle selection in that narrow
-CLI/runtime boundary. Clients supply descriptors, not raw commands or plugin paths.
+The installed wrapper passes the matching `beam-cli`; on lazy first use, `Beam.Mcp.Runtime` obtains
+one Lean command/plugin/helper runtime from `beam-cli --root <root> mcp-config`. Keep bundle
+selection in that narrow boundary: do not accept either explicit runtime flag alone or mix bundle
+artifacts. Clients supply descriptors, not raw commands or plugin paths.
 
 When adding an MCP-facing operation:
 
diff --git a/docs/MCP.md b/docs/MCP.md
index 12f6e3a9..8b80af57 100644
--- a/docs/MCP.md
+++ b/docs/MCP.md
@@ -113,11 +113,16 @@ local descriptor as a sandbox.
 The installed `bin/lean-beam-mcp` wrapper is the public setup path. It pairs the MCP executable with
 the matching installed `beam-cli` and passes `--beam-cli`. On first use of a canonical root,
 [Beam/Mcp/Runtime.lean](../Beam/Mcp/Runtime.lean) asks
-`beam-cli --root <root> mcp-config` for the project-specific Lean command and runAt plugin.
+`beam-cli --root <root> mcp-config` for the project-specific Lean command, runAt plugin, and
+target-built Lake helper. The helper exchanges only JSON metadata with the MCP broker, so workspace
+configuration and zero-build save traces remain owned by the selected Lean/Lake build even when the
+MCP executable itself was built with a different Lean commit.
 
 Keep bundle resolution in this CLI/runtime boundary. Normal MCP clients should pass the workspace
-descriptor, not raw Lean commands or plugin paths. Direct developer runs may still pass
-`--lean-cmd` and `--lean-plugin` explicitly.
+descriptor, not raw Lean commands or plugin paths. Source-tree tests and direct developer runs may
+instead pass `--lean-cmd` and `--lean-plugin` together when the plugin has a sibling `beam-daemon` in
+the standard build or install layout. MCP rejects either explicit flag alone, combining
+`--beam-cli` with explicit runtime flags, and an explicit plugin without that sibling helper.
 
 `lean_drop_workspace` is optional cache management, not context selection. It evicts the runtime
 for its descriptor and invalidates proof handles owned by that runtime. Drop is idempotent and
diff --git a/docs/STATUS.md b/docs/STATUS.md
index 0dcb24ef..c23d7b61 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -165,6 +165,9 @@ Exact event ordering and examples live in
   must build and pass a local plugin load/elaboration probe for their exact fingerprint.
 - The supported fast path is the Lean toolchain pinned by this repository's `lean-toolchain`, because
   the plugin uses internal Lean APIs.
+- MCP sync, probe, `lean_save`, and `lean_close_save` operations can use a target runtime built from
+  a different Lean commit than the MCP server. The target bundle computes Lake server arguments and
+  authors save traces in its own process; live Lake workspace values never cross Lean builds.
 - The installer prebuilds the pinned validated toolchain by default and can prebuild additional
   validated, release-line-compatible, or explicitly custom toolchains; setup flags and offline notes live in
   [SETUP.md](SETUP.md).
diff --git a/docs/TESTING.md b/docs/TESTING.md
index a731d414..ca70d762 100644
--- a/docs/TESTING.md
+++ b/docs/TESTING.md
@@ -220,7 +220,7 @@ When investigating MCP stdio timeouts, prefer the focused descriptor-bound sync
 rerunning the full smoke suite:
 
 ```bash
-lake build Beam.LSP:shared lean-beam-mcp
+lake build Beam.LSP:shared beam-daemon lean-beam-mcp
 PYTHONDONTWRITEBYTECODE=1 python3 tests/test-mcp-stdio.py \
   --scenario progress-sync \
   --repro-runs 100 \
@@ -238,7 +238,7 @@ context, relevant CI and Lean thread env vars, the stderr tail, and a Beam/Lean
 For the same-process concurrency contract, run:
 
 ```bash
-lake build Beam.LSP:shared lean-beam-mcp
+lake build Beam.LSP:shared beam-daemon lean-beam-mcp
 PYTHONDONTWRITEBYTECODE=1 python3 tests/test-mcp-stdio.py \
   --scenario concurrent-dispatch \
   --timeout 40
diff --git a/tests/lean/BeamTest/Broker/McpProtocolTest.lean b/tests/lean/BeamTest/Broker/McpProtocolTest.lean
index e3f0c1f6..53560f7d 100644
--- a/tests/lean/BeamTest/Broker/McpProtocolTest.lean
+++ b/tests/lean/BeamTest/Broker/McpProtocolTest.lean
@@ -551,6 +551,58 @@ private def checkRuntimeSetupErrors : IO Unit := do
     catch _ =>
       pure ()
 
+  let projectRoot ← Beam.resolveExistingPath (← IO.currentDir)
+  let plugin ← BeamTest.TestHarness.pluginPath
+  match ← Beam.Mcp.Runtime.mkBrokerConfig {
+      leanCmd? := some "lean"
+      leanPlugin? := some plugin.toString
+    } projectRoot with
+  | .error err =>
+      throw <| IO.userError s!"explicit MCP runtime setup failed: {err.message}"
+  | .ok config =>
+      require "explicit MCP runtime should infer its sibling target Lake helper"
+        config.leanLakeHelper?.isSome
+
+  for (label, options) in #[
+      ("Lean command only", ({ beamCli? := some "unused", leanCmd? := some "lean" } : Beam.Mcp.Runtime.Options)),
+      ("Lean plugin only", ({ beamCli? := some "unused", leanPlugin? := some plugin.toString } : Beam.Mcp.Runtime.Options)),
+      ("beam-cli with explicit runtime", ({
+        beamCli? := some "unused"
+        leanCmd? := some "lean"
+        leanPlugin? := some plugin.toString
+      } : Beam.Mcp.Runtime.Options))
+    ] do
+    match ← Beam.Mcp.Runtime.mkBrokerConfig options projectRoot with
+    | .ok _ =>
+        throw <| IO.userError s!"{label} MCP runtime setup succeeded unexpectedly"
+    | .error err =>
+        require s!"{label} should be an invalidRequest error" (err.code == -32600)
+        require s!"{label} should reject mixed or partial runtime sources"
+          (err.message.contains "choose exactly one Lean runtime source")
+
+  let isolatedPluginDir :=
+    System.FilePath.mk s!"/tmp/lean-beam-mcp-plugin-without-helper-{← IO.monoNanosNow}"
+  try
+    IO.FS.createDirAll isolatedPluginDir
+    let isolatedPlugin := isolatedPluginDir / plugin.fileName.getD "beam-lsp-plugin"
+    IO.FS.writeFile isolatedPlugin "not loaded by this setup check\n"
+    match ← Beam.Mcp.Runtime.mkBrokerConfig {
+        leanCmd? := some "lean"
+        leanPlugin? := some isolatedPlugin.toString
+      } projectRoot with
+    | .ok _ =>
+        throw <| IO.userError "helperless explicit MCP runtime setup succeeded unexpectedly"
+    | .error err =>
+        require "helperless explicit MCP runtime should be an invalidRequest error" (err.code == -32600)
+        require "helperless explicit MCP runtime should name the target Lake helper"
+          (err.message.contains "could not locate the target Lake helper")
+  finally
+    try
+      if ← isolatedPluginDir.pathExists then
+        IO.FS.removeDirAll isolatedPluginDir
+    catch _ =>
+      pure ()
+
 private def expectResponse (label : String) (value : Option Json) : IO Json := do
   match value with
   | some json => pure json
diff --git a/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean b/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean
index 7cb3252f..99214acb 100644
--- a/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean
+++ b/tests/lean/BeamTest/Broker/StartupHandshakeTest.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Emilio J. Gallego Arias
 -/
 
+import Beam.Broker.LakeEnv
 import BeamTest.Broker.TestUtil
 import Lean
 
@@ -13,11 +14,31 @@ namespace BeamTest.Broker.StartupHandshakeTest
 
 open BeamTest.Broker.TestUtil
 
+private def checkWorkspaceFallbackEnv (root : System.FilePath) : IO Unit := do
+  let invalidRoot := root / "invalid-workspace"
+  IO.FS.createDirAll invalidRoot
+  IO.FS.writeFile (invalidRoot / "lakefile.lean") "this is not a valid Lake configuration\n"
+  let noConfigEnv ← Beam.Broker.leanServerLakeEnv root (some "lean")
+  let invalidConfigEnv ← Beam.Broker.leanServerLakeEnv invalidRoot (some "lean")
+  for serverEnv in #[noConfigEnv, invalidConfigEnv] do
+    let some (_, some loaderPath) := serverEnv.env.find? (·.1 == Lake.sharedLibPathEnvVar)
+      | throw <| IO.userError s!"expected backend environment variable {Lake.sharedLibPathEnvVar}"
+    if loaderPath.isEmpty then
+      throw <| IO.userError s!"expected nonempty backend environment variable {Lake.sharedLibPathEnvVar}"
+  if noConfigEnv.env.any (·.1 == Lake.invalidConfigEnvVar) then
+    throw <| IO.userError "plain Lean fallback unexpectedly marked Lake configuration invalid"
+  unless invalidConfigEnv.env.any (·.1 == Lake.invalidConfigEnvVar) do
+    throw <| IO.userError "invalid same-version Lake configuration should remain marked invalid"
+
+private def fakeLeanInstallProbe :=
+  "if [ \"${1:-}\" = \"--print-prefix\" ]; then exec lean --print-prefix; fi"
+
 private def writeResponseErrorServer (root : System.FilePath) : IO System.FilePath := do
   let script := root / "fake-lean-startup-response-error.sh"
   let body := String.intercalate "\n" [
     "#!/usr/bin/env bash",
     "set -euo pipefail",
+    fakeLeanInstallProbe,
     "printf '%s\\n' \"$$\" > \"$(dirname \"$0\")/fake-lean.pid\"",
     "frame() {",
     "  local body=\"$1\"",
@@ -56,6 +77,7 @@ private def writeAbruptExitServer (root : System.FilePath) : IO System.FilePath
   let body := String.intercalate "\n" [
     "#!/usr/bin/env bash",
     "set -euo pipefail",
+    fakeLeanInstallProbe,
     "python3 -c 'import sys; sys.stderr.buffer.write(b\"stderr-prefix-start\\n\" + bytes([0xc3, 0xa9]) * 10000 + b\"\\nAstderr-tail-marker\\n\")'",
     "exit 23"
   ] ++ "\n"
@@ -115,6 +137,7 @@ def main : IO Unit := do
   IO.FS.createDirAll root
   let plugin ← BeamTest.TestHarness.pluginPath
   try
+    checkWorkspaceFallbackEnv root
     let responseErrorServer ← writeResponseErrorServer root
     checkStartupFailure root responseErrorServer plugin "initialize failed" (checkPidGone := true)
     let abruptExitServer ← writeAbruptExitServer root
diff --git a/tests/test-beam-install.sh b/tests/test-beam-install.sh
index 905371a0..866e74db 100644
--- a/tests/test-beam-install.sh
+++ b/tests/test-beam-install.sh
@@ -1477,12 +1477,16 @@ payload = json.loads(os.environ["MCP_CONFIG_JSON"])
 expected_toolchain = os.environ["EXPECTED_TOOLCHAIN"]
 lean_cmd = payload.get("lean_cmd")
 lean_plugin = payload.get("lean_plugin")
+lean_lake_helper = payload.get("lean_lake_helper")
 if not isinstance(lean_cmd, str) or not lean_cmd:
     print(f"mcp-config did not return a lean_cmd: {payload}", file=sys.stderr)
     sys.exit(1)
 if not isinstance(lean_plugin, str) or not Path(lean_plugin).is_file():
     print(f"mcp-config did not return an existing lean_plugin: {payload}", file=sys.stderr)
     sys.exit(1)
+if not isinstance(lean_lake_helper, str) or not Path(lean_lake_helper).is_file():
+    print(f"mcp-config did not return an existing lean_lake_helper: {payload}", file=sys.stderr)
+    sys.exit(1)
 if payload.get("toolchain") != expected_toolchain:
     print(f"mcp-config returned unexpected toolchain: {payload}", file=sys.stderr)
     sys.exit(1)
diff --git a/tests/test-mcp-conformance.sh b/tests/test-mcp-conformance.sh
index 18e4dd2d..690768fd 100644
--- a/tests/test-mcp-conformance.sh
+++ b/tests/test-mcp-conformance.sh
@@ -93,7 +93,7 @@ start_bridge() {
   bridge_url="$(wait_for_ready_url "$ready_file")" || return
 }
 
-run_step "build MCP server" lake build Beam.LSP:shared lean-beam-mcp
+run_step "build MCP server" lake build Beam.LSP:shared beam-daemon lean-beam-mcp
 mkdir -p "$npm_cache"
 
 scenarios="${MCP_CONFORMANCE_SCENARIOS:-server-initialize ping tools-list}"
diff --git a/tests/test-mcp-modern-sdk.sh b/tests/test-mcp-modern-sdk.sh
index 439f37b3..d113ab02 100755
--- a/tests/test-mcp-modern-sdk.sh
+++ b/tests/test-mcp-modern-sdk.sh
@@ -61,7 +61,7 @@ run_sdk_mode() {
     --mode "$mode"
 }
 
-run_step "build MCP server" lake build Beam.LSP:shared lean-beam-mcp
+run_step "build MCP server" lake build Beam.LSP:shared beam-daemon lean-beam-mcp
 run_step "install official MCP TypeScript client" install_sdk
 mkdir -p "$project_root"
 rsync -a --exclude='.beam/' tests/save_olean_project/ "$project_root"/
diff --git a/tests/test-mcp-stdio.py b/tests/test-mcp-stdio.py
index adcde7e4..c85c7727 100644
--- a/tests/test-mcp-stdio.py
+++ b/tests/test-mcp-stdio.py
@@ -2418,6 +2418,14 @@ def run_multi_toolchain_workspaces(repo_root, fixture_root, timeout, server_trac
         roots = [tmp_root / "fixture-toolchain", tmp_root / "current-toolchain"]
         for root in roots:
             copy_project_fixture(fixture_root, root)
+            lakefile = root / "lakefile.toml"
+            lakefile.write_text(
+                lakefile.read_text(encoding="utf-8").replace(
+                    "\n[[lean_lib]]",
+                    '\nmoreGlobalServerArgs = ["-Dpp.universes=true"]\n\n[[lean_lib]]',
+                ),
+                encoding="utf-8",
+            )
         (roots[1] / "lean-toolchain").write_text(current_toolchain + "\n", encoding="utf-8")
         expected_toolchains = [fixture_toolchain, current_toolchain]
         configs = [beam_cli_mcp_config(repo_root, root, timeout) for root in roots]
@@ -2428,6 +2436,31 @@ def run_multi_toolchain_workspaces(repo_root, fixture_root, timeout, server_trac
             )
             lean_cmd = config.get("lean_cmd")
             require(isinstance(lean_cmd, str) and lean_cmd, f"mcp-config omitted lean_cmd for {root}: {config}")
+            lake_helper = config.get("lean_lake_helper")
+            require(
+                isinstance(lake_helper, str) and Path(lake_helper).is_file(),
+                f"mcp-config omitted the target Lake helper for {root}: {config}",
+            )
+            helper_env = subprocess.run(
+                [lake_helper, "lake-helper", "server-env"],
+                input=json.dumps({"root": str(root), "leanCmd": lean_cmd}),
+                stdout=subprocess.PIPE,
+                stderr=subprocess.PIPE,
+                text=True,
+                encoding="utf-8",
+                timeout=timeout,
+                check=False,
+                cwd=str(root),
+            )
+            require(
+                helper_env.returncode == 0,
+                f"target Lake helper failed for {root}: {helper_env.stdout}{helper_env.stderr}",
+            )
+            helper_result = json.loads(helper_env.stdout).get("result", {})
+            require(
+                "-Dpp.universes=true" in helper_result.get("moreServerArgs", []),
+                f"target Lake helper omitted moreGlobalServerArgs for {root}: {helper_result}",
+            )
             version = subprocess.run(
                 [lean_cmd, "--version"],
                 stdout=subprocess.PIPE,
@@ -2450,6 +2483,10 @@ def run_multi_toolchain_workspaces(repo_root, fixture_root, timeout, server_trac
             configs[0].get("lean_plugin") != configs[1].get("lean_plugin"),
             f"different toolchains resolved to the same Beam plugin: {configs}",
         )
+        require(
+            configs[0].get("lean_lake_helper") != configs[1].get("lean_lake_helper"),
+            f"different toolchains resolved to the same target Lake helper: {configs}",
+        )
 
         client = McpClient(
             repo_root,
@@ -2462,6 +2499,22 @@ def run_multi_toolchain_workspaces(repo_root, fixture_root, timeout, server_trac
         try:
             client.initialize()
             run_concurrent_workspace_updates(client, roots, "toolchain-first-use")
+            for root in roots:
+                saved = client.call_tool(
+                    "lean_save",
+                    {
+                        "path": "SaveSmoke/B.lean",
+                        "workspace": workspace_descriptor(root),
+                    },
+                )
+                require(
+                    saved.get("module") == "SaveSmoke.B",
+                    f"cross-toolchain save returned the wrong module for {root}: {saved}",
+                )
+                require(
+                    Path(saved.get("trace", "")).is_file(),
+                    f"cross-toolchain save did not publish a Lake trace for {root}: {saved}",
+                )
             require_active_lean_workspaces(client, roots, "multi-toolchain process")
         finally:
             client.close()