diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index bd91dc4e..ff45ccf8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -242,6 +242,12 @@ jobs:
                   npx tsc --noEmit -p jsconfig.json
                   popd
 
+            - name: Type check the run-test widget JS code
+              run: |
+                  pushd src/errata/Errata/widget
+                  npx tsc --noEmit -p jsconfig.json
+                  popd
+
             - name: Check the ToC width storage key stays in sync
               run: |
                   # toc-resize.js and toc-resize-preload.js must agree on the localStorage
diff --git a/doc/UsersGuide/Releases/Entries/TestFramework.lean b/doc/UsersGuide/Releases/Entries/TestFramework.lean
index 92c744e7..13e988e7 100644
--- a/doc/UsersGuide/Releases/Entries/TestFramework.lean
+++ b/doc/UsersGuide/Releases/Entries/TestFramework.lean
@@ -13,7 +13,7 @@ release_note
   version := ⟨4, 34, 0⟩
   breaking := false
   tag := "feat-test-framework"
-  prs := [956, 957]
+  prs := [956, 957, 959]
 
 #doc (Manual) "Test Framework" =>
 
@@ -31,3 +31,5 @@ The test runner discovers every test in the package; it can restrict the run to
 Elaboration-time tests can be written with `#test_msgs` and `#test_guard`, variants of `#guard_msgs` and `#guard` that run their check at compile time and record the outcome as a test case, reported together with the rest of the suite.
 
 Verso's own test suite runs on Errata: `lake test` discovers and runs every test in the package, and CI publishes the resulting reports.
+
+Tests can also be run interactively from the editor: a panel widget shown on a test's declaration runs it in a separate process, streaming its output as it is produced.
diff --git a/lakefile.lean b/lakefile.lean
index f6938c77..99fb2b97 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -143,14 +143,26 @@ lean_lib VersoTests where
   roots := #[`VersoTests]
   globs := #[Glob.andSubmodules `VersoTests]
 
--- Everything below is Errata's own implementation: its library, its self-tests, the generated
--- discovery runner, and the `lake test` driver.
+-- Everything below is Errata's own implementation: its library, the single-test runner and widget
+-- support exe, its self-tests, the generated discovery runner, and the `lake test` driver.
 namespace Errata
 
+input_file errataRunTestWidgetJs where
+  text := true
+  path := "src/errata/Errata/widget/run_test_widget.js"
+
 @[default_target]
 lean_lib Errata where
   srcDir := "src/errata"
   roots := #[`Errata]
+  needs := #[errataRunTestWidgetJs]
+
+-- Runs one test in a fresh process so the widget can stream its output and kill it on cancel.
+@[default_target]
+lean_exe «errata-run-one» where
+  srcDir := "src/errata"
+  root := `ErrataRunOne
+  supportInterpreter := true
 
 -- Tests that exercise Errata using Errata itself.
 @[default_target]
diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean
index d5fce3a9..5f7ee92d 100644
--- a/src/errata-tests/ErrataTests.lean
+++ b/src/errata-tests/ErrataTests.lean
@@ -561,6 +561,62 @@ def reportMarkdown : Test := do
   assertContains "expected 1\nactual 2" md
   assertContains "Summary by module" md
 
+/-- `runValue` reports a passing value as passed. -/
+@[test]
+def runOnePasses : Test := do
+  let o ← runValue default (pure () : Test)
+  assertEq "passed" o.status
+
+/-- `runValue` reports a failing value as failed and carries its message. -/
+@[test]
+def runOneFails : Test := do
+  let o ← runValue default (TestResult.fail { message := "boom" })
+  assertEq "failed" o.status
+  assertEq (some "boom") o.message?
+
+/-- `runValue` reports a skipped value as skipped. -/
+@[test]
+def runOneSkips : Test := do
+  let o ← runValue default (TestResult.skip "later")
+  assertEq "skipped" o.status
+
+/-- A failing run surfaces its captured output in the outcome. -/
+@[test]
+def runOneCapturesOutput : Test := do
+  let o ← runValue default (do IO.println "trace line"; failHere "nope" : Test)
+  assertEq "failed" o.status
+  assertEq 1 o.output.size
+  assertEq "stdout" o.output[0]!.stream
+  assertContains "trace line" o.output[0]!.text
+
+/-- An outcome takes the most severe verdict among several named results. -/
+@[test]
+def runOneAggregates : Test := do
+  let o ← runValue default (do result "a" (pure ()); result "b" (failHere "bad") : Test)
+  assertEq "failed" o.status
+
+/-- A passing run still surfaces its captured output. -/
+@[test]
+def runOnePassOutput : Test := do
+  let o ← runValue default (do IO.println "printed"; return true : IO Bool)
+  assertEq "passed" o.status
+  assertEq 1 o.output.size
+  assertEq "stdout" o.output[0]!.stream
+  assertContains "printed" o.output[0]!.text
+
+/-- Captured output keeps stdout and stderr distinct and interleaved in order. -/
+@[test]
+def runOneStreams : Test := do
+  let o ← runValue default (do
+    IO.println "out one"
+    IO.eprintln "err one"
+    IO.println "out two"
+    return true : IO Bool)
+  assertEq "passed" o.status
+  assertEq 3 o.output.size
+  assertEq "stdout" o.output[0]!.stream
+  assertEq "stderr" o.output[1]!.stream
+  assertEq "stdout" o.output[2]!.stream
 /-- `failure` from the `Alternative` instance fails a test. -/
 @[test]
 def alternativeFailure : Test := expectFail failure
diff --git a/src/errata/Errata.lean b/src/errata/Errata.lean
index 1760f91c..aa5358da 100644
--- a/src/errata/Errata.lean
+++ b/src/errata/Errata.lean
@@ -15,6 +15,8 @@ public import Errata.Process
 public import Errata.Golden
 public import Errata.Report
 public import Errata.Runner
+public import Errata.NameJson
+public import Errata.RunOne
 public import Errata.Discovery
 public import Errata.CompileTime
 public import Errata.Property
diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean
index 0ef020b6..092a6e19 100644
--- a/src/errata/Errata/Discovery.lean
+++ b/src/errata/Errata/Discovery.lean
@@ -9,6 +9,8 @@ public import Errata.IsTest
 public import Errata.Runner
 public import Lean
 public meta import Lean
+public meta import Errata.NameJson
+public meta import Errata.Widget
 
 open Lean Meta Elab Term
 
@@ -70,6 +72,70 @@ meta def recordTest (decl : Name) : AttrM Unit := do
   let docstring? ← findDocString? (← getEnv) decl
   modifyEnv (testExt.addEntry · { name := decl, file := ← getFileName, docstring? })
 
+/-- A synthetic syntax carrying the given source range, used to position the widget. -/
+meta def rangeSyntax [Monad m] [MonadFileMap m]
+    (startPos stopPos : String.Pos.Raw) : m Syntax := do
+  let str := (← getFileMap).source
+  let leading : Substring.Raw := { str, startPos, stopPos := startPos }
+  let trailing : Substring.Raw := { str, startPos := stopPos, stopPos }
+  return Syntax.atom (.original leading startPos trailing stopPos) ""
+
+/-- The text of line {lean}`i`, trimmed of surrounding whitespace. -/
+private meta def lineText (lines : Array String) (i : Nat) : String :=
+  ((lines[i]?).getD "").trimAscii.copy
+
+/-- The first non-blank line at or above {lean}`i`, or {lean}`none` if all are blank up to the top. -/
+private meta partial def firstNonBlankUp (lines : Array String) (i : Nat) : Option Nat :=
+  if (lineText lines i).isEmpty then
+    if i == 0 then none else firstNonBlankUp lines (i - 1)
+  else some i
+
+/-- Scanning up from {lean}`i`, the line that opens a doc comment, stopping at a non-comment line. -/
+private meta partial def docOpenLine (lines : Array String) (i : Nat) : Option Nat :=
+  if (lineText lines i).startsWith "/--" then some i
+  else if (lineText lines i).startsWith "/-" then none
+  else if i == 0 then none
+  else docOpenLine lines (i - 1)
+
+/--
+The 0-based start line of a doc comment immediately above {lean}`markerLineIdx`, if any. To avoid
+mistaking an unrelated trailing comment for one, the comment must be a single-line doc comment or
+have its closing delimiter on its own line opened by a doc-comment line.
+-/
+private meta def docStartLine? (lines : Array String) (markerLineIdx : Nat) : Option Nat := do
+  guard (markerLineIdx > 0)
+  let endLine ← firstNonBlankUp lines (markerLineIdx - 1)
+  let t := lineText lines endLine
+  if t.startsWith "/--" && t.endsWith "-/" then return endLine
+  guard (t == "-/" && endLine > 0)
+  docOpenLine lines (endLine - 1)
+
+/--
+The source range to show the test's widget over: the whole declaration, including a doc comment above
+it. The recorded declaration range is used when available; otherwise the command is re-parsed from the
+start of the marker's line, extending up over an immediately preceding doc comment. Falls back to the
+marker itself.
+-/
+meta def widgetRangeSyntax (decl : Name) (attrStx : Syntax) : AttrM Syntax := do
+  let fileMap ← getFileMap
+  if let some ranges ← findDeclarationRanges? decl then
+    let stx ← rangeSyntax (fileMap.ofPosition ranges.range.pos) (fileMap.ofPosition ranges.range.endPos)
+    return stx
+  let some attrPos := attrStx.getPos? | return attrStx
+  let lineStart := fileMap.ofPosition ⟨(fileMap.toPosition attrPos).line, 0⟩
+  let inputCtx := Parser.mkInputContext fileMap.source (← getFileName)
+  let pmctx : Parser.ParserModuleContext := { env := ← getEnv, options := ← getOptions }
+  let (cmdStx, _, _) := Parser.parseCommand inputCtx pmctx { pos := lineStart } {}
+  match cmdStx.getRange? with
+  | some range =>
+    -- Extend the span up over a doc comment immediately above the marker, when there is one.
+    let lines := (fileMap.source.splitOn "\n").toArray
+    let startPos := match docStartLine? lines ((fileMap.toPosition attrPos).line - 1) with
+      | some docIdx => fileMap.ofPosition ⟨docIdx + 1, 0⟩
+      | none => range.start
+    rangeSyntax startPos range.stop
+  | none => return attrStx
+
 /-- Marks a definition as a test, discovered and run by the Errata test runner. -/
 meta initialize
   registerBuiltinAttribute {
@@ -82,6 +148,22 @@ meta initialize
       Attribute.Builtin.ensureNoArgs stx
       unless kind == AttributeKind.global do throwAttrMustBeGlobal `test kind
       recordTest decl
+      -- Show the widget when the cursor is anywhere on the declaration, not just on the marker.
+      let widgetStx ← widgetRangeSyntax decl stx
+      -- A hash of the test's source, so a run is invalidated when the test is edited.
+      let source := (← getFileMap).source
+      let version := match widgetStx.getRange? with
+        | some range =>
+          let sub : Substring.Raw := { str := source, startPos := range.start, stopPos := range.stop }
+          toString sub.toString.hash
+        | none => ""
+      let props := pure <| json% {
+        decl: $(Errata.nameToJson decl),
+        module: $(toString (← getMainModule)),
+        name: $(toString (privateToUserName decl)),
+        version: $version
+      }
+      Lean.Widget.savePanelWidgetInfo Errata.Widget.runTestWidget.javascriptHash.val props widgetStx
   }
 
 /-- The test's name below its module: the declaration's components past the module prefix, dotted. -/
diff --git a/src/errata/Errata/NameJson.lean b/src/errata/Errata/NameJson.lean
new file mode 100644
index 00000000..f9220702
--- /dev/null
+++ b/src/errata/Errata/NameJson.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+
+public import Lean.Data.Json
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+open Lean
+
+/--
+Encodes a {name}`Lean.Name` structurally, preserving the numeric and hygienic components that the
+standard string form does not round-trip. The widget and the single-test runner exchange test names
+this way.
+-/
+def nameToJson : Name → Json
+  | .anonymous => .null
+  | .str p s => Json.mkObj [("str", .arr #[nameToJson p, .str s])]
+  | .num p n => Json.mkObj [("num", .arr #[nameToJson p, .num n])]
+
+/-- Decodes a {name}`Lean.Name` written by {name}`nameToJson`. -/
+partial def nameOfJson? (j : Json) : Except String Name := do
+  if j.isNull then return .anonymous
+  if let .ok arr := j.getObjVal? "str" then
+    let #[p, s] := (← fromJson? arr : Array Json) | .error "malformed name component"
+    return .str (← nameOfJson? p) (← fromJson? s)
+  if let .ok arr := j.getObjVal? "num" then
+    let #[p, n] := (← fromJson? arr : Array Json) | .error "malformed name component"
+    return .num (← nameOfJson? p) (← fromJson? n)
+  .error "expected an encoded `Name`"
diff --git a/src/errata/Errata/RunOne.lean b/src/errata/Errata/RunOne.lean
new file mode 100644
index 00000000..25e7acee
--- /dev/null
+++ b/src/errata/Errata/RunOne.lean
@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+
+public import Errata.IsTest
+public import Lean.Data.Json
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- A run of captured output from a single stream, used to render output with the streams distinct. -/
+structure OutputChunk where
+  /-- The stream the text was written to: {lit}`"stdout"` or {lit}`"stderr"`. -/
+  stream : String
+  /-- The text written to that stream. -/
+  text : String
+  /-- When the chunk was received, in milliseconds since the Unix epoch; set by the runner. -/
+  time : Nat := 0
+deriving Lean.FromJson, Lean.ToJson, Repr, Inhabited, DecidableEq
+
+/-- The chunk for a single captured output fragment, tagged by its stream. -/
+def OutputChunk.ofOutput : Output → OutputChunk
+  | .stdout s => { stream := "stdout", text := s }
+  | .stderr s => { stream := "stderr", text := s }
+
+/--
+The outcome of running a single test, in a form the InfoView widget renders. The status is one of
+{lit}`"passed"`, {lit}`"failed"`, {lit}`"error"`, or {lit}`"skipped"`.
+-/
+structure RunOutcome where
+  /-- The overall verdict: {lit}`"passed"`, {lit}`"failed"`, {lit}`"error"`, or {lit}`"skipped"`. -/
+  status : String
+  /-- How long the run took, in milliseconds. -/
+  durationMs : Nat
+  /-- The failure or skip message, when the test did not pass. -/
+  message? : Option String := none
+  /-- Supporting detail for a failure, such as a diff or counterexample. -/
+  detail? : Option String := none
+  /-- The captured output, in order, with each chunk tagged by the stream it was written to. -/
+  output : Array OutputChunk := #[]
+  /-- The test's docstring, rendered as Markdown, when it has one. -/
+  description? : Option String := none
+deriving Lean.FromJson, Lean.ToJson, Repr, Inhabited
+
+/-- The status name a single result contributes. -/
+private def statusName : Status → String
+  | .pass => "passed"
+  | .fail _ => "failed"
+  | .error _ => "error"
+  | .skip _ => "skipped"
+
+/-- The message a status carries, when it did not pass. -/
+private def statusMessage : Status → Option String
+  | .pass => none
+  | .fail f => some f.message
+  | .error m => some m
+  | .skip r => some r
+
+/-- Appends one output fragment, merging it into the previous chunk when it is from the same stream. -/
+private def pushFragment (chunks : Array OutputChunk) (o : Output) : Array OutputChunk :=
+  let stream := match o with | .stdout _ => "stdout" | .stderr _ => "stderr"
+  match chunks.back? with
+  | some last => if last.stream == stream
+      then chunks.pop.push { last with text := last.text ++ o.text }
+      else chunks.push { stream, text := o.text }
+  | none => chunks.push { stream, text := o.text }
+
+/--
+Condenses the results of one test run into a single outcome. The verdict is the most severe status
+present (error over failed over skipped over passed), the message and detail come from the first
+result with that status, and the output is every result's captured fragments in order, each tagged by
+its stream.
+-/
+def summarizeResults (results : Array Result) : RunOutcome := Id.run do
+  let rank : Status → Nat
+    | .error _ => 3
+    | .fail _ => 2
+    | .skip _ => 1
+    | .pass => 0
+  let worst := results.foldl (fun acc r => if rank r.status > rank acc then r.status else acc) .pass
+  let duration := results.foldl (fun acc r => acc + r.durationMs) 0
+  let output := results.foldl (fun acc r => r.output.log.foldl pushFragment acc) #[]
+  return {
+    status := statusName worst
+    durationMs := duration
+    message? := statusMessage worst
+    detail? := match worst with | .fail f => f.detail? | _ => none
+    output
+  }
+
+/--
+Runs one testable value to completion and condenses its results into a {name}`RunOutcome`. Captured
+output is kept on a passing result too, since the widget shows it on demand rather than only on
+failure.
+-/
+def runValue {α} [IsTest α] (location : Location) (value : α)
+    (sink : Output → IO Unit := fun _ => pure ()) : IO RunOutcome := do
+  let log ← IO.mkRef (#[] : Array Result)
+  let usedOptions ← IO.mkRef ∅
+  let outputFailed ← IO.mkRef false
+  let cfg : Context := { log, usedOptions, outputFailed, location, writeOutput := sink }
+  let start ← IO.monoMsNow
+  let (outcome, output) ← runCapturing cfg (IsTest.toTest value)
+  let dur := (← IO.monoMsNow) - start
+  let logged ← log.get
+  let results :=
+    match cfg.resultOfOutcome outcome output dur (!logged.isEmpty) with
+    | some r => logged.push r
+    | none =>
+      -- A passing test with named results: the results stand for it, but keep the test's own
+      -- top-level output (written outside any result block) so the widget still shows it.
+      if output.log.isEmpty then logged else logged.push { cfg.mkResult .pass with output }
+  return summarizeResults results
+
+/-- Runs one testable value with a default failure location, for callers without a source range. -/
+def runValueDefault {α} [IsTest α] (value : α) : IO RunOutcome := runValue default value
diff --git a/src/errata/Errata/Widget.lean b/src/errata/Errata/Widget.lean
new file mode 100644
index 00000000..d53cf010
--- /dev/null
+++ b/src/errata/Errata/Widget.lean
@@ -0,0 +1,283 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+
+public meta import Lean.Widget.UserWidget
+public meta import Lean.Server
+public meta import Std.Time
+public meta import Errata.NameJson
+public meta import Errata.RunOne
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+open Lean
+
+namespace Errata.Widget
+
+/--
+Shown when the text cursor is on a test's source span. It offers a "run" button that runs the test
+in the language server, streaming its output as it is produced.
+-/
+@[widget_module]
+meta def runTestWidget : Lean.Widget.Module where
+  javascript := include_str "widget/run_test_widget.js"
+
+/-- The current wall-clock time in milliseconds since the Unix epoch. -/
+private meta def nowMs : IO Nat :=
+  return (← Std.Time.Timestamp.now).toMillisecondsSinceUnixEpoch.toInt.toNat
+
+/--
+A live (or just-finished) run. Output chunks accumulate in {name (full := RunState.chunks)}`chunks`
+so a widget that reconnects after the cursor leaves and returns can replay them by index. The wakeup
+promise is resolved and replaced whenever a chunk arrives or the run finishes, waking any waiter.
+-/
+meta structure RunState where
+  /-- Every output chunk produced so far, in order. -/
+  chunks : IO.Ref (Array Errata.OutputChunk)
+  /-- Whether the run has finished. -/
+  finished : IO.Ref Bool
+  /-- The final outcome, set when the run finishes. -/
+  outcome : IO.Ref (Option Errata.RunOutcome)
+  /-- A promise resolved and replaced on each change, used to wake waiters without polling. -/
+  wakeup : IO.Ref (IO.Promise Unit)
+  /-- The current phase, {lit}`"building"` while compiling the module then {lit}`"running"`. -/
+  phase : IO.Ref String
+  /-- A hash of the test's source when the run started; a later request with a different one is stale. -/
+  version : String
+  /-- When the run started, in milliseconds since the Unix epoch. -/
+  startTime : Nat
+  /-- How long the build took, in milliseconds; 0 while still building. -/
+  buildMs : IO.Ref Nat
+  /-- When the test body started (reported by the runner), in epoch ms; 0 until then. -/
+  execStartTime : IO.Ref Nat
+  /--
+  The process to be killed if the run is cancelled. Contains first the build, then the runner.
+  Updated as each is spawned.
+  -/
+  kill : IO.Ref (IO Unit)
+
+/-- The live runs, keyed by the test's declaration name so a run survives re-elaboration. -/
+meta initialize runRegistry : IO.Ref (Std.HashMap Name RunState) ← IO.mkRef {}
+
+/-- A request to start running a test: the declaration and the module that defines it. -/
+meta structure StartRequest where
+  /-- The test declaration to run, encoded by {name}`nameToJson`. -/
+  decl : Json
+  /-- The module that defines the test, as a dotted name. -/
+  module : String
+  /-- A hash of the test's source, recorded with the run so an edit can invalidate it. -/
+  version : String
+deriving Lean.FromJson, Lean.ToJson
+
+/-- A request for output past a known position, naming the test by its encoded declaration. -/
+meta structure AwaitRequest where
+  /-- The test declaration, encoded by {name}`nameToJson`. -/
+  decl : Json
+  /-- The number of chunks the widget already has, so only later ones are returned. -/
+  since : Nat
+  /-- The test's source hash; a run recorded under a different one is stale and ignored. -/
+  version : String
+  /-- The phase the widget last saw; a reply is returned at once when the run's phase differs. -/
+  phase : String
+deriving Lean.FromJson, Lean.ToJson
+
+/-- A request that names a running test by its declaration, encoded by {name}`nameToJson`. -/
+meta structure RunRef where
+  /-- The test declaration, encoded by {name}`nameToJson`. -/
+  decl : Json
+deriving Lean.FromJson, Lean.ToJson
+
+/-- One reply from {lit}`awaitOutput`: any output chunks past the requested position, or the outcome. -/
+meta structure AwaitResult where
+  /-- The output chunks past the requested position. -/
+  chunks : Array Errata.OutputChunk := #[]
+  /-- The position past the returned chunks, to pass as the next request's start. -/
+  nextSince : Nat := 0
+  /-- When the run started, in milliseconds since the Unix epoch. -/
+  startTime : Nat := 0
+  /-- How long the build took, in milliseconds; 0 while still building. -/
+  buildMs : Nat := 0
+  /-- When the test body started, in epoch ms; 0 until then. Output offsets are relative to it. -/
+  execStartTime : Nat := 0
+  /-- The current phase, {lit}`"building"` or {lit}`"running"`. -/
+  phase : String := "running"
+  /-- Whether the run has finished and no more output will arrive. -/
+  done : Bool := false
+  /-- The final outcome, present once {lit}`done` is set. -/
+  outcome : Option Errata.RunOutcome := none
+deriving Lean.FromJson, Lean.ToJson
+
+open Server in
+/-- Decodes the declaration name from a request, failing the request if it is malformed. -/
+private meta def decodeDecl (j : Json) : RequestM Name :=
+  match nameOfJson? j with
+  | .ok n => pure n
+  | .error e => throw (.mk .invalidParams e)
+
+/-- Resolves the run's current wakeup promise and installs a fresh one, waking any waiter. -/
+private meta def signalRun (state : RunState) : IO Unit := do
+  let p ← state.wakeup.get
+  state.wakeup.set (← IO.Promise.new)
+  p.resolve ()
+
+/-- Kills the runner of a name, if any, marks it finished, and forgets it. -/
+private meta def dropRun (declName : Name) : IO Unit := do
+  if let some state := (← runRegistry.get).get? declName then
+    try (← state.kill.get) catch _ => pure ()
+    state.finished.set true
+    signalRun state
+    runRegistry.modify (·.erase declName)
+
+/--
+Reads the runner's JSON protocol from its stdout: a {lit}`chunk` line per output fragment, then an
+{lit}`outcome` line. Marks the run finished at end of input, which is reached when the process exits
+or is killed, so this never holds a thread past the process's lifetime.
+-/
+private meta partial def readLoop (out : IO.FS.Handle) (state : RunState) : IO Unit := do
+  let line ← out.getLine
+  if line.isEmpty then
+    state.finished.set true
+    signalRun state
+  else
+    if let .ok j := Json.parse line then
+      if let .ok c := j.getObjVal? "chunk" then
+        if let .ok chunk := (fromJson? c : Except String Errata.OutputChunk) then
+          state.chunks.modify (·.push chunk)
+          signalRun state
+      else if let .ok ex := j.getObjVal? "exec" then
+        if let .ok t := (fromJson? ex : Except String Nat) then
+          state.execStartTime.set t
+          signalRun state
+      else if let .ok o := j.getObjVal? "outcome" then
+        if let .ok oc := (fromJson? o : Except String Errata.RunOutcome) then
+          state.outcome.set oc
+    readLoop out state
+
+/-- The outcome shown when the build step fails, carrying its message and detail. -/
+private meta def buildFailure (detail : String) : Errata.RunOutcome := {
+  status := "error", durationMs := 0, message? := some "lake build failed", detail? := some detail
+}
+
+/--
+Builds the test's module from the saved source, then runs the test, streaming its output into the
+run state. Building first means a Run reflects the latest saved version of the test.
+-/
+private meta def buildAndRun (module declJson : String) (state : RunState) : IO Unit := do
+  -- `lake query` builds the runner exe and the test's module (so the run reflects the saved source)
+  -- and prints the exe's absolute path on stdout; progress and errors go to stderr.
+  let build ← IO.Process.spawn {
+    stdin := .null, stdout := .piped, stderr := .piped
+    cmd := "lake", args := #["query", "errata-run-one", module]
+  }
+  state.kill.set build.kill
+  let errTask ← IO.asTask build.stderr.readToEnd
+  let queryOut ← build.stdout.readToEnd
+  let buildErr := (← IO.wait errTask).toOption.getD ""
+  if (← build.wait) != 0 then
+    state.outcome.set (some (buildFailure buildErr))
+    state.finished.set true
+    signalRun state
+    return
+  let some runnerPath := (queryOut.splitOn "\n").find? (!·.trimAscii.isEmpty) |>.map (·.trimAscii.copy)
+    | state.outcome.set (some (buildFailure "lake query did not report the runner's path"))
+      state.finished.set true
+      signalRun state
+      return
+  -- Spawn the runner directly rather than through `lake exe` so it inherits the language server's
+  -- broad `LEAN_PATH`. The runner imports the arbitrary test module at runtime, which is not a
+  -- dependency of the exe, so `lake exe` would narrow `LEAN_PATH` to the exe's own deps and the
+  -- import would fail.
+  let run ← IO.Process.spawn {
+    stdin := .null, stdout := .piped, stderr := .inherit
+    cmd := runnerPath, args := #[module, declJson]
+  }
+  state.kill.set run.kill
+  state.buildMs.set ((← nowMs) - state.startTime)
+  state.phase.set "running"
+  signalRun state
+  readLoop run.stdout state
+
+open Server in
+/-- Whether the document's live text matches what is on disk, i.e. it has no unsaved changes. -/
+private meta def bufferIsClean : RequestM Bool := do
+  let docMeta := (← RequestM.readDoc).meta
+  let some path := System.Uri.fileUriToPath? docMeta.uri
+    | return true
+  match (← (IO.FS.readFile path).toBaseIO).toOption with
+  | some disk => return docMeta.text.source == disk.crlfToLf
+  | none => return true
+
+open Server in
+/-- Server RPC method reporting whether the file has no unsaved changes, gating the Run button. -/
+@[server_rpc_method]
+meta def bufferClean (_ : RunRef) : RequestM (RequestTask Bool) := do
+  return RequestTask.pure (← bufferIsClean)
+
+open Server in
+/-- Server RPC method that starts running a test: builds its saved source, then streams its output. -/
+@[server_rpc_method]
+meta def startTest (req : StartRequest) : RequestM (RequestTask Unit) := do
+  let declName ← decodeDecl req.decl
+  unless ← bufferIsClean do
+    throw (.mk .invalidParams "the file has unsaved changes; save it before running the test")
+  dropRun declName
+  let state : RunState := {
+    chunks := ← IO.mkRef #[], finished := ← IO.mkRef false, outcome := ← IO.mkRef none,
+    wakeup := ← IO.mkRef (← IO.Promise.new), phase := ← IO.mkRef "building", version := req.version,
+    startTime := ← nowMs, buildMs := ← IO.mkRef 0, execStartTime := ← IO.mkRef 0,
+    kill := ← IO.mkRef (pure ())
+  }
+  runRegistry.modify (·.insert declName state)
+  let _ ← IO.asTask (buildAndRun req.module req.decl.compress state)
+  return RequestTask.pure ()
+
+open Server in
+/-- Builds the reply for a waiter given the run's current state and the position it already has. -/
+private meta def replyFrom (state : RunState) (since : Nat) : IO AwaitResult := do
+  let chunks ← state.chunks.get
+  let phase ← state.phase.get
+  let startTime := state.startTime
+  let buildMs ← state.buildMs.get
+  let execStartTime ← state.execStartTime.get
+  if chunks.size > since then
+    let slice := chunks.extract since chunks.size
+    return { chunks := slice, nextSince := since + slice.size, phase, startTime, buildMs, execStartTime }
+  let done ← state.finished.get
+  let outcome ← state.outcome.get
+  return { nextSince := chunks.size, phase, startTime, buildMs, execStartTime, done, outcome }
+
+open Server in
+/--
+Server RPC method that returns output chunks past {name (full := AwaitRequest.since)}`since`, or the
+final outcome. When nothing new is available yet, the reply hangs off the run's wakeup promise, so no
+worker thread is held while waiting and a reconnecting widget replays from {lit}`since := 0`.
+-/
+@[server_rpc_method]
+meta def awaitOutput (req : AwaitRequest) : RequestM (RequestTask AwaitResult) := do
+  let declName ← decodeDecl req.decl
+  let some state := (← runRegistry.get).get? declName
+    | return RequestTask.pure ({ done := true } : AwaitResult)
+  -- A run recorded under a different source hash is from before an edit; treat it as absent.
+  if state.version != req.version then
+    return RequestTask.pure ({ done := true } : AwaitResult)
+  let p ← state.wakeup.get
+  let chunks ← state.chunks.get
+  -- Return at once when there is new output, the run finished, or its phase changed (so a widget
+  -- reconnecting mid-build learns it is building rather than waiting silently); otherwise wait.
+  if chunks.size > req.since || (← state.finished.get) || (← state.phase.get) != req.phase then
+    return RequestTask.pure (← replyFrom state req.since)
+  RequestM.mapTaskCheap (p.resultD ()).asServerTask fun _ => liftM (replyFrom state req.since)
+
+open Server in
+/-- Server RPC method that cancels a running test by killing its process. -/
+@[server_rpc_method]
+meta def cancelTest (req : RunRef) : RequestM (RequestTask Unit) := do
+  let declName ← decodeDecl req.decl
+  dropRun declName
+  return RequestTask.pure ()
diff --git a/src/errata/Errata/widget/jsconfig.json b/src/errata/Errata/widget/jsconfig.json
new file mode 100644
index 00000000..9a3cd8ee
--- /dev/null
+++ b/src/errata/Errata/widget/jsconfig.json
@@ -0,0 +1,8 @@
+{
+    "compilerOptions": {
+        "lib": ["ES2024", "DOM", "DOM.Iterable"],
+        "target": "ES2024",
+        "noEmit": true
+    },
+    "include": ["*.js", "*.d.ts"]
+}
diff --git a/src/errata/Errata/widget/run_test_widget.js b/src/errata/Errata/widget/run_test_widget.js
new file mode 100644
index 00000000..3f4c185f
--- /dev/null
+++ b/src/errata/Errata/widget/run_test_widget.js
@@ -0,0 +1,594 @@
+// @ts-check
+import * as React from "react";
+import { useRpcSession } from "@leanprover/infoview";
+
+const e = React.createElement;
+
+// Persists the last outcome per test for the lifetime of the InfoView session, so leaving and
+// returning to a test's `@[test]` marker shows its previous result rather than a blank widget.
+const resultCache = new Map();
+
+const STATUS_COLORS = {
+    passed: "#2e7d32",
+    failed: "#c62828",
+    error: "#e65100",
+    skipped: "#6b6b6b",
+};
+
+const STATUS_SYMBOLS = {
+    passed: "✓",
+    failed: "✗",
+    error: "⚠",
+    skipped: "○",
+};
+
+const STATUS_LABELS = {
+    passed: "Passed",
+    failed: "FAILED",
+    error: "ERROR",
+    skipped: "Skipped",
+};
+
+const preStyle = {
+    margin: "4px 0 0 0",
+    padding: "6px 8px",
+    whiteSpace: "pre-wrap",
+    wordBreak: "break-word",
+    background: "var(--vscode-textCodeBlock-background, rgba(127,127,127,0.1))",
+    borderRadius: "3px",
+    fontSize: "12px",
+};
+
+function formatDuration(ms) {
+    if (ms < 1000) return ms + " ms";
+    return (ms / 1000).toFixed(ms < 10000 ? 2 : 1) + " s";
+}
+
+function block(text) {
+    return e("pre", { style: preStyle }, text);
+}
+
+function pad(n, w) {
+    return String(n).padStart(w || 2, "0");
+}
+
+const monoFont = "var(--vscode-editor-font-family, monospace)";
+
+// A wall-clock time of day, rounded to the nearest second, from a Unix-epoch millisecond timestamp.
+function formatClock(ms) {
+    if (!ms) return "";
+    const d = new Date(Math.round(ms / 1000) * 1000);
+    return pad(d.getHours()) + ":" + pad(d.getMinutes()) + ":" + pad(d.getSeconds());
+}
+
+// A chunk's offset from the start of execution, in tenths of a second, as `(N.Ns)`.
+function chunkOffset(c, execStartTime) {
+    if (!execStartTime || !c.time) return "";
+    return "(" + ((c.time - execStartTime) / 1000).toFixed(1) + "s)";
+}
+
+// A chunk's stream and offset as a plain string, for the native hover tooltip.
+function chunkLabel(c, execStartTime) {
+    const off = chunkOffset(c, execStartTime);
+    return off ? c.stream + " " + off : c.stream;
+}
+
+// Renders captured output: stdout and stderr interleaved in order, both in the editor's code font,
+// with stderr italicized. Hovering a chunk highlights it and reports its stream and time offset.
+function outputBlock(chunks, execStartTime, hovered, setHovered) {
+    return e(
+        "pre",
+        {
+            style: { ...preStyle, fontFamily: monoFont },
+            onMouseLeave: function () {
+                setHovered(null);
+            },
+        },
+        ...chunks.map(function (c, i) {
+            return e(
+                "span",
+                {
+                    key: i,
+                    title: chunkLabel(c, execStartTime),
+                    onMouseEnter: function () {
+                        setHovered(i);
+                    },
+                    style: {
+                        fontStyle: c.stream === "stderr" ? "italic" : undefined,
+                        borderRadius: "2px",
+                        backgroundColor:
+                            hovered === i
+                                ? "var(--vscode-editor-hoverHighlightBackground, rgba(120,170,255,0.3))"
+                                : undefined,
+                    },
+                },
+                c.text,
+            );
+        }),
+    );
+}
+
+/**
+ * @typedef {{stream: string, text: string, time?: number}} Chunk
+ * @typedef {{status: string, durationMs: number, message?: string, detail?: string,
+ *            output?: Chunk[], description?: string}} Outcome
+ * @typedef {{phase: string, chunks: Chunk[], startTime: number, buildMs: number,
+ *            execStartTime: number}} RunFields
+ *
+ * The run's lifecycle as a single state, so that contradictory combinations (a verdict alongside
+ * an error, a spinner alongside an outcome) cannot be represented:
+ *
+ *   idle       no run for this test, and no recorded outcome to show
+ *   running    a run is in progress, streaming output
+ *   done       a finished run's outcome (live or restored from the session cache)
+ *   cancelled  the run was stopped before it produced an outcome
+ *   failed     the run could not be carried out at all
+ *
+ * All timings come from the server, which records them per run: they survive the widget being
+ * remounted while the run continues, and the server is on the same machine, so its clock agrees
+ * with the client's.
+ *
+ * @typedef {{tag: "idle"}
+ *   | ({tag: "running"} & RunFields)
+ *   | ({tag: "done", outcome: Outcome} & RunFields)
+ *   | {tag: "cancelled", chunks: Chunk[]}
+ *   | {tag: "failed", error: string, chunks: Chunk[]}} RunUi
+ */
+
+/** @type {RunUi} */
+const idleState = { tag: "idle" };
+
+/**
+ * A finished state showing a recorded outcome, with no live chunks or timings of its own.
+ * @param outcome {Outcome}
+ * @returns {RunUi}
+ */
+function doneState(outcome) {
+    return {
+        tag: "done",
+        outcome,
+        phase: "",
+        chunks: [],
+        startTime: 0,
+        buildMs: 0,
+        execStartTime: 0,
+    };
+}
+
+/**
+ * Steps the run state by one event:
+ *
+ *   reset    the cursor moved onto a (possibly different) test; show its cached outcome, if any
+ *   start    the user started a run; the client's clock stands in for the start time until the
+ *            server reports the authoritative one
+ *   server   a reply from `awaitOutput`; it may arrive in any state, since the widget reconnects
+ *            to runs it did not start
+ *   cancel   the user stopped the run
+ *   fail     an RPC call failed, so there is no run to wait for
+ *
+ * @param st {RunUi}
+ * @param ev {any}
+ * @returns {RunUi}
+ */
+function step(st, ev) {
+    switch (ev.type) {
+        case "reset":
+            return ev.outcome ? doneState(ev.outcome) : idleState;
+        case "start":
+            return {
+                tag: "running",
+                phase: "building",
+                chunks: [],
+                startTime: ev.now,
+                buildMs: 0,
+                execStartTime: 0,
+            };
+        case "server": {
+            const res = ev.res;
+            // Zero-valued fields in a reply mean "no news"; the server's values otherwise win.
+            const prev =
+                st.tag === "running"
+                    ? st
+                    : { phase: "running", chunks: [], startTime: 0, buildMs: 0, execStartTime: 0 };
+            const merged = {
+                phase: res.phase || prev.phase,
+                chunks:
+                    res.chunks && res.chunks.length ? prev.chunks.concat(res.chunks) : prev.chunks,
+                startTime: res.startTime || prev.startTime,
+                buildMs: res.buildMs || prev.buildMs,
+                execStartTime: res.execStartTime || prev.execStartTime,
+            };
+            if (!res.done) return { tag: "running", ...merged };
+            if (res.outcome) return { tag: "done", outcome: res.outcome, ...merged };
+            // Done without an outcome: nothing is running server-side. That ends a watched run
+            // (stopped from elsewhere, or its process died); in any other state it is no news.
+            return st.tag === "running" ? { tag: "cancelled", chunks: st.chunks } : st;
+        }
+        case "cancel":
+            return { tag: "cancelled", chunks: st.tag === "running" ? st.chunks : [] };
+        case "fail":
+            return {
+                tag: "failed",
+                error: ev.error,
+                chunks: st.tag === "running" ? st.chunks : [],
+            };
+        default:
+            return st;
+    }
+}
+
+export default function (props) {
+    const rs = useRpcSession();
+    // Keyed by both the test and a hash of its source, so editing the test changes the key and
+    // invalidates its cached/in-progress run.
+    const version = props.version || "";
+    const cacheKey = JSON.stringify(props.decl) + "@" + version;
+
+    const [st, dispatch] = React.useReducer(step, undefined, function () {
+        const cached = resultCache.get(cacheKey);
+        return cached ? doneState(cached) : idleState;
+    });
+    // Milliseconds since the run started, ticking while it does.
+    const [elapsed, setElapsed] = React.useState(0);
+    // The output chunk under the cursor, highlighted with its timestamp shown.
+    const [hovered, setHovered] = React.useState(null);
+    // Whether the file has no unsaved changes; the test runs the saved version, so Run is gated on it.
+    const [clean, setClean] = React.useState(true);
+    // Briefly true after the output is copied, to confirm the copy in the button label.
+    const [copied, setCopied] = React.useState(false);
+    // Whether the output disclosure is expanded; open by default, collapsible to hide large output.
+    const [outputOpen, setOutputOpen] = React.useState(true);
+    // Whether the cursor is over the output area, revealing the floating copy button.
+    const [overOutput, setOverOutput] = React.useState(false);
+
+    // Bumped on each run start, cancel, and unmount so a superseded await loop ignores late replies.
+    const gen = React.useRef(0);
+    // The number of chunks already pulled from the server, so a reconnect replays from the start.
+    const sinceRef = React.useRef(0);
+    // The last phase the widget saw; "" forces the next await to return the run's current phase at once.
+    const phaseRef = React.useRef("");
+
+    const running = st.tag === "running";
+    const runStart = running ? st.startTime : 0;
+
+    React.useEffect(
+        function () {
+            if (!running || !runStart) return undefined;
+            function update() {
+                setElapsed(Math.max(0, Date.now() - runStart));
+            }
+            update();
+            const timer = setInterval(update, 100);
+            return function () {
+                clearInterval(timer);
+            };
+        },
+        [running, runStart],
+    );
+
+    function loop(myGen) {
+        rs.call("Errata.Widget.awaitOutput", {
+            decl: props.decl,
+            since: sinceRef.current,
+            version: version,
+            phase: phaseRef.current,
+        }).then(
+            function (res) {
+                if (gen.current !== myGen) return;
+                if (res.phase) phaseRef.current = res.phase;
+                if (res.chunks && res.chunks.length) sinceRef.current = res.nextSince;
+                if (res.done && res.outcome) resultCache.set(cacheKey, res.outcome);
+                dispatch({ type: "server", res: res });
+                if (!res.done) loop(myGen);
+            },
+            function (err) {
+                if (gen.current !== myGen) return;
+                dispatch({ type: "fail", error: (err && err.message) || String(err) });
+            },
+        );
+    }
+
+    // The InfoView reuses one component instance for whichever test the cursor is on, so reset and
+    // reconnect whenever the test changes (keyed on `cacheKey`), not just on mount. Restores any cached
+    // outcome for this test and replays an in-progress run from the start.
+    React.useEffect(
+        function () {
+            const myGen = gen.current + 1;
+            gen.current = myGen;
+            sinceRef.current = 0;
+            phaseRef.current = "";
+            dispatch({ type: "reset", outcome: resultCache.get(cacheKey) || null });
+            setHovered(null);
+            loop(myGen);
+            let cancelledCheck = false;
+            let cleanTimer = null;
+            function checkClean() {
+                rs.call("Errata.Widget.bufferClean", { decl: props.decl }).then(
+                    function (c) {
+                        if (cancelledCheck) return;
+                        setClean(c);
+                        // While the buffer is dirty, re-check so the button re-enables shortly after a save.
+                        if (!c) cleanTimer = setTimeout(checkClean, 1500);
+                    },
+                    function () {},
+                );
+            }
+            checkClean();
+            return function () {
+                gen.current += 1;
+                cancelledCheck = true;
+                if (cleanTimer) clearTimeout(cleanTimer);
+            };
+        },
+        [cacheKey],
+    );
+
+    function run() {
+        const myGen = gen.current + 1;
+        gen.current = myGen;
+        sinceRef.current = 0;
+        phaseRef.current = "building";
+        dispatch({ type: "start", now: Date.now() });
+        setElapsed(0);
+        rs.call("Errata.Widget.startTest", {
+            decl: props.decl,
+            module: props.module,
+            version: version,
+        }).then(
+            function () {
+                if (gen.current === myGen) loop(myGen);
+            },
+            function (err) {
+                if (gen.current !== myGen) return;
+                dispatch({ type: "fail", error: (err && err.message) || String(err) });
+            },
+        );
+    }
+
+    function cancel() {
+        gen.current += 1;
+        dispatch({ type: "cancel" });
+        rs.call("Errata.Widget.cancelTest", { decl: props.decl }).catch(function () {});
+    }
+
+    const name = props.name || "test";
+
+    const header = e(
+        "div",
+        { style: { display: "flex", alignItems: "center", gap: "8px" } },
+        running
+            ? e("button", { onClick: cancel }, "Cancel")
+            : e(
+                  "button",
+                  {
+                      onClick: run,
+                      disabled: !clean,
+                      title: clean ? undefined : "Save the file to run the test",
+                  },
+                  st.tag === "idle" ? "Run" : "Run again",
+              ),
+        e(
+            "span",
+            {
+                style: {
+                    fontFamily: "var(--vscode-editor-font-family, monospace)",
+                    fontSize: "12px",
+                },
+            },
+            name,
+        ),
+        !clean && !running
+            ? e("span", { style: { opacity: 0.6, fontSize: "11px" } }, "unsaved — save to run")
+            : null,
+    );
+
+    const outcome = st.tag === "done" ? st.outcome : null;
+    const timings = st.tag === "running" || st.tag === "done" ? st : null;
+    const execStartTime = timings ? timings.execStartTime : 0;
+
+    // Prefer the live, server-timestamped chunks; fall back to a cached outcome's output.
+    const liveChunks = st.tag === "idle" ? [] : st.chunks;
+    const chunks = liveChunks.length ? liveChunks : outcome && outcome.output ? outcome.output : [];
+
+    function copyOutput() {
+        const text = chunks
+            .map(function (c) {
+                return c.text;
+            })
+            .join("");
+        Promise.resolve(navigator.clipboard.writeText(text)).then(
+            function () {
+                setCopied(true);
+                setTimeout(function () {
+                    setCopied(false);
+                }, 1500);
+            },
+            function () {},
+        );
+    }
+
+    // The copy icon (two overlapping sheets), or a check mark once the output has been copied.
+    const copyIcon = e(
+        "svg",
+        {
+            width: 13,
+            height: 13,
+            viewBox: "0 0 24 24",
+            fill: "none",
+            stroke: "currentColor",
+            strokeWidth: 2,
+            strokeLinecap: "round",
+            strokeLinejoin: "round",
+        },
+        copied
+            ? e("path", { key: "check", d: "M20 6L9 17l-5-5" })
+            : [
+                  e("rect", { key: "sheet", x: 9, y: 9, width: 13, height: 13, rx: 2, ry: 2 }),
+                  e("path", {
+                      key: "back",
+                      d: "M5 15H4a2 2 0 0 1-2-2V4a2 2 0 0 1 2-2h9a2 2 0 0 1 2 2v1",
+                  }),
+              ],
+    );
+
+    // A copy button floating over the top-right of the output, revealed on hover (or while confirming).
+    const copyButton = e(
+        "button",
+        {
+            onClick: copyOutput,
+            title: copied ? "Copied" : "Copy output to clipboard",
+            "aria-label": "Copy output to clipboard",
+            style: {
+                position: "absolute",
+                top: "4px",
+                right: "4px",
+                zIndex: 1,
+                display: "flex",
+                alignItems: "center",
+                padding: "3px",
+                lineHeight: 0,
+                opacity: overOutput || copied ? 0.95 : 0,
+                transition: "opacity 0.1s",
+            },
+        },
+        copyIcon,
+    );
+
+    const outputSection =
+        chunks.length === 0
+            ? null
+            : e(
+                  "details",
+                  {
+                      key: "output",
+                      open: outputOpen,
+                      onToggle: /** @param ev {React.ToggleEvent<HTMLDetailsElement>} */ function (
+                          ev,
+                      ) {
+                          setOutputOpen(ev.currentTarget.open);
+                      },
+                      style: { marginTop: "4px" },
+                  },
+                  e(
+                      "summary",
+                      { style: { opacity: 0.7, fontSize: "11px", cursor: "pointer" } },
+                      hovered !== null && chunks[hovered]
+                          ? [
+                                "Output  —  ",
+                                e(
+                                    "span",
+                                    { key: "stream", style: { fontFamily: monoFont } },
+                                    chunks[hovered].stream,
+                                ),
+                                " " + chunkOffset(chunks[hovered], execStartTime),
+                            ]
+                          : "Output",
+                  ),
+                  e(
+                      "div",
+                      {
+                          style: { position: "relative" },
+                          onMouseEnter: function () {
+                              setOverOutput(true);
+                          },
+                          onMouseLeave: function () {
+                              setOverOutput(false);
+                          },
+                      },
+                      copyButton,
+                      outputBlock(chunks, execStartTime, hovered, setHovered),
+                  ),
+              );
+
+    // The primary status/progress element, then dimmed badges: start time, build and run durations.
+    let primary = null;
+    if (st.tag === "running") {
+        const label = st.phase === "building" ? "Building… " : "Running… ";
+        primary = e(
+            "span",
+            { style: { opacity: 0.8 } },
+            label,
+            e("span", { style: { fontFamily: monoFont } }, formatDuration(elapsed)),
+        );
+    } else if (st.tag === "failed") {
+        primary = e(
+            "span",
+            { style: { color: STATUS_COLORS.error } },
+            "could not run: " + st.error,
+        );
+    } else if (st.tag === "done") {
+        primary = e(
+            "span",
+            { style: { color: STATUS_COLORS[st.outcome.status] || "inherit", fontWeight: 600 } },
+            (STATUS_SYMBOLS[st.outcome.status] || "") +
+                " " +
+                (STATUS_LABELS[st.outcome.status] || st.outcome.status),
+        );
+    } else if (st.tag === "cancelled") {
+        primary = e("span", { style: { opacity: 0.7 } }, "cancelled");
+    }
+
+    const badges = [];
+    if (timings && timings.startTime) badges.push("Start " + formatClock(timings.startTime));
+    if (timings && timings.buildMs) badges.push("Build " + formatDuration(timings.buildMs));
+    if (outcome) badges.push("Run " + formatDuration(outcome.durationMs));
+
+    const infoRow =
+        primary || badges.length
+            ? e(
+                  "div",
+                  {
+                      style: {
+                          display: "flex",
+                          alignItems: "baseline",
+                          gap: "8px",
+                          flexWrap: "wrap",
+                      },
+                  },
+                  primary,
+                  ...badges.map(function (b, i) {
+                      return e(
+                          "span",
+                          { key: i, style: { opacity: 0.55, fontSize: "11px" } },
+                          "· " + b,
+                      );
+                  }),
+              )
+            : null;
+
+    const extras = [];
+    if (outcome && outcome.message) extras.push(e("div", { key: "msg" }, block(outcome.message)));
+    if (outcome && outcome.detail) extras.push(e("div", { key: "detail" }, block(outcome.detail)));
+
+    // The test's docstring, rendered by Lean to Markdown and shown as text alongside its result.
+    const descriptionSection =
+        outcome && outcome.description
+            ? e(
+                  "div",
+                  {
+                      key: "description",
+                      style: {
+                          marginTop: "4px",
+                          fontSize: "12px",
+                          opacity: 0.85,
+                          whiteSpace: "pre-wrap",
+                      },
+                  },
+                  outcome.description,
+              )
+            : null;
+
+    const body =
+        infoRow || descriptionSection || extras.length || outputSection
+            ? e(
+                  "div",
+                  { style: { marginTop: "4px" } },
+                  infoRow,
+                  descriptionSection,
+                  ...extras,
+                  outputSection,
+              )
+            : null;
+
+    return e("div", { style: { padding: "2px 0" } }, header, body);
+}
diff --git a/src/errata/Errata/widget/widget-externals.d.ts b/src/errata/Errata/widget/widget-externals.d.ts
new file mode 100644
index 00000000..b2fc83fa
--- /dev/null
+++ b/src/errata/Errata/widget/widget-externals.d.ts
@@ -0,0 +1,25 @@
+// Minimal ambient declarations for the npm packages the run-test widget imports. The widget is
+// served as-is to the InfoView, which supplies React and the InfoView RPC API at runtime, so only
+// the surface the widget uses is declared here, enough for `tsc` to type-check the rest.
+
+declare module "react" {
+    export function createElement(type: any, props?: any, ...children: any[]): any;
+    export function useState(initial: any): [any, (value: any) => void];
+    export function useReducer<S, A>(
+        reducer: (state: S, action: A) => S,
+        initialArg: any,
+        init?: (arg: any) => S,
+    ): [S, (action: A) => void];
+    export function useEffect(effect: () => void | (() => void), deps?: any[]): void;
+    export function useRef(initial: any): { current: any };
+    export interface ToggleEvent<T = Element> {
+        currentTarget: T;
+        target: EventTarget;
+    }
+}
+
+declare module "@leanprover/infoview" {
+    export function useRpcSession(): {
+        call(method: string, params: any): Promise<any>;
+    };
+}
diff --git a/src/errata/ErrataRunOne.lean b/src/errata/ErrataRunOne.lean
new file mode 100644
index 00000000..7cae3c6a
--- /dev/null
+++ b/src/errata/ErrataRunOne.lean
@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+
+public import Errata
+public import Std.Time
+public meta import Lean
+
+open Lean Meta
+
+/-- The current wall-clock time in milliseconds since the Unix epoch. -/
+def nowMs : IO Nat :=
+  return (← Std.Time.Timestamp.now).toMillisecondsSinceUnixEpoch.toInt.toNat
+
+/--
+Evaluates the test named by {lean}`declName` in the current environment to a runnable action.
+
+The action is reached through {name}`Errata.IsTest.toTest` so any testable type works, and through
+{lit}`import all` of its module so a module-private test is still reachable.
+-/
+unsafe def evalTestM (declName : Name) : CoreM (Errata.TestM Unit × Option String) :=
+  MetaM.run' do
+    let env ← getEnv
+    -- The widget passes the declaration's real name, but a module-private test is mangled, so fall
+    -- back to matching the user-facing name when the exact name is absent.
+    let realName ←
+      if env.contains declName then pure declName
+      else match env.constants.fold (init := none) (fun acc n _ =>
+          acc <|> (if privateToUserName n == declName then some n else none)) with
+        | some n => pure n
+        | none => throwError "unknown test `{declName}`"
+    let decl := mkConst realName
+    let declType ← inferType decl
+    let inst ←
+      match ← trySynthInstance (mkApp (mkConst ``Errata.IsTest) declType) with
+      | .some inst => pure inst
+      | _ => throwError "`{declName}` is not a test"
+    let act := mkApp3 (mkConst ``Errata.IsTest.toTest) declType inst decl
+    let ty := mkApp (mkConst ``Errata.TestM) (mkConst ``Unit)
+    let test ← evalExpr (Errata.TestM Unit) ty act (safety := .unsafe)
+    return (test, ← findDocString? env realName)
+
+/-- Writes one JSON protocol line to the runner's real stdout and flushes it for prompt streaming. -/
+private def emitLine (out : IO.FS.Stream) (key : String) (value : Json) : IO Unit := do
+  out.putStr ((Json.mkObj [(key, value)]).compress ++ "\n")
+  out.flush
+
+/-- Imports {lean}`targetModule`, runs the test named by {lean}`declName`, and streams its result. -/
+unsafe def runImpl (args : List String) : IO UInt32 := do
+  let [modStr, declStr] := args
+    | IO.eprintln "usage: errata-run-one <module> <decl-json>"; return 2
+  let targetModule := modStr.toName
+  let declName ←
+    match Json.parse declStr with
+    | .ok j => IO.ofExcept (Errata.nameOfJson? j)
+    | .error _ => pure declStr.toName
+  -- The runner's real stdout carries the JSON protocol; the test's own output is captured by
+  -- `runValue` and forwarded as chunk lines, so this handle is taken before that redirection.
+  let out ← IO.getStdout
+  initSearchPath (← findSysroot)
+  if let some leanPath ← IO.getEnv "LEAN_PATH" then
+    searchPathRef.modify (· ++ System.SearchPath.parse leanPath)
+  enableInitializersExecution
+  let env ← importModules
+    #[{ module := targetModule, importAll := true }, { module := `Errata }] {} (loadExts := true)
+  let coreCtx : Core.Context := { fileName := "<errata-run-one>", fileMap := default }
+  let ((act, doc?), _) ← (evalTestM declName).toIO coreCtx { env }
+  -- Mark when the test body starts, so the widget shows output offsets within the test itself,
+  -- excluding the build and module-import time before this point.
+  emitLine out "exec" (toJson (← nowMs))
+  let sink := fun (o : Errata.Output) => do
+    let chunk := { Errata.OutputChunk.ofOutput o with time := ← nowMs }
+    emitLine out "chunk" (toJson chunk)
+  let outcome ← Errata.runValue default act (sink := sink)
+  emitLine out "outcome" (toJson { outcome with description? := doc? })
+  return 0
+
+@[implemented_by runImpl]
+opaque run (args : List String) : IO UInt32
+
+/-- Runs a single Errata test, streaming its output and final outcome as JSON lines to stdout. -/
+public def main (args : List String) : IO UInt32 := run args