diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
index f2c68d904b..68e51992b0 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
@@ -56,9 +56,8 @@ object Tool extends LazyLogging {
     }
     _ <- Try(OutputManager.configure(initialization))
   } yield {
-    initialization.source.foreach(OutputManager.initSourceLines)
     println(s"Output directory: ${OutputManager.runDir.normalize()}")
-    OutputManager.withWriterInRunDir(OutputManager.Names.RunFile)(
+    OutputManager.withWriterInRunDir(OutputManager.RunFile)(
         _.println(s"${cmd.env} ${cmd.label} ${cmd.invocation}")
     )
 
@@ -70,7 +69,7 @@ object Tool extends LazyLogging {
     }
 
     // force our programmatic logback configuration, as the autoconfiguration works unpredictably
-    new LogbackConfigurator(OutputManager.runDirPathOpt, OutputManager.customRunDirPathOpt).configureDefaultContext()
+    new LogbackConfigurator(Some(OutputManager.runDir), OutputManager.additionalRunDir).configureDefaultContext()
     // TODO: update workers when the multicore branch is integrated
     logger.info(s"# APALACHE version: ${BuildInfo.version} | build: ${BuildInfo.build}")
 
@@ -164,7 +163,7 @@ object Tool extends LazyLogging {
   }
 
   // Execute the program specified by the subcommand cmd, handling errors as needed
-  private def runCommand(cmd: ApalacheCommand, config: ApalacheConfig): ExitCodes.TExitCode =
+  private def runCommand(cmd: ApalacheCommand, config: ApalacheConfig): ExitCodes.TExitCode = {
     try {
       cmd.run(config) match {
         case Left((errorCode, failMsg)) => { logger.info(failMsg); errorCode }
@@ -174,7 +173,9 @@ object Tool extends LazyLogging {
       case e: AdaptedException =>
         e.err match {
           case NormalErrorMessage(text) => logger.error(text)
-          case FailureMessage(text)     => { logger.error(text, e); generateBugReport(e, cmd) }
+          case FailureMessage(text)     =>
+            logger.error(text, e)
+            generateBugReport(e, cmd, config.source.flatMap(_.readUtf8.value))
         }
         ExitCodes.ERROR
 
@@ -185,9 +186,10 @@ object Tool extends LazyLogging {
 
       case e: Throwable =>
         logger.error("Unhandled exception", e)
-        generateBugReport(e, cmd)
+        generateBugReport(e, cmd, config.source.flatMap(_.readUtf8.value))
         ExitCodes.ERROR
     }
+  }
 
   private def printTimeDiff(startTime: LocalDateTime): Unit = {
     val endTime = LocalDateTime.now()
@@ -242,8 +244,9 @@ object Tool extends LazyLogging {
     }
   }
 
-  private def generateBugReport(e: Throwable, cmd: ApalacheCommand): Unit = {
+  private def generateBugReport(e: Throwable, cmd: ApalacheCommand, sourceText: Option[String]): Unit = {
     val absPath = ReportGenerator.prepareReportFile(
+        sourceText,
         cmd.invocation.split(" ").dropRight(1).mkString(" "),
         s"${BuildInfo.version} build ${BuildInfo.build}",
     )
diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TranspileCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TranspileCmd.scala
index fd18b693b0..bc8ffa5141 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TranspileCmd.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/TranspileCmd.scala
@@ -12,11 +12,7 @@ class TranspileCmd extends AbstractCheckerCmd(name = TRANSPILE, description = "T
 
   override def run(config: ApalacheConfig): Either[(TExitCode, String), String] = {
     runWithOptions(ApalacheConfigResolver.resolveCheck(config)) { options =>
-      val outFilePath = OutputManager.runDirPathOpt
-        .map { p =>
-          p.resolve(TlaExToVMTWriter.outFileName).toAbsolutePath
-        }
-        .getOrElse(TlaExToVMTWriter.outFileName)
+      val outFilePath = OutputManager.pathInRunDir(TlaExToVMTWriter.outFileName).toAbsolutePath
 
       PassChainExecutor(new ReTLAToVMTModule(options)).run() match {
         case Right(_)      => Right(s"VMT constraints successfully generated at\n$outFilePath")
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter/MetricProfilerListener.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter/MetricProfilerListener.scala
index 40d5c084bd..fc6ee32f65 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter/MetricProfilerListener.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter/MetricProfilerListener.scala
@@ -66,7 +66,7 @@ class MetricProfilerListener(sourceStore: SourceStore, changeListener: ChangeLis
 
     logger
       .info("%d profile entries to be found in %s".format(sortedEntries.size,
-              OutputManager.runDir.resolve(profileFileName)))
+              OutputManager.pathInRunDir(profileFileName)))
   }
 
   private def stringOfEntry(entry: (UID, SolverContextMetrics)): String = {
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala
index 14d5523095..c167c3f67c 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Cvc5SolverContext.scala
@@ -221,12 +221,7 @@ class Cvc5SolverContext(val config: SolverConfig) extends SolverContext with Laz
 
   private def initLogs(): Iterable[PrintWriter] = {
     val filePart = s"log$id.smt"
-    val writers =
-      if (OutputManager.isBound) {
-        (OutputManager.runDirPathOpt ++ OutputManager.customRunDirPathOpt).map(OutputManager.printWriter(_, filePart))
-      } else {
-        Iterable.empty
-      }
+    val writers = OutputManager.openLongLivedWritersInRunDirs(filePart)
 
     if (!config.debug) {
       writers.foreach { writer =>
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
index ee6fbd3811..22deef9d89 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
@@ -428,12 +428,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
    */
   private def initLogs(): Iterable[PrintWriter] = {
     val filePart = s"log$id.smt"
-    val writers =
-      if (OutputManager.isBound) {
-        (OutputManager.runDirPathOpt ++ OutputManager.customRunDirPathOpt).map(OutputManager.printWriter(_, filePart))
-      } else {
-        Iterable.empty
-      }
+    val writers = OutputManager.openLongLivedWritersInRunDirs(filePart)
 
     if (!config.debug) {
       writers.foreach { writer =>
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
index 80e8bb229c..50b7c6c43f 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/OutputManager.scala
@@ -1,270 +1,187 @@
 package at.forsyte.apalache.io
 
-import at.forsyte.apalache.io.config.{CommandInitializationOptions, CommonOptions}
-
-import java.io.File
-import java.io.FileWriter
-import java.io.PrintWriter
-import java.nio.file.Files
-import java.nio.file.Path
-import java.nio.charset.StandardCharsets
+import at.forsyte.apalache.io.config.CommandInitializationOptions
+
+import java.io.{IOException, PrintWriter}
+import java.lang.ScopedValue
+import java.nio.file.{Files, Path}
 import java.time.LocalDateTime
 import java.time.format.DateTimeFormatter
-import java.lang.ScopedValue
-import scala.jdk.CollectionConverters._
 
 /**
- * Mutable output state for one dynamically scoped tool invocation.
+ * Owns the output locations and writer lifecycle conventions for one Apalache execution.
+ *
+ * The workspace creates all configured directories during construction and mirrors run output to an additional run
+ * directory when requested. See
+ * [[https://github.com/apalache-mc/apalache/blob/main/docs/src/adr/009adr-outputs.md ADR-009]] for the output layout.
  */
-final private class OutputManagerState {
-  import OutputManager.Names._
-
-  private var commonOptions: Option[CommonOptions] = None
-  // outDirOpt is stored as an expanded and absolute path
-  private var outDirOpt: Option[Path] = None
-  // This should only be set if the IntermediateFlag is true
-  private var intermediateDirOpt: Option[Path] = None
-  // The run directory generated automatically inside the outDir
-  private var runDirOpt: Option[Path] = None
-  // The run directory that users can specify directly through CLI arguments
-  private var customRunDirOpt: Option[Path] = None
-
-  // For bug report templates as well as the next iteration of error messages, we will need to reference
-  // lines in the original input. This variable stores them.
-  private var sourceLinesOpt: Option[IndexedSeq[String]] = None
-
-  // Takes effect only when called on a source that is an existing .tla file or
-  // a string representing a .tla spec
-  def initSourceLines(source: InputSource): Unit =
-    if (sourceLinesOpt.isEmpty && source.exists) {
-      source match {
-        case InputSource.FileSource(path, _) =>
-          sourceLinesOpt = Some(Files.readAllLines(path, StandardCharsets.UTF_8).asScala.toIndexedSeq)
-        case value: InputSource.StringSource =>
-          sourceLinesOpt = Some(value.content.linesIterator.toIndexedSeq)
-      }
+final class OutputManager(initialization: CommandInitializationOptions) {
+  private val groupDir: Path = {
+    val groupName = initialization.source match {
+      case Some(InputSource.FileSource(path, _)) => path.getFileName.toString
+      case _                                     => initialization.command
     }
-
-  def getAllSrc: Option[String] = sourceLinesOpt.map { _.mkString("\n").trim }
-
-  private def setOutDir(base: Path, namespace: String): Unit = {
-    outDirOpt = Some(base.resolve(namespace).toAbsolutePath)
+    findOrCreateDir(initialization.common.outDir.resolve(groupName))
   }
 
-  /* This should only ever be set if the IntermediateFlag is true */
-  private def setIntermediateDir(): Unit = {
-    intermediateDirOpt = Some(runDir.resolve(IntermediateFoldername))
+  /** Unique persistent directory for this execution. */
+  val runDir: Path = {
+    val niceDate = LocalDateTime.now().format(DateTimeFormatter.ofPattern("yyyy-MM-dd"))
+    val niceTime = LocalDateTime.now().format(DateTimeFormatter.ofPattern("HH-mm-ss"))
+    Files.createTempDirectory(groupDir, s"${niceDate}T${niceTime}_")
   }
 
-  /** If this is FALSE, outputs (of any sort) cannot happen, so the tool should exit */
-  def isConfigured: Boolean = outDirOpt.nonEmpty
+  /** User-selected additional directory to which run output is mirrored. */
+  val additionalRunDir: Option[Path] = initialization.common.runDir.map(findOrCreateDir)
 
-  /** Accessor, read-only */
-  def runDirPathOpt: Option[Path] = runDirOpt
+  private val intermediateDirOpt: Option[Path] =
+    if (initialization.common.writeIntermediate) {
+      Some(findOrCreateDir(runDir.resolve(OutputManager.IntermediateDirName)))
+    } else {
+      None
+    }
 
-  /** Accessor, read-only */
-  def customRunDirPathOpt: Option[Path] = customRunDirOpt
+  private val additionalIntermediateDirOpt: Option[Path] =
+    intermediateDirOpt.flatMap(_ =>
+      additionalRunDir.map { path =>
+        findOrCreateDir(path.resolve(OutputManager.IntermediateDirName))
+      })
 
-  /**
-   * Accessor for the configured output directory.
-   *
-   * @throws java.lang.IllegalStateException
-   *   if called before OutputManager is configured: this is considered an implementator error
-   */
-  def outDir: Path = {
-    outDirOpt.getOrElse(throw new IllegalStateException("out-dir is not configured"))
-  }
+  /** Resolve `parts` relative to the primary run directory. */
+  def pathInRunDir(parts: String*): Path = parts.foldLeft(runDir)(_.resolve(_))
 
   /**
-   * Accessor for the configured run directory.
-   *
-   * @throws java.lang.IllegalStateException
-   *   if called before OutputManager is configured: this is considered an implementator error
+   * Open writers in the primary and additional run directories. The caller owns and must close every returned writer.
    */
-  def runDir: Path = {
-    runDirOpt.getOrElse(throw new IllegalStateException("run directory does not exist"))
-  }
+  def openLongLivedWritersInRunDirs(fileName: String): Iterable[PrintWriter] =
+    (Some(runDir) ++ additionalRunDir).map(dir => printWriter(dir.resolve(fileName)))
 
-  // The intermdiate output directory in the configured custom
-  // run directory
-  private def customIntermediateRunDir: Option[Path] = {
-    if (intermediateDirOpt.isEmpty) {
-      None
-    } else {
-      customRunDirOpt.map(_.resolve(IntermediateFoldername))
-    }
+  /** Write below each run directory and close each writer afterward. */
+  def withWriterInRunDir(parts: String*)(f: PrintWriter => Unit): Unit = {
+    withWriterAt(pathInRunDir(parts: _*))(f)
+    additionalRunDir.foreach(withWriterInJointPath(_, parts, f))
   }
 
-  private def ensureDirExists(path: Path): Unit = {
-    val f = path.toFile
-    if (!((f.exists() && f.isDirectory) || f.mkdirs())) {
-      throw new ConfigurationError(s"Could not find or create directory: ${f.getCanonicalPath}.")
+  /** Write below each intermediate directory when intermediate output is enabled. */
+  def withWriterInIntermediateDir(parts: String*)(f: PrintWriter => Unit): Unit = {
+    intermediateDirOpt.foreach { dir =>
+      withWriterInJointPath(dir, parts, f)
+      additionalIntermediateDirOpt.foreach(withWriterInJointPath(_, parts, f))
     }
   }
 
-  // Sets the customRunDir, if one is given, otherwise is noop
-  private def setCustomRunDir(pathOpt: Option[Path]): Unit = {
-    pathOpt.foreach { path =>
-      val dir = path.toAbsolutePath()
-      customRunDirOpt = Some(dir)
-      ensureDirExists(dir)
+  /** Write the rule-profiling report when profiling is enabled. */
+  def withProfilingWriter(f: PrintWriter => Unit): Boolean = {
+    if (initialization.common.profiling) {
+      withWriterInRunDir(OutputManager.RuleProfileFile)(f)
+      true
+    } else {
+      false
     }
   }
 
-  /** Configure output paths for a command. */
-  def configure(initialization: CommandInitializationOptions): Unit = {
-    commonOptions = Some(initialization.common)
-
-    val fileName = initialization.source match {
-      case Some(InputSource.FileSource(path, _)) => path.getFileName.toString
-      case Some(_: InputSource.StringSource)     => initialization.command
-      case None                                  => initialization.command
-    }
+  /** Write to an arbitrary path outside this workspace and close the writer afterward. */
+  def withWriterOutsideWorkspace(path: Path)(f: PrintWriter => Unit): Unit = withWriterAt(path)(f)
 
-    setOutDir(initialization.common.outDir, fileName)
-    ensureDirExists(outDir)
-    createRunDirectory()
-    setCustomRunDir(initialization.common.runDir)
+  private def printWriter(path: Path): PrintWriter = new PrintWriter(Files.newBufferedWriter(path))
 
-    if (initialization.common.writeIntermediate) {
-      setIntermediateDir()
-      intermediateDirOpt.foreach(ensureDirExists)
-      customIntermediateRunDir.foreach(ensureDirExists)
+  private def withWriterAt(path: Path)(f: PrintWriter => Unit): Unit = {
+    val writer = printWriter(path)
+    try {
+      f(writer)
+    } finally {
+      writer.close()
     }
   }
 
-  /* Inside `outputDirOpt`, create a directory for an individual run */
-  private def createRunDirectory(): Unit = {
-    val nicedate = LocalDateTime.now().format(DateTimeFormatter.ofPattern(s"yyyy-MM-dd"))
-    val nicetime = LocalDateTime.now().format(DateTimeFormatter.ofPattern(s"HH-mm-ss"))
-    // prefix for disambiguation
-    val rundir = Files.createTempDirectory(outDir, s"${nicedate}T${nicetime}_")
-    runDirOpt = Some(rundir)
+  private def withWriterInJointPath(dir: Path, parts: Seq[String], f: PrintWriter => Unit): Unit = {
+    val path = parts.foldLeft(dir)(_.resolve(_))
+    withWriterAt(path)(f)
   }
 
-  /** Create a PrintWriter to the file formed by appending `fileParts` to the `base` file */
-  def printWriter(base: File, fileParts: String*): PrintWriter = {
-    val file = fileParts.foldLeft(base)((file, part) => new File(file, part))
-    new PrintWriter(new FileWriter(file))
+  private def findOrCreateDir(path: Path): Path = {
+    val absolutePath = path.toAbsolutePath
+    try {
+      Files.createDirectories(absolutePath)
+    } catch {
+      case e: IOException =>
+        throw new ConfigurationError(s"Could not find or create directory $absolutePath: ${e.getMessage}")
+    }
   }
+}
 
-  /** Create a PrintWriter to the file formed by appending `fileParts` to the `base` file */
-  def printWriter(base: Path, fileParts: String*): PrintWriter = {
-    printWriter(base.toFile, fileParts: _*)
+/**
+ * Dynamically scoped access to the output workspace for the current tool invocation.
+ *
+ * A fresh scope starts without a configured workspace. [[configure]] installs one after command initialization has been
+ * resolved. [[captureScope]] and [[Scope.run]] propagate the same workspace state to another thread.
+ */
+object OutputManager {
+  final private class State {
+    var workspace: Option[OutputManager] = None
   }
 
-  /**
-   * Create a PrintWriter to the file formed by appending `fileParts` to the `base` file
-   *
-   * E.g., to create a writer to the file `foo/bar/bas.json`:
-   *
-   * val w = printWriter("foo", "bar", "baz.json")
-   */
-  def printWriter(base: String, fileParts: String*): PrintWriter = {
-    printWriter(Path.of(base), fileParts: _*)
+  final class Scope private[OutputManager] (private val state: State) {
+    def run[A](body: => A): A = withState(state)(body)
   }
 
-  /** Apply f to the writer w, being sure to close w */
-  private def withWriter(f: PrintWriter => Unit)(w: PrintWriter): Unit = {
-    try {
-      f(w)
-    } finally {
-      w.close()
-    }
-  }
+  private val currentState: ScopedValue[State] = ScopedValue.newInstance[State]()
 
-  def withWriterToFile(file: File)(f: PrintWriter => Unit): Unit = {
-    withWriter(f)(printWriter(file))
-  }
+  private[io] val IntermediateDirName = "intermediate"
+  val RunFile = "run.txt"
+  val RuleProfileFile = "profile-rules.txt"
 
-  /** Applies `f` to a PrintWriter created by appending the `parts` to the `runDir` */
-  def withWriterInRunDir(parts: String*)(f: PrintWriter => Unit): Boolean = {
-    val writeToDir: Path => Unit = dir => withWriter(f)(printWriter(dir, parts: _*))
-    runDirOpt.exists { runDir =>
-      writeToDir(runDir)
-      customRunDirOpt.foreach(writeToDir)
-      true
-    }
-  }
+  /** Run `body` with a fresh, initially unconfigured workspace scope. */
+  def withScope[A](body: => A): A = new Scope(new State).run(body)
 
-  /**
-   * Conditionally applies a function to a PrintWriter constructed relative to the intermediate directory
-   *
-   * @param parts
-   *   path parts describing a path relative to the intermediate directory (all parents must exist)
-   * @param f
-   *   a function that will be applied to the `PrintWriter`, if the `IntermediateFlag` is set.
-   * @return
-   *   `true` if the `IntermediateFlag` is true, and `f` can be applied to the PrintWriter created by appending the
-   *   `parts` to the intermediate output dir. Otherwise, `false`.
-   */
-  def withWriterInIntermediateDir(parts: String*)(f: PrintWriter => Unit): Boolean = {
-    val writeToDir: Path => Unit = dir => withWriter(f)(printWriter(dir, parts: _*))
-    intermediateDirOpt.exists { dir =>
-      writeToDir(dir)
-      customIntermediateRunDir.foreach(writeToDir)
-      true
-    }
-  }
+  /** Capture the current workspace scope for explicit propagation to another thread. */
+  def captureScope(): Scope = new Scope(state)
 
-  /**
-   * Conditionally write into "profile-rules.txt", depending on whether the `profiling` config is set
-   */
-  def withProfilingWriter(f: PrintWriter => Unit): Boolean = {
-    if (commonOptions.exists(_.profiling)) {
-      withWriterInRunDir("profile-rules.txt")(f)
-      true
-    } else {
-      false
-    }
+  /** Construct and install the workspace for the current scope. */
+  def configure(initialization: CommandInitializationOptions): Unit = {
+    state.workspace = Some(new OutputManager(initialization))
   }
 
-  /**
-   * Reads the contents of a file into a string
-   */
-  def readFileIntoString(file: File): String = {
-    Files.readString(file.toPath, StandardCharsets.UTF_8).trim
-  }
+  def runDir: Path = current.runDir
 
-  /**
-   * Calls `readFileIntoString` relative to the run directory
-   */
-  def readContentsOfFileInRunDir(filename: String): Option[String] = runDirPathOpt
-    .map { runDir =>
-      readFileIntoString(new File(runDir.toFile, filename))
-    }
-}
+  def additionalRunDir: Option[Path] = current.additionalRunDir
 
-/**
- * The OutputManager is the central source of truth for all IO-related locations. Its public methods are retained as a
- * compatibility facade, while each invocation stores its mutable state in a [[java.lang.ScopedValue]].
- *
- * Calls must run inside [[withScope]]. Code that hands work to another thread may use [[captureScope]] and
- * [[Scope.run]] to propagate the current manager explicitly.
- */
-object OutputManager {
+  def pathInRunDir(parts: String*): Path = current.pathInRunDir(parts: _*)
 
-  object Names {
-    val IntermediateFoldername = "intermediate"
-    val RunFile = "run.txt"
-  }
+  /** Optional output for components that may be used outside the tool runtime. */
+  def openLongLivedWritersInRunDirs(fileName: String): Iterable[PrintWriter] =
+    currentOption.map(_.openLongLivedWritersInRunDirs(fileName)).getOrElse(Iterable.empty)
 
-  final class Scope private[OutputManager] (private val state: OutputManagerState) {
-    def run[A](body: => A): A = withState(state)(body)
-  }
+  /** Optional output for components that may be used outside the tool runtime. */
+  def withWriterInRunDir(parts: String*)(f: PrintWriter => Unit): Boolean =
+    currentOption.exists { workspace =>
+      workspace.withWriterInRunDir(parts: _*)(f)
+      true
+    }
 
-  private val currentState: ScopedValue[OutputManagerState] = ScopedValue.newInstance[OutputManagerState]()
+  /** Optional output that is disabled until a workspace is configured and intermediate output is enabled. */
+  def withWriterInIntermediateDir(parts: String*)(f: PrintWriter => Unit): Unit =
+    currentOption.foreach(_.withWriterInIntermediateDir(parts: _*)(f))
 
-  /** Run `body` with a fresh output manager and restore the previous binding afterwards. */
-  def withScope[A](body: => A): A = new Scope(new OutputManagerState).run(body)
+  /** Optional output for components that may be used outside the tool runtime. */
+  def withProfilingWriter(f: PrintWriter => Unit): Boolean =
+    currentOption.exists(_.withProfilingWriter(f))
 
-  /** Capture the currently bound output manager for explicit propagation to another thread. */
-  def captureScope(): Scope = new Scope(current)
+  def withWriterOutsideWorkspace(path: Path)(f: PrintWriter => Unit): Unit =
+    current.withWriterOutsideWorkspace(path)(f)
 
-  /** Used by low-level components whose output logging is optional when they are used outside the tool runtime. */
-  private[apalache] def isBound: Boolean = currentState.isBound
+  private def currentOption: Option[OutputManager] =
+    if (currentState.isBound) currentState.get().workspace else None
 
-  private def current: OutputManagerState = {
+  private def current: OutputManager =
+    currentOption.getOrElse {
+      throw new IllegalStateException(
+          "OutputManager is not configured in the current scope; " +
+            "call OutputManager.withScope { OutputManager.configure(...) ... }"
+      )
+    }
+
+  private def state: State = {
     if (currentState.isBound) {
       currentState.get()
     } else {
@@ -275,46 +192,9 @@ object OutputManager {
   }
 
   // Carrier.run has the same JVM descriptor on Java 21 through Java 25. Carrier.call does not.
-  private def withState[A](state: OutputManagerState)(body: => A): A = {
+  private def withState[A](state: State)(body: => A): A = {
     var result: Option[A] = None
     ScopedValue.where(currentState, state).run(() => result = Some(body))
     result.get
   }
-
-  def initSourceLines(source: InputSource): Unit = current.initSourceLines(source)
-
-  def getAllSrc: Option[String] = current.getAllSrc
-
-  def isConfigured: Boolean = current.isConfigured
-
-  def runDirPathOpt: Option[Path] = current.runDirPathOpt
-
-  def customRunDirPathOpt: Option[Path] = current.customRunDirPathOpt
-
-  def outDir: Path = current.outDir
-
-  def runDir: Path = current.runDir
-
-  def configure(initialization: CommandInitializationOptions): Unit = current.configure(initialization)
-
-  def printWriter(base: File, fileParts: String*): PrintWriter = current.printWriter(base, fileParts: _*)
-
-  def printWriter(base: Path, fileParts: String*): PrintWriter = current.printWriter(base, fileParts: _*)
-
-  def printWriter(base: String, fileParts: String*): PrintWriter = current.printWriter(base, fileParts: _*)
-
-  def withWriterToFile(file: File)(f: PrintWriter => Unit): Unit = current.withWriterToFile(file)(f)
-
-  def withWriterInRunDir(parts: String*)(f: PrintWriter => Unit): Boolean =
-    current.withWriterInRunDir(parts: _*)(f)
-
-  def withWriterInIntermediateDir(parts: String*)(f: PrintWriter => Unit): Boolean =
-    current.withWriterInIntermediateDir(parts: _*)(f)
-
-  def withProfilingWriter(f: PrintWriter => Unit): Boolean =
-    currentState.isBound && current.withProfilingWriter(f)
-
-  def readFileIntoString(file: File): String = current.readFileIntoString(file)
-
-  def readContentsOfFileInRunDir(filename: String): Option[String] = current.readContentsOfFileInRunDir(filename)
 }
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala
index e0f132e662..a19c58aea5 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/ReportGenerator.scala
@@ -1,20 +1,22 @@
 package at.forsyte.apalache.io
 
-import java.io.File
+import java.nio.charset.StandardCharsets
+import java.nio.file.Files
 import java.util.regex.Matcher
 
 object ReportGenerator {
   private val reportFile = "BugReport.md"
-
-  private def getFileOrEmptyStr(filename: String) = OutputManager.readContentsOfFileInRunDir(filename).getOrElse("")
+  private val detailedLogFile = "detailed.log"
 
   def getLog(): String =
-    Matcher.quoteReplacement(getFileOrEmptyStr("detailed.log")) // handle $s in log
+    Matcher.quoteReplacement(
+        Files.readString(OutputManager.pathInRunDir(detailedLogFile), StandardCharsets.UTF_8).trim
+    ) // handle $s in log
 
   // Can't access Version or Command in IO, have to pass at call site
-  def prepareReportFile(cmdStr: String, versionStr: String): String = {
+  def prepareReportFile(sourceText: Option[String], cmdStr: String, versionStr: String): String = {
     val specTxt =
-      OutputManager.getAllSrc.map(spec => s"```\n$spec\n````").getOrElse("<!-- TLA+ specification not found. -->")
+      sourceText.map(spec => s"```\n${spec.trim}\n````").getOrElse("<!-- TLA+ specification not found. -->")
     val log = getLog()
     val os = System.getProperty("os.name")
     val jdk = System.getProperty("java.version")
@@ -25,7 +27,7 @@ object ReportGenerator {
       _.println(filledTemplate)
     }
 
-    new File(OutputManager.runDir.toFile, reportFile).getCanonicalPath
+    OutputManager.pathInRunDir(reportFile).toFile.getCanonicalPath
   }
 
   private def template(
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/CounterexampleWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/CounterexampleWriter.scala
index c61e57336b..f3e2353dea 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/CounterexampleWriter.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/CounterexampleWriter.scala
@@ -167,7 +167,7 @@ object CounterexampleWriter extends LazyLogging {
 
     fileNames.flatMap { case (kind, name) =>
       if (OutputManager.withWriterInRunDir(name)(writerHelper(kind))) {
-        Some(OutputManager.runDir.resolve(name).normalize.toString)
+        Some(OutputManager.pathInRunDir(name).normalize.toString)
       } else {
         None
       }
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriterFactory.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriterFactory.scala
index 20144ec643..7ed80e82b8 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriterFactory.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriterFactory.scala
@@ -40,7 +40,7 @@ trait TlaWriterFactory {
     )(module: TlaModule,
       extendedModuleNames: List[String]): Unit = {
     val writeHelper: (PrintWriter => Unit) => Unit = file match {
-      case Some(f) => OutputManager.withWriterToFile(f)
+      case Some(f) => OutputManager.withWriterOutsideWorkspace(f.toPath)
       case None    => OutputManager.withWriterInIntermediateDir(module.name + extension)
     }
     writeHelper(createWriter(_).write(module, extendedModuleNames))
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/TestOutputManager.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/TestOutputManager.scala
index a584b7f55e..9b10383eeb 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/TestOutputManager.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/TestOutputManager.scala
@@ -13,71 +13,99 @@ import scala.util.Using
 @RunWith(classOf[JUnitRunner])
 class TestOutputManager extends AnyFunSuite {
 
-  private case class Observation(outDir: Path, runDir: Path, source: String)
+  private case class Observation(runDir: Path, contents: String)
 
-  test("calls outside a scope fail with a useful error") {
-    val error = intercept[IllegalStateException](OutputManager.isConfigured)
+  test("required access outside a configured scope fails and optional output is disabled") {
+    val error = intercept[IllegalStateException](OutputManager.runDir)
     assert(error.getMessage.contains("OutputManager.withScope"))
     assert(!OutputManager.withProfilingWriter(_ => fail("unbound profiling writer should be disabled")))
-    assert(OutputManager.Names.RunFile == "run.txt")
+    assert(OutputManager.openLongLivedWritersInRunDirs("unbound.txt").isEmpty)
+    assert(!OutputManager.withWriterInRunDir("unbound.txt")(_ => fail("unbound run output is disabled")))
+    OutputManager.withWriterInIntermediateDir("unbound.txt")(_ => fail("unbound intermediate output is disabled"))
+    assert(OutputManager.RunFile == "run.txt")
   }
 
-  test("fresh scopes do not retain paths or source lines") {
-    withTempDirectory("output-manager-sequential") { root =>
-      val firstOut = root.resolve("first-out")
-      val firstCustom = root.resolve("first-custom")
-      val firstSource = InputSource.StringSource("---- MODULE First ----\n====")
+  test("a workspace owns and mirrors its filesystem output") {
+    withTempDirectory("output-workspace-filesystem") { root =>
+      val additional = root.resolve("additional")
+      val workspace = new OutputManager(
+          initialization(
+              "check",
+              root.resolve("out"),
+              Some(additional),
+              writeIntermediate = true,
+              profiling = true,
+          )
+      )
+
+      assert(workspace.runDir.getParent == root.resolve("out/check").toAbsolutePath)
+      assert(workspace.additionalRunDir.contains(additional.toAbsolutePath))
+      assert(workspace.pathInRunDir("nested", "file.txt") == workspace.runDir.resolve("nested/file.txt"))
+
+      workspace.withWriterInRunDir("result.txt")(_.print("result"))
+      assert(Files.readString(workspace.pathInRunDir("result.txt")) == "result")
+      assert(Files.readString(additional.resolve("result.txt")) == "result")
+
+      workspace.withWriterInIntermediateDir("intermediate.txt")(_.print("intermediate"))
+      assert(Files.readString(workspace.pathInRunDir("intermediate/intermediate.txt")) == "intermediate")
+      assert(Files.readString(additional.resolve("intermediate/intermediate.txt")) == "intermediate")
+
+      assert(workspace.withProfilingWriter(_.print("profile")))
+      assert(Files.readString(workspace.pathInRunDir(OutputManager.RuleProfileFile)) == "profile")
+
+      val external = root.resolve("external.txt")
+      workspace.withWriterOutsideWorkspace(external)(_.print("external"))
+      assert(Files.readString(external) == "external")
+
+      val longLivedWriters = workspace.openLongLivedWritersInRunDirs("long-lived.txt").toList
+      try {
+        longLivedWriters.foreach { writer =>
+          writer.print("long-lived")
+          writer.flush()
+        }
+        assert(Files.readString(workspace.pathInRunDir("long-lived.txt")) == "long-lived")
+        assert(Files.readString(additional.resolve("long-lived.txt")) == "long-lived")
+      } finally {
+        longLivedWriters.foreach(_.close())
+      }
 
-      OutputManager.withScope {
-        assert(!OutputManager.isConfigured)
-        assert(OutputManager.getAllSrc.isEmpty)
-        OutputManager
-          .configure(initialization("first", firstOut, Some(firstCustom), writeIntermediate = true, Some(firstSource)))
-        OutputManager.initSourceLines(firstSource)
-
-        assert(OutputManager.isConfigured)
-        assert(OutputManager.outDir == firstOut.resolve("first").toAbsolutePath)
-        assert(OutputManager.customRunDirPathOpt.contains(firstCustom.toAbsolutePath))
-        assert(OutputManager.getAllSrc.contains("---- MODULE First ----\n===="))
-        assert(OutputManager.withWriterInIntermediateDir("first.txt")(_.println("first")))
-        assert(OutputManager.withWriterInRunDir("result.txt")(_.println("first")))
-        assert(Files.exists(OutputManager.runDir.resolve("result.txt")))
-        assert(Files.exists(firstCustom.resolve("result.txt")))
+      val disabled = new OutputManager(initialization("disabled", root.resolve("out")))
+      disabled.withWriterInIntermediateDir("disabled.txt")(_ => fail("intermediate output should be disabled"))
+      assert(!disabled.withProfilingWriter(_ => fail("profiling should be disabled")))
+      assert(!Files.exists(disabled.pathInRunDir(OutputManager.IntermediateDirName)))
+    }
+  }
+
+  test("fresh scopes do not retain a previously configured workspace") {
+    withTempDirectory("output-workspace-sequential") { root =>
+      val firstRunDir = OutputManager.withScope {
+        OutputManager.configure(initialization("first", root.resolve("first-out")))
+        OutputManager.withWriterInRunDir("result.txt")(_.print("first"))
+        OutputManager.runDir
       }
 
-      val secondOut = root.resolve("second-out")
-      val secondSource = InputSource.StringSource("---- MODULE Second ----\n====")
       OutputManager.withScope {
-        assert(!OutputManager.isConfigured)
-        assert(OutputManager.runDirPathOpt.isEmpty)
-        assert(OutputManager.customRunDirPathOpt.isEmpty)
-        assert(OutputManager.getAllSrc.isEmpty)
-
-        OutputManager
-          .configure(initialization("second", secondOut, None, writeIntermediate = false, Some(secondSource)))
-        OutputManager.initSourceLines(secondSource)
-
-        assert(OutputManager.outDir == secondOut.resolve("second").toAbsolutePath)
-        assert(OutputManager.customRunDirPathOpt.isEmpty)
-        assert(OutputManager.getAllSrc.contains("---- MODULE Second ----\n===="))
-        assert(!OutputManager.withWriterInIntermediateDir("second.txt")(_ => ()))
+        intercept[IllegalStateException](OutputManager.runDir)
+        OutputManager.configure(initialization("second", root.resolve("second-out")))
+        assert(OutputManager.runDir != firstRunDir)
+        assert(!Files.exists(OutputManager.pathInRunDir("result.txt")))
       }
     }
   }
 
   test("nested and exceptional scopes restore the previous binding") {
-    withTempDirectory("output-manager-nested") { root =>
+    withTempDirectory("output-workspace-nested") { root =>
       OutputManager.withScope {
         OutputManager.configure(initialization("outer", root.resolve("outer")))
-        val outerDir = OutputManager.outDir
+        val outerDir = OutputManager.runDir
 
         OutputManager.withScope {
-          assert(!OutputManager.isConfigured)
+          intercept[IllegalStateException](OutputManager.runDir)
           OutputManager.configure(initialization("inner", root.resolve("inner")))
-          assert(OutputManager.outDir != outerDir)
+          assert(OutputManager.runDir != outerDir)
         }
 
-        assert(OutputManager.outDir == outerDir)
+        assert(OutputManager.runDir == outerDir)
       }
 
       intercept[RuntimeException] {
@@ -85,42 +113,36 @@ class TestOutputManager extends AnyFunSuite {
           throw new RuntimeException("boom")
         }
       }
-      intercept[IllegalStateException](OutputManager.isConfigured)
+      intercept[IllegalStateException](OutputManager.runDir)
     }
   }
 
   test("captured scopes isolate concurrent configuration and can be rebound on worker threads") {
-    withTempDirectory("output-manager-concurrent") { root =>
+    withTempDirectory("output-workspace-concurrent") { root =>
       val firstScope = OutputManager.withScope(OutputManager.captureScope())
       val secondScope = OutputManager.withScope(OutputManager.captureScope())
       val barrier = new CyclicBarrier(2)
       val executor = Executors.newFixedThreadPool(2)
 
-      def task(
-          scope: OutputManager.Scope,
-          command: String,
-          sourceText: String): Callable[Observation] =
+      def task(scope: OutputManager.Scope, command: String): Callable[Observation] =
         () =>
           scope.run {
-            val source = InputSource.StringSource(sourceText)
-            OutputManager.configure(initialization(command, root.resolve(s"$command-out"), source = Some(source)))
-            OutputManager.initSourceLines(source)
+            OutputManager.configure(initialization(command, root.resolve(s"$command-out")))
+            OutputManager.withWriterInRunDir("same.txt")(_.print(command))
             barrier.await()
-            Observation(OutputManager.outDir, OutputManager.runDir, OutputManager.getAllSrc.get)
+            Observation(OutputManager.runDir, Files.readString(OutputManager.pathInRunDir("same.txt")))
           }
 
       try {
-        val first = executor.submit(task(firstScope, "first", "---- MODULE First ----\n===="))
-        val second = executor.submit(task(secondScope, "second", "---- MODULE Second ----\n===="))
+        val first = executor.submit(task(firstScope, "first"))
+        val second = executor.submit(task(secondScope, "second"))
         val firstResult = first.get()
         val secondResult = second.get()
 
-        assert(firstResult.outDir == root.resolve("first-out/first").toAbsolutePath)
-        assert(secondResult.outDir == root.resolve("second-out/second").toAbsolutePath)
-        assert(firstResult.runDir.startsWith(firstResult.outDir))
-        assert(secondResult.runDir.startsWith(secondResult.outDir))
-        assert(firstResult.source.contains("MODULE First"))
-        assert(secondResult.source.contains("MODULE Second"))
+        assert(firstResult.runDir.startsWith(root.resolve("first-out/first").toAbsolutePath))
+        assert(secondResult.runDir.startsWith(root.resolve("second-out/second").toAbsolutePath))
+        assert(firstResult.contents == "first")
+        assert(secondResult.contents == "second")
       } finally {
         executor.shutdownNow()
       }
@@ -132,19 +154,19 @@ class TestOutputManager extends AnyFunSuite {
       outDir: Path,
       runDir: Option[Path] = None,
       writeIntermediate: Boolean = false,
-      source: Option[InputSource] = None): CommandInitializationOptions =
+      profiling: Boolean = false): CommandInitializationOptions =
     CommandInitializationOptions(
         command,
         CommonOptions(
             debug = false,
             features = Nil,
             outDir = outDir,
-            profiling = false,
+            profiling = profiling,
             runDir = runDir,
             smtprof = false,
             writeIntermediate = writeIntermediate,
         ),
-        source,
+        source = None,
     )
 
   private def withTempDirectory[A](prefix: String)(body: Path => A): A = {