diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d68f7852..9e31734d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -70,11 +70,13 @@ jobs:
 
             - name: Check for orphaned modules
               run: |
-                  # These are all the library modules; docs and tests are excluded
+                  # These are all the library modules plus the Errata self-tests, whose modules
+                  # must stay reachable from their root for the test driver to run them; docs and
+                  # the remaining test libraries are excluded
                   out="$(lake query VersoUtil:orphanMods Verso:orphanMods MultiVerso:orphanMods \
                     VersoSearch:orphanMods VersoBlog:orphanMods VersoManual:orphanMods \
                     VersoIlluminate:orphanMods VersoTutorial:orphanMods VersoLiterate:orphanMods \
-                    VersoLiterateCode:orphanMods)"
+                    VersoLiterateCode:orphanMods Errata:orphanMods ErrataTests:orphanMods)"
                   if [ -n "$(printf '%s' "$out" | tr -d '[:space:]')" ]; then
                     echo "Found orphaned modules:"
                     echo "$out"
diff --git a/.github/workflows/no-eval-in-source.yml b/.github/workflows/no-eval-in-source.yml
index 29b5e75a..671d654f 100644
--- a/.github/workflows/no-eval-in-source.yml
+++ b/.github/workflows/no-eval-in-source.yml
@@ -25,10 +25,11 @@ jobs:
                     fi
                   done < <(find ./src -path ./src/tests -prune -o \
                     -path ./src/test-projects -prune -o \
+                    -path ./src/errata-tests -prune -o \
                     -name "*.lean" -type f -print0)
 
                   if [ ${#OFFENDING_FILES[@]} -gt 0 ]; then
-                    echo "Found #eval statements in module source files (should be in src/tests/):"
+                    echo "Found #eval statements in module source files (should be in src/tests/ or src/errata-tests/):"
                     printf '%s\n' "${OFFENDING_FILES[@]}"
                     echo ""
                     echo "Offending lines:"
diff --git a/doc/UsersGuide/Releases/Entries.lean b/doc/UsersGuide/Releases/Entries.lean
index d2dd7cd0..ffdacb0f 100644
--- a/doc/UsersGuide/Releases/Entries.lean
+++ b/doc/UsersGuide/Releases/Entries.lean
@@ -24,4 +24,5 @@ public import UsersGuide.Releases.Entries.MethodInMultiVerso
 public import UsersGuide.Releases.Entries.ReleaseNotesChapter
 public import UsersGuide.Releases.Entries.RoleDiagnostics
 public import UsersGuide.Releases.Entries.SearchPriority
+public import UsersGuide.Releases.Entries.TestFramework
 public import UsersGuide.Releases.Entries.VersionedReleaseNotes
diff --git a/doc/UsersGuide/Releases/Entries/TestFramework.lean b/doc/UsersGuide/Releases/Entries/TestFramework.lean
new file mode 100644
index 00000000..23b46293
--- /dev/null
+++ b/doc/UsersGuide/Releases/Entries/TestFramework.lean
@@ -0,0 +1,31 @@
+/-
+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 UsersGuide.Releases.Entry
+
+open Verso.Genre Manual InlineLean UsersGuide.Releases
+
+release_note
+  version := ⟨4, 34, 0⟩
+  breaking := false
+  tag := "feat-test-framework"
+  prs := [956]
+
+#doc (Manual) "Test Framework" =>
+
+Added `Errata`, a testing framework with test discovery, uniform failure reporting, and CI-friendly report formats.
+
+Previously, Verso's tests were all essentially _ad hoc_ IO actions that were run in sequence or elaborations that would fail.
+Each item was tested with the appropriate tool for the job (random testing, golden testing, traditional unit tests, etc), but there was no overarching test code.
+In particular, there were no universal conventions about output or failure reporting, and it could be difficult to see which test had actually failed at a glance.
+`Errata` unifies reporting and eliminates the need to plumb lists of tests through the system.
+
+Tests are marked with the `@[test]` attribute, and a test's value can have any type with an `IsTest` instance.
+Each test's docstring and source range are saved for failure reporting.
+The test runner discovers every test in the package; it can restrict the run to named libraries, rerun property tests with a fixed seed, update golden files, fail the run on warnings with `--wfail`, and write JUnit XML, JSON, and Markdown reports.
+
+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.
diff --git a/lake-manifest.json b/lake-manifest.json
index 589c8920..fff4d1a0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/illuminate",
+ [{"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/illuminate",
    "type": "git",
    "subDir": null,
    "scope": "",
diff --git a/lakefile.lean b/lakefile.lean
index ade9bbab..180a89fc 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -5,6 +5,7 @@ require subverso from git "https://github.com/leanprover/subverso"@"main"
 require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 require plausible from git "https://github.com/leanprover-community/plausible"@"main"
 require illuminate from git "https://github.com/leanprover/illuminate"@"main"
+require Cli from git "https://github.com/leanprover/lean4-cli"@"main"
 
 package verso where
   precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30
@@ -144,6 +145,224 @@ lean_exe «verso-tests» where
   srcDir := "src/tests"
   supportInterpreter := true
 
+-- Everything below is Errata's own implementation: its library, its self-tests, the generated
+-- discovery runner, and the runner script.
+namespace Errata
+
+@[default_target]
+lean_lib Errata where
+  srcDir := "src/errata"
+  roots := #[`Errata]
+
+-- Tests that exercise Errata using Errata itself.
+@[default_target]
+lean_lib ErrataTests where
+  srcDir := "src/errata-tests"
+  roots := #[`ErrataTests]
+
+-- The directory below the package's Lake directory where the Errata driver writes the generated
+-- runner sources.
+def errataRunnerDir : System.FilePath := defaultLakeDir / "errata-runner"
+
+-- The selected test set, written by the driver. The generated targets depend on it, so changing
+-- the selection changes their trace and Lake rebuilds them rather than relinking a stale object.
+input_file errataSelection where
+  text := true
+  path := errataRunnerDir / "selection"
+
+-- The generated discovered-tests module (`allTests`), written by the Errata driver.
+lean_lib ErrataGenerated where
+  srcDir := errataRunnerDir
+  roots := #[`ErrataDiscovered]
+  needs := #[errataSelection]
+
+-- The generated, discovered test runner. Its source is written by the Errata test driver.
+lean_exe «errata-runner» where
+  root := `ErrataRunnerMain
+  srcDir := errataRunnerDir
+  supportInterpreter := true
+  needs := #[errataSelection]
+
+/--
+Reads a built module's `.olean` header: whether it participates in the module system, and whether
+it records any `@[test]` (including those generated by `#test_msgs` and `#test_guard`).
+-/
+private def moduleInfo (oleanFile : System.FilePath) : IO (Bool × Bool) := do
+  let (data, region) ← Lean.readModuleData oleanFile
+  let hasTests := data.entries.any fun (name, entries) => name == `Errata.test && entries.size > 0
+  let isModule := data.isModule
+  unsafe region.free
+  return (isModule, hasTests)
+
+/--
+The modules that sit under a library's roots on disk without being among the modules the library
+actually builds. Nothing imports them and no glob covers them, so they are never compiled, and any
+tests they define never run. `known` is the library's module set.
+-/
+private def unreachableModules (lib : Lake.LeanLib) (known : Lean.NameSet) :
+    IO (Array Lean.Name) := do
+  let found ← IO.mkRef (#[] : Array Lean.Name)
+  for root in lib.config.roots do
+    try
+      Lake.Glob.submodules root |>.forEachModuleIn lib.srcDir fun m => do
+        unless known.contains m do found.modify (·.push m)
+    catch
+      -- Thrown for a root with no corresponding directory, which has no submodules to orphan.
+      | .noFileOrDirectory .. => pure ()
+      | e => throw e
+  found.get
+
+/--
+Generate the bridge module: `import all` the module-system test modules so their private tests
+are reachable, gathering them into `allTests` through `getAllTests%`.
+-/
+private def discoveredSource (packageName : String) (mods : Array Lean.Name) : String :=
+  let imports := "\n".intercalate ("public import Errata" :: mods.toList.map (s!"import all {·}"))
+  let modList := " ".intercalate (mods.toList.map (·.toString))
+  s!"module\n\n{imports}\n\n\
+    public def allTests : Array Errata.TestEntry := getAllTests% \"{packageName}\" {modList}\n"
+
+/--
+Generate the non-module main: import the bridge module and the non-module test modules (which a
+`module` cannot import), then run their combined tests.
+-/
+private def mainSource (packageName : String) (mods : Array Lean.Name) (discovered : Lean.Name) :
+    String :=
+  let imports := "\n".intercalate
+    ("import Errata" :: s!"import {discovered}" :: mods.toList.map (s!"import {·}"))
+  let modList := " ".intercalate (mods.toList.map (·.toString))
+  s!"{imports}\n\n\
+    def main (args : List String) : IO UInt32 :=\n  \
+    Errata.runMain (allTests ++ getAllTests% \"{packageName}\" {modList}) args\n"
+
+/--
+Splits driver arguments at the `--test-options` marker into library names and runner passthrough
+arguments. Library names precede the marker and may not look like options; everything after the
+marker goes to the runner.
+-/
+private def splitArgs (args : List String) : Except String (List String × List String) :=
+  let (names, rest) :=
+    match args.span (· != "--test-options") with
+    | (names, _ :: after) => (names, after)
+    | (names, []) => (names, [])
+  match names.find? (·.startsWith "-") with
+  | some opt =>
+    .error s!"unexpected option '{opt}': arguments before the `--test-options` marker name the \
+      libraries to test. Put runner options after the marker, \
+      e.g. `lake run Errata.run --test-options {opt}`."
+  | none => .ok (names, rest)
+
+/-- Usage information for `lake run Errata.run`. -/
+private def usage : String := include_str "src/errata/Errata/usage.txt"
+
+script run (args) do
+  let ws ← getWorkspace
+  -- Answer the driver's own `--help` before discovering or building anything. A `--help` after the
+  -- marker asks for the runner's options, so it goes to the runner along with the other arguments.
+  if (args.takeWhile (· != "--test-options")).any (fun a => a == "--help" || a == "-h") then
+    IO.println usage
+    return 0
+  let (libNames, runnerArgs) ←
+    match splitArgs args with
+    | .ok result => pure result
+    | .error msg =>
+      IO.eprintln s!"error: {msg}"
+      IO.eprintln usage
+      return 1
+  -- `--wfail` is the runner's warnings-as-errors flag; the driver's own warnings honor it too.
+  let wfail := runnerArgs.contains "--wfail"
+  -- Search the named libraries, or every library in the package by default. A name may be a bare
+  -- `Library` in this package or a `package/Library` reaching into a dependency, following Lake's
+  -- target syntax. A library whose source lives in the generated-runner directory has no source
+  -- until this script writes it, and no tests of its own.
+  let candidates := ws.root.leanLibs.filter (·.config.srcDir != errataRunnerDir)
+  let libs ←
+    if libNames.isEmpty then pure candidates
+    else do
+      let mut chosen : Array Lake.LeanLib := #[]
+      for spec in libNames do
+        let lib? ←
+          match spec.splitOn "/" with
+          | [libName] => pure (candidates.find? (·.name == libName.toName))
+          | [pkgName, libName] =>
+            let pkgName := if pkgName.startsWith "@" then pkgName.drop 1 else pkgName
+            let pkg? := if pkgName.isEmpty then some ws.root else ws.findPackageByName? pkgName.toName
+            match pkg? with
+            | some pkg => pure (pkg.findLeanLib? libName.toName)
+            | none =>
+              IO.eprintln s!"error: no package named '{pkgName}'"
+              return 1
+          | _ =>
+            IO.eprintln s!"error: invalid library spec '{spec}' (expected `Library` or `package/Library`)"
+            return 1
+        match lib? with
+        | some lib => chosen := chosen.push lib
+        | none =>
+          IO.eprintln s!"error: no library matches '{spec}'"
+          return 1
+      pure chosen
+  -- Build every module in the selected libraries; their compiled `.olean` headers are authoritative
+  -- on which modules carry tests.
+  let (modInfos, libMods) ← runBuild do
+    let mut oleanJobs := #[]
+    let mut infos : Array (Lean.Name × System.FilePath) := #[]
+    let mut libMods : Array (Lake.LeanLib × Array Lean.Name) := #[]
+    for lib in libs do
+      let mods ← (← lib.modules.fetch).await
+      libMods := libMods.push (lib, mods.map (·.name))
+      for m in mods do
+        oleanJobs := oleanJobs.push (← m.olean.fetch)
+        infos := infos.push (m.name, m.oleanFile)
+    pure <| (Job.collectArray oleanJobs).map (sync := true) fun _ => (infos, libMods)
+  -- A test module is one whose `.olean` records a test. Module-system test modules go in the bridge
+  -- module (`import all`); non-module ones can only be imported by the non-module main.
+  let mut moduleMods : Array Lean.Name := #[]
+  let mut nonModuleMods : Array Lean.Name := #[]
+  for (moduleName, oleanFile) in modInfos do
+    let (isModule, hasTests) ← moduleInfo oleanFile
+    if hasTests then
+      if isModule then moduleMods := moduleMods.push moduleName
+      else nonModuleMods := nonModuleMods.push moduleName
+  -- A module that sits under a library's roots without being reachable from them is never built, so
+  -- any tests it defines are silently left out. A library is checked when it was named on the
+  -- command line, since naming it declares that its tests are expected, or when its built modules
+  -- carry tests. That is a configuration slip rather than a test failure, so report it and run
+  -- anyway.
+  let testMods := moduleMods ++ nonModuleMods
+  let mut unreachable : Array (Lake.LeanLib × Array Lean.Name) := #[]
+  for (lib, mods) in libMods do
+    if !libNames.isEmpty || mods.any (testMods.contains ·) then
+      let known := mods.foldl (init := Lean.NameSet.empty) (·.insert ·)
+      let missed ← unreachableModules lib known
+      unless missed.isEmpty do unreachable := unreachable.push (lib, missed)
+  unless unreachable.isEmpty do
+    let level := if wfail then "error" else "warning"
+    IO.eprintln s!"{level}: these modules are not reachable from their library's roots, so any \
+      tests they define are not discovered. Import them from a root, or widen the library's \
+      `globs` (e.g. `globs := #[Glob.andSubmodules `Root]`):"
+    for (lib, mods) in unreachable do
+      for mod in mods do
+        IO.eprintln s!"  {lib.name}: {mod}"
+    if wfail then return 1
+  -- Write the generated sources, plus a `selection` file naming the chosen test set. The generated
+  -- targets depend on that file, so a changed selection invalidates them through Lake's own trace.
+  let dir := ws.root.dir / errataRunnerDir
+  IO.FS.createDirAll dir
+  let selection := "\n".intercalate ((moduleMods ++ nonModuleMods).map (·.toString) |>.qsort (· < ·)).toList
+  for (name, src) in
+      [("selection", selection ++ "\n"),
+       ("ErrataDiscovered.lean", discoveredSource ws.root.prettyName moduleMods),
+       ("ErrataRunnerMain.lean", mainSource ws.root.prettyName nonModuleMods `ErrataDiscovered)] do
+    let file := dir / name
+    let changed ← if ← file.pathExists then pure ((← IO.FS.readFile file) != src) else pure true
+    if changed then IO.FS.writeFile file src
+  -- Build and run the discovered runner.
+  let exePath ← runBuild «errata-runner».fetch
+  let child ← IO.Process.spawn { cmd := exePath.toString, args := runnerArgs.toArray }
+  child.wait
+
+end Errata
+
 -- The release notes compute the version under development from this file while they elaborate,
 -- so its contents are an input to the library.
 input_file leanToolchain where
diff --git a/src/errata-tests/ErrataTests.lean b/src/errata-tests/ErrataTests.lean
new file mode 100644
index 00000000..1a11ce2e
--- /dev/null
+++ b/src/errata-tests/ErrataTests.lean
@@ -0,0 +1,572 @@
+/-
+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
+
+Tests that exercise Errata using Errata itself.
+-/
+module
+
+public import Errata
+public meta import Errata
+import all ErrataTests.Fixture
+import all ErrataTests.Fixture.Sub
+
+open Errata
+
+/-- A bare boolean is a passing test. -/
+@[test]
+def onePlusOne : Bool := 1 + 1 == 2
+
+/-- An assertion-based test. -/
+@[test]
+def equality : Test := do
+  assertEq 4 (2 + 2)
+
+/-- A test with named results. -/
+@[test]
+def named : Test := do
+  result "first" (assertEq 1 1)
+  result "second" (assertContains "b" "abc")
+
+/-- A test that completes without any check is a bare success. -/
+@[test]
+def emptyBody : Test := pure ()
+
+/-- A test that expects a failure. -/
+@[test]
+def expectsFailure : Test :=
+  expectFail (assertEq 1 2)
+
+/-- A data-driven family expressed as a plain loop. -/
+@[test]
+def squares : Test := do
+  for (n, sq) in [(1, 1), (2, 4), (3, 9)] do
+    result s!"square {n}" (assertEq sq (n * n))
+
+/-- A subprocess test. -/
+@[test]
+def echoRuns : Test := do
+  let out ← IO.Process.output { cmd := "echo", args := #["hello"] }
+  assertExitCode 0 out
+  assertContains "hello" out.stdout
+
+/-- info: 3 -/
+#test_msgs in
+#eval 1 + 2
+
+-- The expected block is read from the source, so `#test_msgs` works in verso docstring mode.
+set_option doc.verso true in
+/-- info: 7 -/
+#test_msgs in
+#eval 3 + 4
+
+/--
+error: Module `NoSuchModule` is not imported, so its tests cannot be reached. Import it, using `import all NoSuchModule` if it belongs to the module system.
+-/
+#test_msgs in
+example : Array TestEntry := getAllTests% "verso" NoSuchModule
+
+/-- A module below several named roots contributes its tests once. -/
+@[test]
+def discoveryDeduplicates : Test := do
+  -- `ErrataTests.Fixture.Sub` lies below both roots, so exactly the two fixture tests are found.
+  let entries := (getAllTests% "verso" ErrataTests.Fixture ErrataTests.Fixture.Sub)
+  assertEq 2 entries.size
+
+/-- A property test. -/
+@[test]
+def addComm : Test :=
+  property (∀ a b : Nat, a + b = b + a)
+
+open Lean (toJson fromJson?)
+
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Lean.Position
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Location
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for TestFailure
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Status
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Output
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for OutputLog
+deriving instance Plausible.Shrinkable, Plausible.Arbitrary for Result
+
+/-- The JSON encoding of a result round-trips: decoding the encoding recovers the result. -/
+@[test]
+def jsonRoundTrips : Test :=
+  property (∀ r : Result, (fromJson? (toJson r)).toOption = some r)
+
+/-- A temp-directory fixture with a golden file. -/
+@[test]
+def goldenRoundTrip : Test :=
+  IO.FS.withTempDir fun dir => do
+    let goldenPath := dir / "expected.txt"
+    IO.FS.writeFile goldenPath "contents\n"
+    assertFileExists goldenPath
+    goldenFile goldenPath "contents\n"
+
+/-- A golden file is written through directories that do not exist yet. -/
+@[test]
+def goldenFileCreatesDirectories : Test :=
+  IO.FS.withTempDir fun dir =>
+    withReader ({ · with updateGolden := true }) do
+      let goldenPath := dir / "nested" / "deeper" / "expected.txt"
+      goldenFile goldenPath "contents\n"
+      assertFileExists goldenPath
+
+/-- Runs one action as a test in a fresh context, returning the results it recorded. -/
+private def resultsOf (act : Test) : TestM (Array Result) := do
+  let cfg ← mkContext
+  runEntry cfg <|
+    TestEntry.of "p" "M" "inner" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } act
+
+/-- A missing produced directory is a golden failure at the call site, not a bare error. -/
+@[test]
+def goldenDirReportsMissingOutput : Test := do
+  let results ← IO.FS.withTempDir fun dir =>
+    resultsOf (goldenDir (dir / "expected") (dir / "never-created"))
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .fail _)
+
+/-- A produced directory with no files in it can be recorded and then compared. -/
+@[test]
+def goldenDirHandlesEmptyOutput : Test := do
+  let results ← IO.FS.withTempDir fun dir => do
+    let expected := dir / "expected"
+    let actual := dir / "actual"
+    IO.FS.createDirAll actual
+    resultsOf do
+      withReader ({ · with updateGolden := true }) (goldenDir expected actual)
+      goldenDir expected actual
+  assertEq 1 results.size
+  assertTrue results[0]!.status.isSuccess
+
+/-- Updating absorbs a path that changed shape between file and directory, in both directions. -/
+@[test]
+def goldenDirUpdatesAcrossShapeChanges : Test := do
+  let results ← IO.FS.withTempDir fun dir => do
+    let expected := dir / "expected"
+    let actual := dir / "actual"
+    IO.FS.createDirAll expected
+    IO.FS.writeFile (expected / "d") "was a file\n"
+    IO.FS.createDirAll (actual / "d")
+    IO.FS.writeFile (actual / "d" / "inner") "now a directory\n"
+    resultsOf do
+      -- First update: the golden file `d` becomes a directory holding `inner`.
+      withReader ({ · with updateGolden := true }) (goldenDir expected actual)
+      goldenDir expected actual
+      -- Second update, the other way: the produced `d` is a file again.
+      IO.FS.removeDirAll (actual / "d")
+      IO.FS.writeFile (actual / "d") "a file once more\n"
+      withReader ({ · with updateGolden := true }) (goldenDir expected actual)
+      goldenDir expected actual
+  assertEq 1 results.size
+  assertTrue results[0]!.status.isSuccess
+
+/-- A file where a directory was expected is a golden failure, not a raw error. -/
+@[test]
+def goldenDirRejectsNonDirectory : Test := do
+  let results ← IO.FS.withTempDir fun dir => do
+    let actual := dir / "actual"
+    IO.FS.writeFile actual "not a directory\n"
+    resultsOf (goldenDir (dir / "expected") actual)
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .fail _)
+
+/-- A directory standing where the golden tree has a file is a missing file, not a pass. -/
+@[test]
+def goldenDirRejectsDirectoryForFile : Test := do
+  let results ← IO.FS.withTempDir fun dir => do
+    let expected := dir / "expected"
+    let actual := dir / "actual"
+    writeFile (expected / "d") "contents\n"
+    IO.FS.createDirAll (actual / "d")
+    resultsOf (goldenDir expected actual)
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .fail _)
+
+/-- A file standing where the golden tree has a directory is a golden failure, not a raw error. -/
+@[test]
+def goldenDirRejectsFileForDirectory : Test := do
+  let results ← IO.FS.withTempDir fun dir => do
+    let expected := dir / "expected"
+    let actual := dir / "actual"
+    writeFile (expected / "d" / "inner") "contents\n"
+    writeFile (actual / "d") "not a directory\n"
+    resultsOf (goldenDir expected actual)
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .fail _)
+
+/-- Output written before a failure reaches the enclosing result, where it explains the failure. -/
+@[test]
+def captureOutputKeepsOutputOnFailure : Test := do
+  let results ← resultsOf (discard <| captureOutput (do IO.println "diagnostic"; fail "boom"))
+  assertEq 1 results.size
+  let r := results[0]!
+  assertTrue (r.status matches .fail _)
+  assertContains "diagnostic" r.output.all
+
+/-- Output from an action that completes stays with the capture, rather than reaching the result. -/
+@[test]
+def captureOutputDivertsOnSuccess : Test := do
+  let results ← resultsOf do
+    let captured ← captureOutput (IO.println "quiet")
+    assertContains "quiet" captured.all
+  assertEq 1 results.size
+  assertTrue results[0]!.status.isSuccess
+  assertTrue results[0]!.output.isEmpty
+
+/-- A raw write may end partway through a code point; the write that completes it is joined on. -/
+@[test]
+def captureJoinsSplitWrites : Test := do
+  let bytes := "é".toUTF8
+  let captured ← captureOutput do
+    let out ← IO.getStdout
+    out.write (bytes.extract 0 1)
+    out.write (bytes.extract 1 bytes.size)
+  assertEq "é" captured.stdout
+
+/-- Bytes whose code point is never completed are an error, not silently dropped. -/
+@[test]
+def captureRejectsDanglingBytes : Test := do
+  let results ← resultsOf do
+    let out ← IO.getStdout
+    out.write ("é".toUTF8.extract 0 1)
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .error _)
+
+/-- Under --wfail, an option no test read fails the run instead of only warning. -/
+@[test]
+def wfailPromotesUnusedOptions : Test := do
+  let entry := TestEntry.of "p" "M" "t"
+    { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } (pure () : Test)
+  let lax ← IO.mkRef (0 : UInt32)
+  let wfail ← IO.mkRef (0 : UInt32)
+  discard <| captureOutput do
+    lax.set (← runMain #[entry] ["--", "--bogus=1"])
+    wfail.set (← runMain #[entry] ["--wfail", "--", "--bogus=1"])
+  assertEq 0 (← lax.get)
+  assertEq 1 (← wfail.get)
+
+/-- The detail given to a true-assertion is attached to its failure. -/
+@[test]
+def assertTrueAttachesDetail : Test := do
+  let results ← resultsOf (assertTrue false "boom" (detail? := some "why"))
+  assertEq 1 results.size
+  match results[0]!.status with
+  | .fail f => assertEq (some "why") f.detail?
+  | s => fail s!"expected a failure, got {repr s}"
+
+/-- An expected IO error passes, and the predicate picks which errors are acceptable. -/
+@[test]
+def assertThrowsIOAccepts : Test := do
+  assertThrowsIO (throw (IO.userError "nope") : IO Unit)
+  assertThrowsIO (throw (IO.userError "nope") : IO Unit)
+    (acceptable := fun e => e matches .userError _)
+
+/-- A successful action fails the throw assertion, as does an error the predicate rejects. -/
+@[test]
+def assertThrowsIORejects : Test := do
+  expectFail (assertThrowsIO (pure () : IO Unit))
+  expectFail <|
+    assertThrowsIO (throw (IO.userError "nope") : IO Unit) (acceptable := fun _ => false)
+
+/-- Output mixed from raw writes and prints is recorded in the order it was produced. -/
+@[test]
+def captureOrdersMixedWrites : Test := do
+  let captured ← captureOutput do
+    let out ← IO.getStdout
+    out.write "é".toUTF8
+    IO.print "x"
+    out.write "û".toUTF8
+  assertEq "éxû" captured.stdout
+
+/-- Text printed while a raw code point is unfinished is malformed output, not reordered output. -/
+@[test]
+def capturePrintDuringPartialWriteRejected : Test := do
+  let results ← resultsOf do
+    let out ← IO.getStdout
+    out.write ("é".toUTF8.extract 0 1)
+    IO.print "x"
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .error _)
+
+/-- Dangling bytes at the end of a failing test do not displace the test's own failure. -/
+@[test]
+def danglingBytesKeepFailure : Test := do
+  let results ← resultsOf do
+    let out ← IO.getStdout
+    out.write ("é".toUTF8.extract 0 1)
+    fail "the real failure"
+  assertEq 1 results.size
+  match results[0]!.status with
+  | .fail f => assertEq "the real failure" f.message
+  | s => fail s!"expected the assertion failure, got {repr s}"
+
+/-- A raw write with no valid decoding is rejected at the write itself. -/
+@[test]
+def captureRejectsInvalidBytes : Test := do
+  let results ← resultsOf do
+    let out ← IO.getStdout
+    out.write (ByteArray.mk #[0xFF])
+  assertEq 1 results.size
+  assertTrue (results[0]!.status matches .error _)
+
+/--
+A live output destination writes to the real stdout, so printing from it does not re-enter the
+capture. The counter is bounded so that a regression fails this test instead of exhausting the stack.
+-/
+@[test]
+def writeOutputDoesNotRecurse : Test := do
+  let depth ← IO.mkRef 0
+  let cfg ← mkContext
+  let ctx := { cfg with
+    writeOutput := some fun o => do
+      depth.modify (· + 1)
+      if (← depth.get) < 5 then
+        match o with
+        | .stdout s => IO.print s
+        | .stderr s => IO.eprint s }
+  discard <| runEntry ctx <|
+    TestEntry.of "p" "M" "prints" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ }
+      (IO.println "live" : Test)
+  assertEq 1 (← depth.get)
+
+/--
+A fragment printed inside a nested result reaches the live output destination exactly once. The
+destination is cut off after a few fragments so that a regression fails this test with a short
+array instead of flooding it.
+-/
+@[test]
+def writeOutputDeliversNestedFragmentsOnce : Test := do
+  let received ← IO.mkRef (#[] : Array String)
+  let cfg ← mkContext
+  let ctx := { cfg with
+    writeOutput := some fun o => do
+      if (← received.get).size < 5 then
+        match o with
+        | .stdout s => received.modify (·.push s); IO.print s
+        | .stderr s => IO.eprint s }
+  discard <| runEntry ctx <|
+    TestEntry.of "p" "M" "nested" { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ }
+      (result "inner" (IO.println "hi") : Test)
+  assertEq #["hi\n"] (← received.get)
+
+/--
+A live output destination that fails does not fail the test that happened to be printing. It is
+reported once and then left alone, rather than retried for every fragment.
+-/
+@[test]
+def writeOutputFailureIsContained : Test := do
+  let calls ← IO.mkRef 0
+  let statuses ← IO.mkRef (#[] : Array Status)
+  let cfg ← mkContext
+  let ctx := { cfg with
+    writeOutput := some fun _ => do
+      calls.modify (· + 1)
+      throw (.userError "broken pipe") }
+  let out ← captureOutput do
+    for name in ["first", "second"] do
+      let entry := TestEntry.of "p" "M" name
+        { file := "f", startPos := ⟨0, 0⟩, endPos := ⟨0, 0⟩ } (IO.println "output" : Test)
+      for r in ← runEntry ctx entry do
+        statuses.modify (·.push r.status)
+  result "the printing tests are not blamed" do
+    assertTrue ((← statuses.get).all (·.isSuccess))
+  result "the destination is left alone after it fails" do
+    assertEq 1 (← calls.get)
+  result "the failure is reported" do
+    assertContains "live output destination failed" out.all
+
+/-- A failure that a nested `result` recorded still satisfies `expectFail`. -/
+@[test]
+def expectFailSeesNestedResult : Test := do
+  let results ← resultsOf (expectFail (result "inner" (assertEq 1 2)))
+  assertEq 1 results.size
+  assertTrue results[0]!.status.isSuccess
+
+/-- An error inside `expectFail` is not an expected failure, even when a nested `result` records it. -/
+@[test]
+def expectFailRejectsNestedError : Test := do
+  let results ← resultsOf <|
+    expectFail (result "inner" (show IO Unit from throw (.userError "broken setup")))
+  assertTrue (results.any (!·.status.isSuccess))
+
+/-- An error inside `expectFail` stands even when a sibling result recorded a failure. -/
+@[test]
+def expectFailKeepsErrorBesideFailure : Test := do
+  let results ← resultsOf <| expectFail do
+    result "a" <| assertEq 1 2
+    result "b" <| show IO Unit from throw (.userError "broken setup")
+  assertTrue (results.any (·.status matches .error _))
+
+/-- A nested failure satisfies `expectFail` whether or not the action goes on to throw. -/
+@[test]
+def expectFailAgreesAcrossPaths : Test := do
+  let thrown ← resultsOf (expectFail (do result "a" (assertEq 1 2); assertEq 3 4))
+  let recorded ← resultsOf (expectFail (do result "a" (assertEq 1 2); result "b" (assertEq 3 4)))
+  result "action throws afterwards" (assertTrue (thrown.all (·.status.isSuccess)))
+  result "action records only" (assertTrue (recorded.all (·.status.isSuccess)))
+
+/-- Results other than the expected failure survive `expectFail`. -/
+@[test]
+def expectFailKeepsPassingResults : Test := do
+  let results ← resultsOf <| expectFail do
+    result "ok" (assertEq 1 1)
+    result "a" (assertEq 1 2)
+  assertTrue (results.any (fun r => r.status.isSuccess && r.testName.endsWith "ok"))
+
+-- `here%` reports its own position, so the expected column below is the indentation of the line it
+-- sits on, and the expected span is the five characters of the token itself.
+def indentedHere : Location :=
+  here%
+
+/-- Source positions follow Lean's convention: lines count from one and columns from zero. -/
+@[test]
+def positionConvention : Test := do
+  assertEq 2 indentedHere.startPos.column
+  assertEq 5 (indentedHere.endPos.column - indentedHere.startPos.column)
+
+/-- The `Verbosity` predicates behave as the report relies on. -/
+@[test]
+def verbosityLevels : Test := do
+  assertEq false Verbosity.silent.showsPasses
+  assertEq true Verbosity.quiet.showsPasses
+  assertEq true Verbosity.verbose.showsPasses
+  assertEq true Verbosity.superVerbose.showsPasses
+  assertEq false Verbosity.silent.truncates
+  assertEq true Verbosity.quiet.truncates
+  assertEq false Verbosity.verbose.truncates
+  assertEq false Verbosity.superVerbose.truncates
+  assertEq false Verbosity.verbose.showsAllDocstrings
+  assertEq true Verbosity.superVerbose.showsAllDocstrings
+
+/--
+The runner's command line: the `-v` forms select the verbosity, declared flags parse, and options
+for the tests go after `--`.
+-/
+@[test]
+def runnerArgParsing : Test := do
+  result "default verbosity" do
+    assertEq (some Verbosity.silent) ((parseOptions []).toOption.map (·.verbosity))
+  result "-v" do
+    assertEq (some Verbosity.quiet) ((parseOptions ["-v"]).toOption.map (·.verbosity))
+  result "--verbose" do
+    assertEq (some Verbosity.quiet) ((parseOptions ["--verbose"]).toOption.map (·.verbosity))
+  result "-vv" do
+    assertEq (some Verbosity.verbose) ((parseOptions ["-vv"]).toOption.map (·.verbosity))
+  result "-vvv" do
+    assertEq (some Verbosity.superVerbose) ((parseOptions ["-vvv"]).toOption.map (·.verbosity))
+  result "update-golden" do
+    assertEq (some true) ((parseOptions ["--update-golden"]).toOption.map (·.updateGolden))
+  result "seed" do
+    assertEq (some (some 42)) ((parseOptions ["--seed", "42"]).toOption.map (·.seed))
+  result "non-numeric seed rejected" do
+    assertTrue ((parseOptions ["--seed", "x"]) matches .error _)
+  result "junit path" do
+    assertEq (some (some "r.xml")) ((parseOptions ["--junit", "r.xml"]).toOption.map (·.junitPath))
+  result "missing junit path rejected" do
+    assertTrue ((parseOptions ["--junit"]) matches .error _)
+  result "test options after --" do
+    let opts := (parseOptions ["--", "--golden", "on", "--flag=v=1", "--golden", "two"]).toOption
+    assertEq (some #["on", "two"]) (opts.map (·.options.getD "golden" #[]))
+    assertEq (some #["v=1"]) (opts.map (·.options.getD "flag" #[]))
+  result "valueless test option" do
+    assertEq (some #[""]) ((parseOptions ["--", "--fast"]).toOption.map (·.options.getD "fast" #[]))
+  result "unknown flag rejected" do
+    assertTrue ((parseOptions ["--golden", "on"]) matches .error _)
+  result "misplaced library name diagnosed" do
+    match parseOptions ["--verbose", "ErrataTests"] with
+    | .error msg => assertContains "ErrataTests" msg
+    | .ok _ => assertTrue false "expected an error"
+
+/-- A run that discovers nothing fails: a test tool with no tests is a broken setup, not a pass. -/
+@[test]
+def emptyRunFails : Test := do
+  let code ← IO.mkRef (0 : UInt32)
+  let out ← captureOutput do
+    code.set (← runMain #[] [])
+  assertContains "no tests were discovered" out.all
+  assertEq 1 (← code.get).toNat
+
+/-- At silent verbosity the report hides passes but shows failures and the summary line. -/
+@[test]
+def reportSilent : Test := do
+  let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass }
+  let fail : Result := { package := "p", moduleName := "M", test := "u", status := .fail { message := "boom" } }
+  let out ← captureOutput do discard <| humanReport .silent #[pass, fail]
+  assertContains "FAIL  p/M  u: boom" out.stdout
+  assertContains "1 passed, 1 failed, 0 errors, 0 skipped" out.stdout
+  assertEq 1 (out.stdout.splitOn "ok    ").length
+
+/-- At verbose verbosity the report shows passes too. -/
+@[test]
+def reportVerbose : Test := do
+  let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass }
+  let out ← captureOutput do discard <| humanReport .verbose #[pass]
+  assertContains "ok    p/M  t" out.stdout
+
+/-- Characters XML 1.0 forbids are dropped from the JUnit report rather than emitted. -/
+@[test]
+def junitDropsForbiddenChars : Test := do
+  let bad := (Char.ofNat 0xFFFF).toString ++ (Char.ofNat 0xFFFE).toString ++ (Char.ofNat 0x1).toString
+  let r : Result := { package := "p", moduleName := "M", test := "t",
+                      status := .fail { message := s!"bad{bad}char" } }
+  let xml := junitReport #[r]
+  assertContains "badchar" xml
+  assertTrue (!xml.contains (Char.ofNat 0xFFFF) && !xml.contains (Char.ofNat 0xFFFE))
+
+/-- A test's results are truncated after the cap at quiet verbosity, with a summary, but not at verbose. -/
+@[test]
+def reportTruncates : Test := do
+  let many := (Array.range 60).map fun i =>
+    ({ package := "p", moduleName := "M", test := "many", resultPath := #[s!"case {i}"], status := .pass } : Result)
+  let quiet ← captureOutput do discard <| humanReport .quiet many
+  assertEq 51 (quiet.stdout.splitOn "ok    ").length
+  assertContains "(... and 10 more passed)" quiet.stdout
+  let verbose ← captureOutput do discard <| humanReport .verbose many
+  assertEq 61 (verbose.stdout.splitOn "ok    ").length
+  assertEq 1 (verbose.stdout.splitOn "(... and").length
+
+/--
+Truncation never suppresses a failure or error: past the cap they print in full and only the passes
+around them are summarized.
+-/
+@[test]
+def reportTruncationShowsFailures : Test := do
+  let many := (Array.range 60).map fun i =>
+    let status : Status := if i == 55 then .fail { message := "boom" } else .pass
+    ({ package := "p", moduleName := "M", test := "many", resultPath := #[s!"case {i}"], status } : Result)
+  let quiet ← captureOutput do discard <| humanReport .quiet many
+  assertContains "FAIL  p/M  many.case 55: boom" quiet.stdout
+  assertContains "(... and 9 more passed)" quiet.stdout
+
+/-- `humanReport` returns the number of failures and errors. -/
+@[test]
+def reportFailureCount : Test := do
+  let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass }
+  let fail : Result := { package := "p", moduleName := "M", test := "u", status := .fail { message := "x" } }
+  let err : Result := { package := "p", moduleName := "M", test := "v", status := .error "oops" }
+  assertEq 2 (← humanReport .silent #[pass, fail, err])
+
+/-- `markdownReport` gives a tally, an open collapsible per failure, and a per-module table. -/
+@[test]
+def reportMarkdown : Test := do
+  let pass : Result := { package := "p", moduleName := "M", test := "t", status := .pass }
+  let f : TestFailure := { message := "boom", detail? := some "expected 1\nactual 2" }
+  let fail : Result := { package := "p", moduleName := "M", test := "u", status := .fail f }
+  let md := markdownReport #[pass, fail]
+  assertContains "**1** passed · **1** failed" md
+  assertContains "<details open><summary>❌ <code>p/M</code> u: boom</summary>" md
+  assertContains "expected 1\nactual 2" md
+  assertContains "Summary by module" md
+
+/-- `failure` from the `Alternative` instance fails a test. -/
+@[test]
+def alternativeFailure : Test := expectFail failure
+
+/-- `<|>` recovers from an assertion failure by running the alternative. -/
+@[test]
+def alternativeOrElse : Test := failure <|> assertEq 1 1
+
+-- Two guards whose first source line is identical must get distinct generated names.
+#test_guard 1 + 1 == 2
+#test_guard 1 + 1 == 2
diff --git a/src/errata-tests/ErrataTests/Fixture.lean b/src/errata-tests/ErrataTests/Fixture.lean
new file mode 100644
index 00000000..13e2317c
--- /dev/null
+++ b/src/errata-tests/ErrataTests/Fixture.lean
@@ -0,0 +1,17 @@
+/-
+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
+
+A module holding a test, for checks of test discovery itself. Its name is a prefix of
+`ErrataTests.Fixture.Sub`'s name.
+-/
+module
+
+public import Errata
+
+open Errata
+
+/-- A test in the fixture module. -/
+@[test]
+def fixtureTest : Bool := true
diff --git a/src/errata-tests/ErrataTests/Fixture/Sub.lean b/src/errata-tests/ErrataTests/Fixture/Sub.lean
new file mode 100644
index 00000000..9e62f275
--- /dev/null
+++ b/src/errata-tests/ErrataTests/Fixture/Sub.lean
@@ -0,0 +1,17 @@
+/-
+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
+
+A module holding a test, for checks of test discovery itself. Its name extends
+`ErrataTests.Fixture`'s name, so it lies below that module as well as below itself.
+-/
+module
+
+public import Errata
+
+open Errata
+
+/-- A test in the nested fixture module. -/
+@[test]
+def subFixtureTest : Bool := true
diff --git a/src/errata/Errata.lean b/src/errata/Errata.lean
new file mode 100644
index 00000000..1760f91c
--- /dev/null
+++ b/src/errata/Errata.lean
@@ -0,0 +1,22 @@
+/-
+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.Result
+public import Errata.Context
+public import Errata.Here
+public import Errata.TestM
+public import Errata.IsTest
+public import Errata.Assertions
+public import Errata.Process
+public import Errata.Golden
+public import Errata.Report
+public import Errata.Runner
+public import Errata.Discovery
+public import Errata.CompileTime
+public import Errata.Property
+
+set_option doc.verso true
diff --git a/src/errata/Errata/Assertions.lean b/src/errata/Errata/Assertions.lean
new file mode 100644
index 00000000..91c11b7c
--- /dev/null
+++ b/src/errata/Errata/Assertions.lean
@@ -0,0 +1,83 @@
+/-
+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.TestM
+public import Errata.Here
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- Asserts that a condition holds, attaching the detail to the failure when given. -/
+def assertTrue (cond : Bool) (message : String := "assertion failed")
+    (detail? : Option String := none) (loc : Location := by exact here%) : TestM Unit :=
+  unless cond do failAt loc message (detail? := detail?)
+
+/-- Asserts that the actual value equals the expected value, reporting both when they differ. -/
+def assertEq {α} [BEq α] [Repr α] (expected actual : α)
+    (loc : Location := by exact here%) : TestM Unit :=
+  unless actual == expected do
+    failAt loc "values are not equal" (detail? := some s!"expected: {repr expected}\nactual:   {repr actual}")
+
+/-- Asserts that the actual value differs from the unexpected value. -/
+def assertNe {α} [BEq α] [Repr α] (unexpected actual : α)
+    (loc : Location := by exact here%) : TestM Unit := do
+  if actual == unexpected then
+    failAt loc "values are equal but should differ" (detail? := some s!"both: {repr actual}")
+
+/-- Asserts that the actual string contains the expected substring. -/
+def assertContains (expected actual : String) (message : String := "substring not found")
+    (loc : Location := by exact here%) : TestM Unit := do
+  unless (actual.find? expected).isSome do
+    failAt loc message (detail? := some s!"expected to contain: {expected}\nactual: {actual}")
+
+/-- Asserts that the actual string does not contain the unexpected substring. -/
+def assertNotContains (unexpected actual : String) (message : String := "unexpected substring found")
+    (loc : Location := by exact here%) : TestM Unit :=
+  unless (actual.find? unexpected).isNone do
+    failAt loc message (detail? := some s!"expected not to contain: {unexpected}\nactual: {actual}")
+
+/--
+Asserts that an action throws an {name}`IO.Error`. The predicate picks the subset of acceptable
+errors: the assertion fails when the action succeeds, and when it throws an error the predicate
+rejects. The name says {lit}`IO` because the expectation is about a thrown {name}`IO.Error`, as
+opposed to failure in some other error monad.
+-/
+def assertThrowsIO {α} (act : IO α) (acceptable : IO.Error → Bool := fun _ => true)
+    (loc : Location := by exact here%) : TestM Unit := do
+  match ← act.toBaseIO with
+  | .ok _ => failAt loc "expected an IO error, but the action succeeded"
+  | .error e =>
+    unless acceptable e do
+      failAt loc "the action threw an unacceptable IO error" (detail? := some (toString e))
+
+/-- Asserts that a file exists. -/
+def assertFileExists (path : System.FilePath)
+    (loc : Location := by exact here%) : TestM Unit := do
+  unless ← path.pathExists do
+    failAt loc s!"file does not exist: {path}"
+
+/-- Asserts that an option is absent. -/
+def assertNone {α} [Repr α] (value : Option α)
+    (loc : Location := by exact here%) : Test := do
+  if let some v := value then
+    failAt loc s!"expected none, got {repr v}"
+
+/-- Asserts that an option is present, returning its contents. -/
+def assertSome {α} (value : Option α)
+    (loc : Location := by exact here%) : TestM α :=
+  match value with
+  | some v => pure v
+  | none => throw { message := "expected some, got none", location? := some loc }
+
+/-- Asserts that an option is present, without inspecting its contents. -/
+def assertIsSome {α} (value : Option α)
+    (loc : Location := by exact here%) : Test :=
+  discard (assertSome value loc)
diff --git a/src/errata/Errata/CompileTime.lean b/src/errata/Errata/CompileTime.lean
new file mode 100644
index 00000000..0213a6f0
--- /dev/null
+++ b/src/errata/Errata/CompileTime.lean
@@ -0,0 +1,154 @@
+/-
+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.Result
+public meta import Errata.CompileTime.Helpers
+public import Lean.Elab.Command
+public import Lean.Elab.GuardMsgs
+public import Lean.Data.Options
+
+open Lean Elab Command Errata.CompileTime
+
+public section
+
+set_option doc.verso true
+
+/--
+When true, a failing Errata compile-time test is an elaboration error rather than a warning.
+-/
+register_option errata.failOnError : Bool := {
+  defValue := false
+  descr := "Make a failing Errata compile-time test an elaboration error rather than a warning."
+}
+
+namespace Errata
+
+/--
+Checks that the command below produces the messages given in the preceding doc comment.
+
+This is a version of `#guard_msgs` that is specialized for use in Errata. If the messages
+don't match, it is not a compile-time error unless the option {lit}`errata.failOnError` is
+{name}`true`. This allows failing compile-time tests to appear in the test output together
+with failing run-time tests.
+-/
+syntax (name := testMsgsCmd) (plainDocComment)? "#test_msgs" "in" command : command
+
+@[command_elab testMsgsCmd]
+meta def elabTestMsgs : Command.CommandElab
+  | `($[$dc?:docComment]? #test_msgs%$tk in $cmd) => do
+    let expected := ((← dc?.mapM (getDocStringText ·)).getD "").trimAscii.copy
+    -- Elaborate the command, capturing its messages instead of letting them surface. Collection
+    -- covers the asynchronous snapshot tasks as well as the synchronous log, so messages from
+    -- linters, which run after elaboration, are included. Elaborating the command replaces the
+    -- message log, so the surrounding one is put back afterwards.
+    let saved := (← get).messages
+    let produced ← Lean.Elab.Tactic.GuardMsgs.runAndCollectMessages cmd
+    modify ({ · with messages := saved })
+    let visible := produced.toList.filter (!·.isSilent)
+    let strings ← (visible.mapM formatMessage : IO (List String))
+    -- Multiple messages are separated by `---`, matching the block `#guard_msgs` compares against.
+    let actual := ("---\n".intercalate strings).trimAscii.copy
+    let passed := messagesMatch expected actual
+    -- Reify the verdict into a discovered test, named after the source position. The module name
+    -- qualifies it so that two modules with a `#test_msgs` at the same position do not collide.
+    let fileMap ← getFileMap
+    let startPos := fileMap.toPosition (tk.getPos?.getD 0)
+    let endPos := fileMap.toPosition (tk.getTailPos?.getD (tk.getPos?.getD 0))
+    let declName := `_root_ ++ (← getMainModule) ++
+      Name.mkSimple s!"errataMsgTest_L{startPos.line}_C{startPos.column}"
+    let detail := s!"Expected:\n{expected}\n\nActual:\n{actual}"
+    let verdict ←
+      if passed then
+        `(Errata.TestResult.pass)
+      else
+        `(Errata.TestResult.mismatch "compile-time messages do not match" $(quote detail)
+            $(quote (← getFileName))
+            $(quote startPos.line) $(quote startPos.column)
+            $(quote endPos.line) $(quote endPos.column))
+    elabCommand (← `(@[test] def $(mkIdent declName) : Errata.TestResult := $verdict))
+    -- Report a mismatch at build time, offering the corrected expected block as a fix.
+    unless passed do
+      let fixRef := (dc?.map (·.raw)).getD tk
+      let hint ← liftCoreM <| MessageData.hint m!"Update the expected output:"
+        #[{ suggestion := suggestedDoc actual }] (ref? := some fixRef)
+      let body := m!"Errata #test_msgs: the messages do not match.\n\n{detail}"
+      if (← getOptions).getBool `errata.failOnError false then
+        logErrorAt tk (body ++ hint)
+      else
+        logWarningAt tk (body ++ hint)
+  | _ => throwUnsupportedSyntax
+
+/--
+Checks that a Boolean expression evaluates to {lean}`true`, registering the verdict as a test.
+
+This is a version of `#guard` that is specialized for use in Errata. If the condition does not
+hold, it is not a compile-time error unless the option {lit}`errata.failOnError` is
+{name}`true`. This allows failing compile-time tests to appear in the test output together
+with failing run-time tests.
+
+-/
+syntax (name := testGuardCmd) "#test_guard" term : command
+
+@[command_elab testGuardCmd]
+meta def elabTestGuard : Command.CommandElab
+  | `(#test_guard%$tk $e:term) => do
+    -- Evaluate the expression to a `Bool` at elaboration time, as `#guard` does.
+    let passed ← Command.liftTermElabM do
+      let v ← Term.elabTermEnsuringType e (mkConst ``Bool)
+      Term.synthesizeSyntheticMVarsNoPostponing
+      let v ← instantiateMVars v
+      let mvars ← Lean.Meta.getMVars v
+      if mvars.isEmpty then
+        unsafe Lean.Meta.evalExpr (checkMeta := false) Bool (mkConst ``Bool) v
+      else
+        discard <| Term.logUnassignedUsingErrorInfos mvars
+        pure false
+    -- The checked expression's source text and span, for naming, location, and detail.
+    let fileMap ← getFileMap
+    let startStr := e.raw.getPos?.getD 0
+    let endStr := e.raw.getTailPos?.getD startStr
+    let source := ({ str := fileMap.source, startPos := startStr, stopPos := endStr } : Substring.Raw).toString
+    let startPos := fileMap.toPosition startStr
+    let endPos := fileMap.toPosition endStr
+    -- Name the test after the first line of the expression, in the current namespace, marking a
+    -- truncated multi-line expression with an ellipsis and disambiguating against earlier ones.
+    let lines := source.splitOn "\n"
+    -- Strip guillemets so an escaped name in the source does not nest inside the test's own name.
+    let firstLine := lines.headD source |>.trimAscii |>.replace "«" "" |>.replace "»" ""
+    let base :=
+      if (lines.drop 1).any (fun l => !l.trimAscii.isEmpty) then firstLine ++ "…" else firstLine
+    let ns ← getCurrNamespace
+    let env ← getEnv
+    -- Use the module name as part of the test name to avoid conflicts
+    let modName ← getMainModule
+    -- `_root_` marks the name as absolute for the declaration, but it's not _really_ part of the name
+    let declared (n : String) : Name := modName ++ ns ++ Name.mkSimple n
+    let qualified (n : String) : Name := `_root_ ++ declared n
+    let mut name := base
+    let mut n := 1
+    -- In a `module`, the generated definition is private, so probe its mangled name as well.
+    while env.contains (declared name)
+        || env.contains (mkPrivateName env (declared name)) do
+      n := n + 1
+      name := s!"{base} ({n})"
+    let verdict ←
+      if passed then
+        `(Errata.TestResult.pass)
+      else
+        `(Errata.TestResult.mismatch "expression did not evaluate to `true`" $(quote source)
+            $(quote (← getFileName))
+            $(quote startPos.line) $(quote startPos.column)
+            $(quote endPos.line) $(quote endPos.column))
+    elabCommand (← `(@[test] def $(mkIdent (qualified name)) : Errata.TestResult := $verdict))
+    -- Report a failure at build time, as `#test_msgs` does.
+    unless passed do
+      let body := m!"Errata #test_guard: the expression did not evaluate to `true`:\n{source}"
+      if (← getOptions).getBool `errata.failOnError false then
+        logErrorAt tk body
+      else
+        logWarningAt tk body
+  | _ => throwUnsupportedSyntax
diff --git a/src/errata/Errata/CompileTime/Helpers.lean b/src/errata/Errata/CompileTime/Helpers.lean
new file mode 100644
index 00000000..50f58f87
--- /dev/null
+++ b/src/errata/Errata/CompileTime/Helpers.lean
@@ -0,0 +1,48 @@
+/-
+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
+
+Non-meta helpers for the `#test_msgs` command, kept separate so the command elaborator is the
+only meta definition.
+-/
+module
+
+public import Lean.Message
+public import Lean.Elab.GuardMsgs
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata.CompileTime
+
+/-- Renders a message with a severity prefix, in the form the expected block is compared against. -/
+def formatMessage (msg : Lean.Message) : IO String := do
+  let mut str ← msg.data.toString
+  unless msg.caption == "" do
+    str := msg.caption ++ ":\n" ++ str
+  -- The severity is followed by a space only when the body stays on the same line, matching the
+  -- rendering that `#guard_msgs` compares against.
+  unless str.startsWith "\n" do str := " " ++ str
+  str :=
+    if msg.isTrace then "trace:" ++ str
+    else match msg.severity with
+      | .information => "info:" ++ str
+      | .warning => "warning:" ++ str
+      | .error => "error:" ++ str
+  unless str.endsWith "\n" do str := str ++ "\n"
+  return str
+
+open Lean.Elab.Tactic.GuardMsgs (WhitespaceMode) in
+/-- Whether the expected and actual message blocks match, normalizing whitespace as `#guard_msgs` does. -/
+def messagesMatch (expected actual : String) : Bool :=
+  let norm := fun s => (WhitespaceMode.normalized.apply s).trimAscii.copy
+  norm expected == norm actual
+
+/-- The doc comment that would make the expected block match the actual output. -/
+def suggestedDoc (actual : String) : String :=
+  if actual.isEmpty then ""
+  else if actual.contains '\n' then s!"/--\n{actual}\n-/\n"
+  else s!"/-- {actual} -/\n"
diff --git a/src/errata/Errata/Context.lean b/src/errata/Errata/Context.lean
new file mode 100644
index 00000000..155ae9ab
--- /dev/null
+++ b/src/errata/Errata/Context.lean
@@ -0,0 +1,74 @@
+/-
+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 Std.Data.HashSet
+public import Errata.Result
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+open Std (HashMap HashSet)
+
+/-- A multi-map from option names to all the values supplied for them. -/
+abbrev OptionMap := HashMap String (Array String)
+
+/-- The standard streams from before a test's output was captured. -/
+structure RealStreams where
+  /-- The stdout from before the capture. -/
+  stdout : IO.FS.Stream
+  /-- The stderr from before the capture. -/
+  stderr : IO.FS.Stream
+
+/-- The run-wide configuration and per-test state threaded through every test. -/
+structure Context where
+  /-- Whether golden checks rewrite their expected files instead of comparing. -/
+  updateGolden : Bool := false
+  /-- Project-specific options, as a multi-map so repeated options accumulate. -/
+  options : OptionMap := {}
+  /-- The seed used for property tests, or {lean}`none` to draw a fresh one. -/
+  seed : Option Nat := none
+  /-- The package that defines the running test. -/
+  package : String := ""
+  /-- The module that defines the running test, as a dotted name. -/
+  moduleName : String := ""
+  /-- The running test declaration's name below its module. -/
+  test : String := ""
+  /-- The running test's docstring, rendered as Markdown, when it has one. -/
+  description? : Option String := none
+  /-- The named result currently being recorded, below the test. -/
+  resultPath : Array String := #[]
+  /--
+  The source location reported for the next failure. The runner seeds it with the test's own
+  source range; the assertion language refines it to each call site.
+  -/
+  location : Location := default
+  /-- The results collected so far during the current test. -/
+  log : IO.Ref (Array Result)
+  /-- The option names read during the run, shared across all tests, for reporting unused options. -/
+  usedOptions : IO.Ref (HashSet String)
+  /--
+  Receives each captured output fragment as it is written, in order. A live runner sets it to
+  stream output as the test produces it, and it is {lean}`none` when no runner is listening.
+
+  It runs with the streams that were in place before the test's output was redirected, so it may
+  print in case of internal errors.
+  -/
+  writeOutput : Option (Output → IO Unit) := none
+  /--
+  Whether a write to the output destination has failed. If true, further attempts are suppressed.
+  -/
+  outputFailed : IO.Ref Bool
+  /--
+  The streams from before the outermost capture, under which the output destination runs. The
+  outermost capture records them, and a capture nested inside it reuses them, so a {lit}`writeOutput`
+  handler that prints reaches the runner's own streams from any nesting depth.
+  -/
+  realStreams? : Option RealStreams := none
diff --git a/src/errata/Errata/Discovery.lean b/src/errata/Errata/Discovery.lean
new file mode 100644
index 00000000..0ef020b6
--- /dev/null
+++ b/src/errata/Errata/Discovery.lean
@@ -0,0 +1,144 @@
+/-
+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 Errata.Runner
+public import Lean
+public meta import Lean
+
+open Lean Meta Elab Term
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/--
+Verifies that a tagged declaration can be run as a test: it is not {lit}`meta`, and it has an
+{name}`IsTest` instance.
+-/
+meta def checkIsTest (decl : Name) : MetaM Unit := do
+  let env ← getEnv
+  if isMarkedMeta env decl then
+    throwError m!"A test must not be `meta`"
+  let info ← getConstInfo decl
+  let goal := mkApp (mkConst ``IsTest) info.type
+  match ← trySynthInstance goal with
+  | .some _ => pure ()
+  | _ =>
+    throwError m!"`@[test]` requires an `Errata.IsTest` instance for the test's type{indentExpr info.type}"
+
+/--
+A recorded test: its declaration name and the source file that defines it. The file is captured
+when the attribute is applied; the declaration's line and column are recovered later, once the
+declaration ranges are available.
+-/
+structure TestDecl where
+  /-- The test declaration's name. -/
+  name : Name
+  /-- The source file that defines the test. -/
+  file : String
+  /-- The test's docstring, rendered as Markdown, captured when the attribute is applied. -/
+  docstring? : Option String := none
+deriving Inhabited
+
+/--
+The tests recorded by {lit}`@[test]`, per module. The attribute is an elaboration-time feature:
+tests are recorded as modules are elaborated, and {lit}`getAllTests%` reads them back at elaboration
+time to build the runnable test array.
+-/
+meta initialize testExt : SimplePersistentEnvExtension TestDecl (Array TestDecl) ←
+  registerSimplePersistentEnvExtension {
+    name := `Errata.test
+    addEntryFn := Array.push
+    addImportedFn := fun es => es.foldl Array.append #[]
+  }
+
+/--
+Records a declaration as a test, capturing the source file that defines it and its docstring.
+The docstring is read here, while it is still in the live environment, since a downstream build does
+not load the imported docstrings.
+-/
+meta def recordTest (decl : Name) : AttrM Unit := do
+  (checkIsTest decl).run'
+  let docstring? ← findDocString? (← getEnv) decl
+  modifyEnv (testExt.addEntry · { name := decl, file := ← getFileName, docstring? })
+
+/-- Marks a definition as a test, discovered and run by the Errata test runner. -/
+meta initialize
+  registerBuiltinAttribute {
+    ref := `Errata.test
+    name := `test
+    descr := "Marks a definition as a test, discovered and run by the Errata test runner."
+    -- Applied after compilation so the declaration's docstring is in the environment to capture.
+    applicationTime := .afterCompilation
+    add := fun decl stx kind => do
+      Attribute.Builtin.ensureNoArgs stx
+      unless kind == AttributeKind.global do throwAttrMustBeGlobal `test kind
+      recordTest decl
+  }
+
+/-- The test's name below its module: the declaration's components past the module prefix, dotted. -/
+meta def testNameBelow (moduleName declName : Name) : String :=
+  let below :=
+    if moduleName.isPrefixOf declName then declName.components.drop moduleName.components.length
+    else declName.components
+  ".".intercalate (below.map (·.toString))
+
+/--
+{lit}`getAllTests% "package" Mod.A Mod.B ...` reads the tests recorded by {lit}`@[test]` in the
+named modules and every imported module below them, and expands to the array of {name}`TestEntry`
+values that run them. A module that lies below more than one of the named modules contributes its
+tests once. Each module must be imported, with {lit}`import all` for module-system modules, so its
+tests are reachable.
+-/
+syntax (name := getAllTests) "getAllTests%" str ident* : term
+
+/-- Expands {lit}`getAllTests%` by reading the recorded tests of the named modules. -/
+@[term_elab getAllTests]
+meta def elabGetAllTests : TermElab := fun stx expectedType? => do
+  let `(getAllTests% $pkg:str $mods:ident*) := stx
+    | throwUnsupportedSyntax
+  let package := pkg.getString
+  let env ← getEnv
+  let moduleNames := env.allImportedModuleNames
+  let mut entries : Array Term := #[]
+  -- One root's name may extend another's, putting a module below both; each module's tests are
+  -- gathered once.
+  let mut seen : NameSet := {}
+  for modStx in mods do
+    let rootName := modStx.getId
+    unless (env.getModuleIdx? rootName).isSome do
+      throwErrorAt modStx "Module `{rootName}` is not imported, so its tests cannot be \
+          reached. Import it, using `import all {rootName}` if it belongs to the module system."
+    for h : idx in [0 : moduleNames.size] do
+      let moduleName := moduleNames[idx]
+      unless rootName.isPrefixOf moduleName do continue
+      if seen.contains moduleName then continue
+      seen := seen.insert moduleName
+      let moduleStr := moduleName.toString
+      for test in testExt.getModuleEntries env idx do
+        -- The internal name is used here, because the user-facing name can be ambiguous for private
+        -- tests
+        let userName := privateToUserName test.name
+        let testName := testNameBelow moduleName userName
+        let range ← findDeclarationRanges? test.name
+        let pos := (range.map (·.range.pos)).getD ⟨0, 0⟩
+        let endPos := (range.map (·.range.endPos)).getD ⟨0, 0⟩
+        -- The docstring captured when the attribute was applied, so the report and widget can show it.
+        let docStx ← match test.docstring? with
+          | some doc => `(some $(quote doc))
+          | none => `((none : Option String))
+        entries := entries.push <| ←
+          `(Errata.TestEntry.of $(quote package) $(quote moduleStr) $(quote testName)
+              (Errata.Location.mk $(quote test.file)
+                (Lean.Position.mk $(quote pos.line) $(quote pos.column))
+                (Lean.Position.mk $(quote endPos.line) $(quote endPos.column)))
+              (@$(mkCIdent test.name)) (docstring? := $docStx))
+  elabTerm (← `(#[$entries,*])) expectedType?
diff --git a/src/errata/Errata/Golden.lean b/src/errata/Errata/Golden.lean
new file mode 100644
index 00000000..69e86cb9
--- /dev/null
+++ b/src/errata/Errata/Golden.lean
@@ -0,0 +1,106 @@
+/-
+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.TestM
+import Lean.Util.Diff
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/--
+A line-by-line diff of expected against actual output. Lines marked {lit}`-` are in the expected
+output only, and lines marked {lit}`+` are in the actual output only.
+-/
+private def goldenDiff (expected actual : String) : String :=
+  let diff := Lean.Diff.diff (expected.splitOn "\n").toArray (actual.splitOn "\n").toArray
+  "- expected, + actual:\n" ++ Lean.Diff.linesToString diff
+
+/-- Compares a produced string against a golden file, or rewrites it under `--update-golden`. -/
+def goldenFile (expected : System.FilePath) (actual : String)
+    (loc : Location := by exact here%) : TestM Unit := do
+  let ctx ← read
+  if ctx.updateGolden then
+    writeFile expected actual
+  else if ← expected.pathExists then
+    let want ← IO.FS.readFile expected
+    unless want == actual do
+      failAt loc s!"golden mismatch for {expected}" (detail? := some (goldenDiff want actual))
+  else
+    failAt loc s!"missing golden file {expected}"
+      (detail? := some "Run with --update-golden to create it.")
+
+/-- All files below a directory, recursively, in a deterministic order. -/
+def filesUnder (dir : System.FilePath) : IO (Array System.FilePath) := do
+  let mut out : Array System.FilePath := #[]
+  for entry in ← dir.walkDir do
+    unless ← entry.isDir do out := out.push entry
+  return out.qsort (·.toString < ·.toString)
+
+/-- The path of a file relative to a base directory. -/
+private def relativeTo (base file : System.FilePath) : String :=
+  (file.toString.drop (base.toString.length + 1)).copy
+
+/-- The offset of the first byte at which two contents differ, within the length they share. -/
+private def firstDifference (a b : ByteArray) : Option Nat := Id.run do
+  for i in [0 : min a.size b.size] do
+    if a[i]! != b[i]! then return some i
+  return none
+
+/-- Describes how two contents differ, for content that is not text. -/
+private def binaryDifference (want got : ByteArray) : String :=
+  let place :=
+    match firstDifference want got with
+    | some i => s!"binary content differs at byte {i}"
+    | none => "binary content differs in length"
+  if want.size == got.size then place
+  else s!"{place}: expected {want.size} bytes, produced {got.size} bytes"
+
+/-- Compares a produced directory tree against a golden tree, or rewrites it under `--update-golden`. -/
+def goldenDir (expected actual : System.FilePath)
+    (loc : Location := by exact here%) : TestM Unit := do
+  let ctx ← read
+  unless ← actual.isDir do
+    failAt loc s!"missing produced directory {actual}"
+      (detail? := some "The code under test did not create it as a directory.")
+  let actualFiles ← filesUnder actual
+  if ctx.updateGolden then
+    -- The recorded tree is replaced wholesale, so a path that changed shape between file and
+    -- directory updates as cleanly as changed content. The golden tree is recorded even when the
+    -- produced tree holds no files, so that a later run compares against it rather than reporting
+    -- it as missing.
+    if ← expected.isDir then IO.FS.removeDirAll expected
+    else if ← expected.pathExists then IO.FS.removeFile expected
+    IO.FS.createDirAll expected
+    for file in actualFiles do
+      writeBinFile (expected / relativeTo actual file) (← IO.FS.readBinFile file)
+    return
+  unless ← expected.pathExists do
+    failAt loc s!"missing golden directory {expected}"
+      (detail? := some "Run with --update-golden to create it.")
+  -- Membership is decided against the walked file lists rather than by a filesystem probe, so a
+  -- directory standing where a file belongs counts as that file being absent.
+  let expectedRels := (← filesUnder expected).map (relativeTo expected)
+  let actualRels := actualFiles.map (relativeTo actual)
+  for rel in actualRels do
+    unless expectedRels.contains rel do
+      failAt loc s!"file not present in the golden directory: {rel}"
+    let wantContent ← IO.FS.readBinFile (expected / rel)
+    let gotContent ← IO.FS.readBinFile (actual / rel)
+    unless wantContent == gotContent do
+      -- A diff is only meaningful for text; other content is described by size.
+      let detail :=
+        match String.fromUTF8? wantContent, String.fromUTF8? gotContent with
+        | some wantText, some gotText => goldenDiff wantText gotText
+        | _, _ => binaryDifference wantContent gotContent
+      failAt loc s!"golden mismatch for {rel}" (detail? := some detail)
+  for rel in expectedRels do
+    unless actualRels.contains rel do
+      failAt loc s!"file missing from the produced output: {rel}"
diff --git a/src/errata/Errata/Here.lean b/src/errata/Errata/Here.lean
new file mode 100644
index 00000000..ae1ba60c
--- /dev/null
+++ b/src/errata/Errata/Here.lean
@@ -0,0 +1,32 @@
+/-
+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.Result
+public meta import Lean
+
+open Lean Elab Term
+
+public section
+
+set_option doc.verso true
+
+/--
+`here%` elaborates to the {name}`Errata.Location` of its own occurrence. Used as a default argument
+(`by exact here%`), it is elaborated at each call site, so it captures the caller's position.
+-/
+syntax (name := hereStx) "here%" : term
+
+@[term_elab hereStx]
+meta def elabHere : TermElab := fun _stx _expectedType? => do
+  let ref ← getRef
+  let fileMap ← getFileMap
+  let startPos := fileMap.toPosition (ref.getPos?.getD 0)
+  let endPos := fileMap.toPosition (ref.getTailPos?.getD (ref.getPos?.getD 0))
+  let file ← getFileName
+  elabTerm (← `(Errata.Location.mk $(quote file)
+      (Lean.Position.mk $(quote startPos.line) $(quote startPos.column))
+      (Lean.Position.mk $(quote endPos.line) $(quote endPos.column)))) none
diff --git a/src/errata/Errata/IsTest.lean b/src/errata/Errata/IsTest.lean
new file mode 100644
index 00000000..1f4d1728
--- /dev/null
+++ b/src/errata/Errata/IsTest.lean
@@ -0,0 +1,42 @@
+/-
+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.TestM
+public import Errata.Result
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- Runs a returned verdict as a test action. -/
+def TestResult.toTest : TestResult → TestM Unit
+  | .pass => pure ()
+  | .fail f => throw f
+  | .skip reason => Errata.skip reason
+
+/-- Types that can serve as the body of a test. -/
+class IsTest (α : Type) where
+  /-- Runs the value as a test action. -/
+  toTest : α → TestM Unit
+
+instance : IsTest (TestM Unit) where
+  toTest act := act
+
+instance : IsTest TestResult where
+  toTest := TestResult.toTest
+
+instance : IsTest (IO TestResult) where
+  toTest act := do (← act).toTest
+
+instance : IsTest Bool where
+  toTest b := unless b do failHere "expected true, got false"
+
+instance : IsTest (IO Bool) where
+  toTest act := do unless (← act) do failHere "expected true, got false"
diff --git a/src/errata/Errata/Process.lean b/src/errata/Errata/Process.lean
new file mode 100644
index 00000000..4209e322
--- /dev/null
+++ b/src/errata/Errata/Process.lean
@@ -0,0 +1,23 @@
+/-
+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.TestM
+public import Errata.Here
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- Asserts that a process exited with the expected code, showing its output otherwise. -/
+def assertExitCode (expected : UInt32) (output : IO.Process.Output)
+    (loc : Location := by exact here%) : TestM Unit :=
+  unless output.exitCode == expected do
+    failAt loc s!"process exited with code {output.exitCode}, expected {expected}"
+      (detail? := some s!"stdout:\n{output.stdout}\nstderr:\n{output.stderr}")
diff --git a/src/errata/Errata/Property.lean b/src/errata/Errata/Property.lean
new file mode 100644
index 00000000..12aa48d6
--- /dev/null
+++ b/src/errata/Errata/Property.lean
@@ -0,0 +1,35 @@
+/-
+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.TestM
+public import Plausible
+public import Plausible.ArbitraryFueled
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+open Plausible
+
+open scoped Plausible.Decorations in
+/-- Checks a property with Plausible, failing with the counterexample if it is falsified. -/
+def property (p : Prop) (cfg : Configuration := {}) (loc : Location := by exact here%)
+    (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : TestM Unit := do
+  let ctx ← read
+  let cfg := { cfg with
+    quiet := true,
+    randomSeed := ctx.seed.orElse (fun _ => cfg.randomSeed)
+  }
+  match ← Testable.checkIO p' (cfg := cfg) with
+  | .success _ => pure ()
+  | .gaveUp n => failAt loc s!"property gave up after discarding {n} cases"
+  | .failure _ counterExample _ =>
+    failAt loc "property falsified" (detail? := some ("\n".intercalate counterExample))
diff --git a/src/errata/Errata/Report.lean b/src/errata/Errata/Report.lean
new file mode 100644
index 00000000..e53db16a
--- /dev/null
+++ b/src/errata/Errata/Report.lean
@@ -0,0 +1,321 @@
+/-
+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.Result
+public import Lean.Data.Json
+
+public section
+
+open Lean (Json ToJson FromJson)
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+private def indentLines (text : String) : String :=
+  "\n".intercalate ((text.splitOn "\n").map (fun l => "    " ++ l))
+
+/-- A source location rendered as the clickable `file:line:col` of the span's start. -/
+private def locationText (l : Location) : String :=
+  s!"{l.file}:{l.startPos.line}:{l.startPos.column}"
+
+/--
+Prints one result: its status line, its docstring when shown, and for a failure its detail and
+captured output. A failure or error always shows its docstring; a pass or skip shows it only at a
+verbosity that shows all docstrings.
+-/
+private def printResult (verbosity : Verbosity) (r : Result) : IO Unit := do
+  let name := s!"{r.moduleTarget}  {r.testName}"
+  let printDoc : IO Unit := do
+    if verbosity.showsAllDocstrings || !r.status.isSuccess then
+      if let some d := r.description? then IO.println (indentLines d)
+  match r.status with
+  | .pass => IO.println s!"ok    {name} ({r.durationMs}ms)"; printDoc
+  | .skip reason => IO.println s!"skip  {name}: {reason}"; printDoc
+  | .fail f =>
+    IO.println s!"FAIL  {name}: {f.message}"
+    printDoc
+    if let some l := f.location? then IO.println (indentLines (locationText l))
+    if let some d := f.detail? then IO.println (indentLines d)
+    unless r.output.isEmpty do IO.println (indentLines s!"output:\n{r.output.all}")
+  | .error m =>
+    IO.println s!"ERROR {name}: {m}"
+    printDoc
+    unless r.output.isEmpty do IO.println (indentLines s!"output:\n{r.output.all}")
+
+/--
+A running tally of results suppressed by truncation. Only passes and skips are ever suppressed;
+failures and errors always print.
+-/
+private structure Suppressed where
+  passed : Nat := 0
+  skipped : Nat := 0
+
+/-- Counts one more suppressed result. -/
+private def Suppressed.add (s : Suppressed) : Status → Suppressed
+  | .skip _ => { s with skipped := s.skipped + 1 }
+  | _ => { s with passed := s.passed + 1 }
+
+/-- The number of suppressed results. -/
+private def Suppressed.total (s : Suppressed) : Nat :=
+  s.passed + s.skipped
+
+/-- Prints the truncation summary for a test whose results were capped, if any were suppressed. -/
+private def printSuppressed (s : Suppressed) : IO Unit := do
+  if s.total > 0 then
+    let parts := (if s.passed > 0 then #[s!"{s.passed} more passed"] else #[])
+      ++ (if s.skipped > 0 then #[s!"{s.skipped} more skipped"] else #[])
+    IO.println s!"    (... and {", ".intercalate parts.toList})"
+
+/--
+Prints a human-readable report and returns the number of failures. Failures and errors are printed at
+every verbosity. {name}`Verbosity.quiet` adds passes and skips, truncating each test's after a cap and
+summarizing the remainder; {name}`Verbosity.verbose` shows them all; and
+{name}`Verbosity.superVerbose` also shows every test's docstring.
+-/
+def humanReport (verbosity : Verbosity) (results : Array Result) : IO Nat := do
+  let cap := 50
+  let mut passed := 0
+  let mut failed := 0
+  let mut errors := 0
+  let mut skipped := 0
+  let mut curKey : Option (String × String) := none
+  let mut shown := 0
+  let mut more : Suppressed := {}
+  for r in results do
+    match r.status with
+    | .pass => passed := passed + 1
+    | .fail _ => failed := failed + 1
+    | .error _ => errors := errors + 1
+    | .skip _ => skipped := skipped + 1
+    -- Results of one test are contiguous; truncation is per test (its data-driven sub-results).
+    let key := (r.moduleTarget, r.test)
+    if curKey != some key then
+      printSuppressed more
+      curKey := some key
+      shown := 0
+      more := {}
+    match r.status with
+    | .fail _ | .error _ =>
+      printResult verbosity r
+      shown := shown + 1
+    | .pass | .skip _ =>
+      if verbosity.showsPasses then
+        if verbosity.truncates && shown ≥ cap then
+          more := more.add r.status
+        else
+          printResult verbosity r
+          shown := shown + 1
+  printSuppressed more
+  IO.println s!"{passed} passed, {failed} failed, {errors} errors, {skipped} skipped"
+  return failed + errors
+
+/--
+Drops the characters XML 1.0 forbids even when escaped: those below {lit}`U+0020` other than tab,
+newline, and carriage return, and the noncharacters {lit}`U+FFFE` and {lit}`U+FFFF`.
+-/
+private def dropXmlForbidden (s : String) : String :=
+  s.foldl (init := "") fun acc c =>
+    if c == '\uFFFE' || c == '\uFFFF' then acc
+    else if c == '\t' || c == '\n' || c == '\r' || Nat.ble 0x20 c.toNat then acc.push c
+    else acc
+
+/--
+Escapes text for XML and drops characters XML 1.0 forbids even when escaped, so a captured ANSI escape
+or NUL byte in a message or output fragment cannot make the report malformed.
+-/
+private def xmlEscape (s : String) : String :=
+  dropXmlForbidden <|
+    s.replace "&" "&amp;" |>.replace "<" "&lt;" |>.replace ">" "&gt;" |>.replace "\"" "&quot;"
+
+instance : ToJson Location where
+  toJson l := json%{
+    "file": $l.file,
+    "startLine": $l.startPos.line,
+    "startColumn": $l.startPos.column,
+    "endLine": $l.endPos.line,
+    "endColumn": $l.endPos.column
+  }
+
+instance : FromJson Location where
+  fromJson? j := do
+    return {
+      file := ← j.getObjValAs? String "file",
+      startPos := ⟨← j.getObjValAs? Nat "startLine", ← j.getObjValAs? Nat "startColumn"⟩,
+      endPos := ⟨← j.getObjValAs? Nat "endLine", ← j.getObjValAs? Nat "endColumn"⟩
+    }
+
+instance : ToJson Output where
+  toJson
+    | .stdout s => json%{ "stream": "stdout", "text": $s }
+    | .stderr s => json%{ "stream": "stderr", "text": $s }
+
+instance : FromJson Output where
+  fromJson? j := do
+    let text ← j.getObjValAs? String "text"
+    match ← j.getObjValAs? String "stream" with
+    | "stdout" => return .stdout text
+    | "stderr" => return .stderr text
+    | other => .error s!"unknown output stream: {other}"
+
+instance : ToJson OutputLog where
+  toJson o := ToJson.toJson o.log
+
+instance : FromJson OutputLog where
+  fromJson? j := return { log := ← FromJson.fromJson? j }
+
+/-- The suite a result belongs to: its package-qualified module. -/
+private def suiteOf (r : Result) : String :=
+  r.moduleTarget
+
+/-- The case name of a result: the test name below the module. -/
+private def caseOf (r : Result) : String :=
+  r.testName
+
+private def countWhere (results : Array Result) (p : Status → Bool) : Nat :=
+  results.countP (p ·.status)
+
+/-- Groups results by their package-qualified module in a single pass, keeping first-seen order. -/
+private def byModule (results : Array Result) : Array (String × Array Result) := Id.run do
+  let mut order : Array String := #[]
+  let mut groups : Std.HashMap String (Array Result) := {}
+  for r in results do
+    let s := suiteOf r
+    if !groups.contains s then order := order.push s
+    groups := groups.alter s fun cur => some ((cur.getD #[]).push r)
+  return order.map fun s => (s, groups.getD s #[])
+
+/-- Renders the results as JUnit XML, grouping by the module path. -/
+def junitReport (results : Array Result) : String := Id.run do
+  let mut out := "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n<testsuites>\n"
+  -- Every case in a group shares a package and a module, since the group is keyed by both.
+  for (_, cases) in byModule results do
+    let pkg := (cases[0]?.map (·.package)).getD ""
+    let suite := (cases[0]?.map (·.moduleName)).getD ""
+    let failures := countWhere cases (fun s => s matches .fail _)
+    let errors := countWhere cases (fun s => s matches .error _)
+    let skipped := countWhere cases (fun s => s matches .skip _)
+    out := out ++ s!"  <testsuite name=\"{xmlEscape suite}\" package=\"{xmlEscape pkg}\" \
+      tests=\"{cases.size}\" failures=\"{failures}\" errors=\"{errors}\" skipped=\"{skipped}\">\n"
+    for r in cases do
+      let time := toString (Float.ofNat r.durationMs / 1000.0)
+      let opening := s!"    <testcase name=\"{xmlEscape (caseOf r)}\" \
+        classname=\"{xmlEscape suite}\" time=\"{time}\">"
+      match r.status with
+      | .pass =>
+        out := out ++ opening ++ "</testcase>\n"
+      | .fail f =>
+        let loc := match f.location? with | some l => locationText l ++ ": " | none => ""
+        out := out ++ opening ++ s!"\n      <failure message=\"{xmlEscape (loc ++ f.message)}\">\
+          {xmlEscape (f.detail?.getD "")}</failure>\n    </testcase>\n"
+      | .error m =>
+        out := out ++ opening ++ s!"\n      <error message=\"{xmlEscape m}\"></error>\n    </testcase>\n"
+      | .skip reason =>
+        out := out ++ opening ++ s!"\n      <skipped message=\"{xmlEscape reason}\"></skipped>\n    </testcase>\n"
+    out := out ++ "  </testsuite>\n"
+  out := out ++ "</testsuites>\n"
+  return out
+
+private def statusFields : Status → List (String × Json)
+  | .pass => [("status", Json.str "pass")]
+  | .fail f =>
+    [("status", Json.str "fail"), ("message", Json.str f.message)] ++
+      (match f.detail? with | some d => [("detail", Json.str d)] | none => []) ++
+      (match f.location? with | some l => [("location", ToJson.toJson l)] | none => [])
+  | .error m => [("status", Json.str "error"), ("message", Json.str m)]
+  | .skip reason => [("status", Json.str "skip"), ("reason", Json.str reason)]
+
+instance : ToJson Result where
+  toJson r := private
+    Json.mkObj <|
+      [("package", Json.str r.package), ("module", Json.str r.moduleName),
+        ("test", Json.str r.test), ("resultPath", ToJson.toJson r.resultPath),
+        ("durationMs", ToJson.toJson r.durationMs)] ++
+      statusFields r.status ++
+      (if r.output.isEmpty then [] else [("output", ToJson.toJson r.output)]) ++
+      (match r.description? with | some d => [("description", Json.str d)] | none => [])
+
+/-- Decodes an optional field: absent maps to {lean}`none`. -/
+private def optField [FromJson α] (j : Json) (key : String) : Except String (Option α) :=
+  match j.getObjVal? key with
+  | .ok v => some <$> FromJson.fromJson? v
+  | .error _ => pure none
+
+instance : FromJson Status where
+  fromJson? j := private do
+    match ← j.getObjValAs? String "status" with
+    | "pass" => return .pass
+    | "error" => return .error (← j.getObjValAs? String "message")
+    | "skip" => return .skip (← j.getObjValAs? String "reason")
+    | "fail" => return .fail {
+        message := ← j.getObjValAs? String "message",
+        detail? := ← optField j "detail",
+        location? := ← optField j "location"
+      }
+    | other => .error s!"unknown status: {other}"
+
+instance : FromJson Result where
+  fromJson? j := private do
+    return {
+      package := ← j.getObjValAs? String "package",
+      moduleName := ← j.getObjValAs? String "module",
+      test := ← j.getObjValAs? String "test",
+      resultPath := ← j.getObjValAs? (Array String) "resultPath",
+      durationMs := ← j.getObjValAs? Nat "durationMs",
+      status := ← FromJson.fromJson? j,
+      output := (← optField j "output").getD {},
+      description? := ← optField j "description"
+    }
+
+/-- Renders the results as a JSON array of objects. -/
+def jsonReport (results : Array Result) : String := (ToJson.toJson results).pretty
+
+/-- The length of the longest run of consecutive backticks in {name}`s`. -/
+private def longestBacktickRun (s : String) : Nat :=
+  (s.foldl (init := (0, 0)) fun (cur, best) c =>
+    if c == '`' then (cur + 1, Nat.max best (cur + 1)) else (0, best)).2
+
+/-- Wraps {name}`body` in a fenced code block whose fence outlasts any backtick run inside it. -/
+private def fencedBlock (body : String) : String :=
+  let fence := String.ofList (List.replicate (Nat.max 3 (longestBacktickRun body + 1)) '`')
+  s!"{fence}\n{body}\n{fence}"
+
+/--
+Renders the results as Markdown for a CI job summary: a headline tally, each failure and error in an
+open collapsible block with its location and detail, and a per-module table in a closed one.
+-/
+def markdownReport (results : Array Result) : String := Id.run do
+  let passed := countWhere results (· matches .pass)
+  let failed := countWhere results (· matches .fail _)
+  let errors := countWhere results (· matches .error _)
+  let skipped := countWhere results (· matches .skip _)
+  let icon := if failed + errors == 0 then "✅" else "❌"
+  let mut out := s!"## {icon} Errata test results\n\n"
+  out := out ++
+    s!"**{passed}** passed · **{failed}** failed · **{errors}** errors · **{skipped}** skipped\n\n"
+  for r in results do
+    let render (mark message : String) (detail? : Option String) : String := Id.run do
+      let mut s := s!"<details open><summary>{mark} <code>{xmlEscape r.moduleTarget}</code> \
+        {xmlEscape r.testName}: {xmlEscape message}</summary>\n\n"
+      if let some d := r.description? then s := s ++ s!"{d}\n\n"
+      if let .fail f := r.status then
+        if let some l := f.location? then s := s ++ s!"`{locationText l}`\n\n"
+      if let some d := detail? then s := s ++ s!"{fencedBlock d}\n\n"
+      unless r.output.isEmpty do
+        s := s ++ s!"<details><summary>output</summary>\n\n{fencedBlock r.output.all}\n\n</details>\n\n"
+      return s ++ "</details>\n\n"
+    match r.status with
+    | .fail f => out := out ++ render "❌" f.message f.detail?
+    | .error m => out := out ++ render "💥" m none
+    | _ => pure ()
+  out := out ++ "<details><summary>Summary by module</summary>\n\n"
+  out := out ++ "| Module | ✅ | ❌ | 💥 | ⏭️ |\n| :-- | --: | --: | --: | --: |\n"
+  for (m, cs) in byModule results do
+    out := out ++ s!"| {m} | {countWhere cs (· matches .pass)} | {countWhere cs (· matches .fail _)} \
+      | {countWhere cs (· matches .error _)} | {countWhere cs (· matches .skip _)} |\n"
+  return out ++ "\n</details>\n"
diff --git a/src/errata/Errata/Result.lean b/src/errata/Errata/Result.lean
new file mode 100644
index 00000000..dee7e100
--- /dev/null
+++ b/src/errata/Errata/Result.lean
@@ -0,0 +1,176 @@
+/-
+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.Position
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- How much the human-readable report prints. -/
+inductive Verbosity where
+  /-- Print only failures and errors. -/
+  | silent
+  /-- Also print passes and skips, truncating each test's results after a cap. -/
+  | quiet
+  /-- Print every result. -/
+  | verbose
+  /-- Print every result, and each test's docstring alongside it, not only those that fail. -/
+  | superVerbose
+deriving Repr, Inhabited, DecidableEq, BEq
+
+/-- Whether passes and skips are printed at this verbosity. -/
+def Verbosity.showsPasses : Verbosity → Bool
+  | .silent => false
+  | .quiet | .verbose | .superVerbose => true
+
+/-- Whether each test's results are truncated after a cap at this verbosity. -/
+def Verbosity.truncates : Verbosity → Bool
+  | .quiet => true
+  | .silent | .verbose | .superVerbose => false
+
+/-- Whether every result's docstring is shown, not only those of failures and errors. -/
+def Verbosity.showsAllDocstrings : Verbosity → Bool
+  | .superVerbose => true
+  | .silent | .quiet | .verbose => false
+
+/--
+A source span, used in failure messages and editor integration.
+-/
+structure Location where
+  /-- The source file that contains the span. -/
+  file : String
+  /-- The start of the span. -/
+  startPos : Lean.Position
+  /-- The end of the span. -/
+  endPos : Lean.Position
+deriving Repr, Inhabited, BEq, DecidableEq
+
+/-- A test failure, carrying the information needed to explain it. -/
+structure TestFailure where
+  /-- A short description of what went wrong. -/
+  message : String
+  /-- Supporting detail, such as a diff, a counterexample, or expected and actual values. -/
+  detail? : Option String := none
+  /-- The source location of the failed check, when known. -/
+  location? : Option Location := none
+deriving Repr, Inhabited, DecidableEq
+
+/-- The verdict that a test body may return. -/
+inductive TestResult where
+  /-- The test passed. -/
+  | pass
+  /-- The test failed, with details. -/
+  | fail (failure : TestFailure)
+  /-- The test was skipped, with a reason. -/
+  | skip (reason : String)
+deriving Repr, Inhabited
+
+/-- The recorded outcome of a test or a named result. -/
+inductive Status where
+  /-- The check passed. -/
+  | pass
+  /-- The check failed. -/
+  | fail (failure : TestFailure)
+  /-- An error escaped the check, so it could not produce a verdict. -/
+  | error (message : String)
+  /-- The check was skipped. -/
+  | skip (reason : String)
+deriving Repr, Inhabited, DecidableEq
+
+/-- Whether a status counts as success for the exit code. -/
+def Status.isSuccess : Status → Bool
+  | .pass | .skip _ => true
+  | .fail _ | .error _ => false
+
+/-- A fragment of captured output, tagged by the stream it was written to. -/
+inductive Output where
+  /-- Text written to standard output. -/
+  | stdout (text : String)
+  /-- Text written to standard error. -/
+  | stderr (text : String)
+deriving Repr, Inhabited, DecidableEq
+
+/-- The text of an output fragment, regardless of stream. -/
+def Output.text : Output → String
+  | .stdout s | .stderr s => s
+
+/-- All captured output, concatenated in order. -/
+def capturedText (output : Array Output) : String :=
+  output.foldl (fun acc o => acc ++ o.text) ""
+
+/-- Output captured from an action, in order and tagged by stream. -/
+structure OutputLog where
+  /-- The captured fragments, in order, tagged by stream. -/
+  log : Array Output := #[]
+deriving Repr, Inhabited, DecidableEq
+
+namespace OutputLog
+
+/-- Whether no output was captured. -/
+def isEmpty (o : OutputLog) : Bool := o.log.isEmpty
+
+/-- The text written to stdout, concatenated in order. -/
+def stdout (o : OutputLog) : String :=
+  o.log.foldl (fun acc out => match out with | .stdout s => acc ++ s | .stderr _ => acc) ""
+
+/-- The text written to stderr, concatenated in order. -/
+def stderr (o : OutputLog) : String :=
+  o.log.foldl (fun acc out => match out with | .stderr s => acc ++ s | .stdout _ => acc) ""
+
+/-- The text written to stdout and stderr, concatenated in order. -/
+def all (o : OutputLog) : String := capturedText o.log
+
+end OutputLog
+
+/-- One entry collected during a run and rendered by the reporters. -/
+structure Result where
+  /-- The package that defines the test. -/
+  package : String
+  /-- The module that defines the test, as a dotted name. -/
+  moduleName : String
+  /-- The test declaration's name below its module, as a dotted name. -/
+  test : String
+  /-- The named result below the test; empty for the test's own result. -/
+  resultPath : Array String := #[]
+  /-- The recorded outcome. -/
+  status : Status
+  /-- How long the check took, in milliseconds. -/
+  durationMs : Nat := 0
+  /-- What the test wrote to stdout and stderr. -/
+  output : OutputLog := {}
+  /-- The test's docstring, rendered as Markdown, when it has one. -/
+  description? : Option String := none
+deriving Repr, Inhabited, DecidableEq
+
+/-- The test name below the module: the declaration and any named result, dotted. -/
+def Result.testName (result : Result) : String :=
+  if result.resultPath.isEmpty then result.test
+  else result.test ++ "." ++ ".".intercalate result.resultPath.toList
+
+/--
+The package-qualified module that defines the test ({lit}`package/module`). Reports use it to label
+each result and to group the results of one module together.
+-/
+def Result.moduleTarget (result : Result) : String :=
+  result.package ++ "/" ++ result.moduleName
+
+/-- A failed verdict from a compile-time message mismatch, carrying its source span. -/
+def TestResult.mismatch (message detail file : String)
+    (startLine startCol endLine endCol : Nat) : TestResult :=
+  .fail {
+    message,
+    detail? := some detail,
+    location? := some {
+      file,
+      startPos := { line := startLine, column := startCol },
+      endPos := { line := endLine, column := endCol }
+    }
+  }
diff --git a/src/errata/Errata/Runner.lean b/src/errata/Errata/Runner.lean
new file mode 100644
index 00000000..4bce4087
--- /dev/null
+++ b/src/errata/Errata/Runner.lean
@@ -0,0 +1,219 @@
+/-
+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.TestM
+public import Errata.IsTest
+public import Errata.Report
+public import Cli
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/-- A test to run: its identity and the action that produces its results. -/
+structure TestEntry where
+  /-- The package that defines the test. -/
+  package : String
+  /-- The module that defines the test, as a dotted name. -/
+  moduleName : String
+  /-- The test declaration's name below its module. -/
+  test : String
+  /-- The test's own source range, used as the default failure location. -/
+  location : Location
+  /-- The test's docstring, rendered as Markdown, when it has one. -/
+  docstring? : Option String := none
+  /-- The action to run. -/
+  run : TestM Unit
+
+/-- Builds a test entry from any testable value. -/
+def TestEntry.of {α} [IsTest α] (package moduleName test : String) (location : Location)
+    (value : α) (docstring? : Option String := none) : TestEntry where
+  package := package
+  moduleName := moduleName
+  test := test
+  location := location
+  docstring? := docstring?
+  run := IsTest.toTest value
+
+/-- Runs a single test entry, collecting all of its results. -/
+def runEntry (cfg : Context) (entry : TestEntry) : IO (Array Result) := do
+  let log ← IO.mkRef (#[] : Array Result)
+  let ctx := { cfg with
+    package := entry.package, moduleName := entry.moduleName, test := entry.test,
+    resultPath := #[], location := entry.location, log, description? := entry.docstring?
+  }
+  let start ← IO.monoMsNow
+  let (outcome, output) ← runCapturing ctx entry.run
+  let stop ← IO.monoMsNow
+  let dur := stop - start
+  let logged ← log.get
+  return match ctx.resultOfOutcome outcome output dur (!logged.isEmpty) with
+    | some r => logged.push r
+    | none => logged
+
+/-- Runs all the test entries and collects their results. -/
+def run (cfg : Context) (entries : Array TestEntry) : IO (Array Result) := do
+  let mut all : Array Result := #[]
+  for entry in entries do
+    all := all ++ (← runEntry cfg entry)
+  return all
+
+/-- A base context with the given settings and a fresh, empty log. -/
+def mkContext (updateGolden : Bool := false)
+    (options : OptionMap := {}) (seed : Option Nat := none) : IO Context := do
+  let log ← IO.mkRef (#[] : Array Result)
+  let usedOptions ← IO.mkRef ({} : Std.HashSet String)
+  let outputFailed ← IO.mkRef false
+  return { updateGolden, options, seed, log, usedOptions, outputFailed }
+
+/-- The settings parsed from the runner's command line. -/
+structure Options where
+  /-- The reporting verbosity. -/
+  verbosity : Verbosity := .silent
+  /-- Rewrites golden expected files instead of comparing. -/
+  updateGolden : Bool := false
+  /-- The seed for property tests, for reproducing a failure. -/
+  seed : Option Nat := none
+  /-- Writes a JUnit XML report to this path. -/
+  junitPath : Option String := none
+  /-- Writes a JSON report to this path. -/
+  jsonPath : Option String := none
+  /-- Writes a Markdown report to this path. -/
+  markdownPath : Option String := none
+  /-- Fails the run if warnings are logged, as Lake's `--wfail` does for builds. -/
+  wfail : Bool := false
+  /-- Project-specific options, as a multi-map so repeated options accumulate. -/
+  options : OptionMap := {}
+
+open Cli in
+/-- The runner's command-line interface. The handler receives the parsed arguments. -/
+def runnerCmd (handler : Cli.Parsed → IO UInt32) : Cli.Cmd :=
+  `[Cli|
+    "errata-runner" VIA handler;
+    "Runs the discovered Errata tests."
+
+    FLAGS:
+      v, verbose;              "Also report passes and skips, truncating each test's results."
+      vv, "verbose-all";       "Report every result, without truncation."
+      vvv, "verbose-docs";     "Report every result and every test's docstring."
+      "update-golden";         "Rewrite golden expected files instead of comparing."
+      seed : Nat;              "Seed property tests, to reproduce a failure."
+      junit : String;          "Write a JUnit XML report to the given path."
+      json : String;           "Write a JSON report to the given path."
+      markdown : String;       "Write a Markdown report (for a CI job summary) to the given path."
+      wfail;                   "Fail the run if warnings are logged."
+
+    ARGS:
+      ...testOption : String;  "Options for the tests themselves; see below."
+
+    EXTENSIONS:
+      longDescription "Options for the tests themselves go after a `--` separator, as \
+        `--name value` or `--name=value`. Write a value that begins with `-` as `--name=value`."
+  ]
+
+/--
+Parses the options passed through to the tests: {lit}`--name value` and {lit}`--name=value` pairs,
+collected into a multi-map so repeated options accumulate. The {lit}`--name value` form takes the
+next token as the value when that token does not begin with {lit}`-`; a value that does uses the
+{lit}`--name=value` form. Any other token is rejected.
+-/
+partial def projectOptions (tokens : List String) : Except String OptionMap :=
+  go {} tokens
+where
+  push (acc : OptionMap) (name value : String) : OptionMap :=
+    acc.insert name ((acc.getD name #[]).push value)
+  go (acc : OptionMap) : List String → Except String OptionMap
+    | [] => .ok acc
+    | tok :: rest =>
+      match tok.dropPrefix? "--" with
+      | none =>
+        .error s!"unexpected argument '{tok}': test options are `--name value` or `--name=value`"
+      | some name =>
+        match name.copy.splitOn "=" with
+        | [] => unreachable! -- `splitOn` always returns at least one element
+        | [n] =>
+          if n.isEmpty then .error s!"unexpected argument: {tok}"
+          else match rest with
+            | value :: rest' =>
+              if value.startsWith "-" then go (push acc n "") rest
+              else go (push acc n value) rest'
+            | [] => .ok (push acc n "")
+        | n :: valueParts =>
+          if n.isEmpty then .error s!"unexpected argument: {tok}"
+          else go (push acc n ("=".intercalate valueParts)) rest
+
+/-- The value of a path-valued flag, when it is present; a present but empty path is an error. -/
+private def pathFlag (p : Cli.Parsed) (name : String) : Except String (Option String) :=
+  match p.flag? name with
+  | none => .ok none
+  | some f => if f.value.isEmpty then .error s!"--{name} expects a path" else .ok (some f.value)
+
+/-- Interprets a parsed command line as runner settings. -/
+def optionsOfParsed (p : Cli.Parsed) : Except String Options := do
+  let verbosity : Verbosity :=
+    if p.hasFlag "verbose-docs" then .superVerbose
+    else if p.hasFlag "verbose-all" then .verbose
+    else if p.hasFlag "verbose" then .quiet
+    else .silent
+  return {
+    verbosity,
+    updateGolden := p.hasFlag "update-golden",
+    seed := p.flag? "seed" |>.map (·.as! Nat),
+    junitPath := ← pathFlag p "junit",
+    jsonPath := ← pathFlag p "json",
+    markdownPath := ← pathFlag p "markdown",
+    wfail := p.hasFlag "wfail",
+    options := ← projectOptions (p.variableArgsAs! String).toList
+  }
+
+/--
+Parses the runner's command line into settings: the declared flags, then any options for the tests
+themselves after a {lit}`--` separator.
+-/
+def parseOptions (args : List String) : Except String Options :=
+  match (runnerCmd fun _ => pure 0).parse args with
+  | .error e => .error e.kind.msg
+  | .ok (_, parsed) => optionsOfParsed parsed
+
+/-- The entry point the generated runner calls: parse arguments, run the tests, and report. -/
+def runMain (entries : Array TestEntry) (args : List String) : IO UInt32 := do
+  let cmd := runnerCmd fun parsed => do
+    let opts ←
+      match optionsOfParsed parsed with
+      | .ok opts => pure opts
+      | .error msg =>
+        IO.eprintln s!"error: {msg}"
+        return 1
+    let cfg ← mkContext (updateGolden := opts.updateGolden)
+      (options := opts.options) (seed := opts.seed)
+    let results ← run cfg entries
+    let writeReport (path? : Option String) (render : Array Result → String) : IO Unit := do
+      if let some path := path? then
+        writeFile path (render results)
+    writeReport opts.junitPath junitReport
+    writeReport opts.jsonPath jsonReport
+    writeReport opts.markdownPath markdownReport
+    let failures ← humanReport opts.verbosity results
+    if entries.isEmpty then
+      IO.eprintln "error: no tests were discovered"
+      return 1
+    -- Warn about options that were supplied but never read by any test (typos, removed flags).
+    -- Under `--wfail`, the warning is an error and fails the run.
+    let used ← cfg.usedOptions.get
+    let unused := opts.options.toList.filterMap fun (k, _) => if used.contains k then none else some k
+    unless unused.isEmpty do
+      let level := if opts.wfail then "error" else "warning"
+      IO.eprintln s!"{level}: option(s) provided but never read: {", ".intercalate unused}"
+    -- A process exit status keeps only its low 8 bits, so report a failing run as 1 rather than the
+    -- count, which a multiple of 256 would otherwise wrap to 0.
+    if failures != 0 then return 1
+    if opts.wfail && !unused.isEmpty then return 1
+    return 0
+  cmd.validate args
diff --git a/src/errata/Errata/TestM.lean b/src/errata/Errata/TestM.lean
new file mode 100644
index 00000000..8c51f4dd
--- /dev/null
+++ b/src/errata/Errata/TestM.lean
@@ -0,0 +1,291 @@
+/-
+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.Context
+public import Errata.Result
+public import Errata.Here
+
+public section
+
+set_option linter.missingDocs true
+set_option doc.verso true
+
+namespace Errata
+
+/--
+The monad in which tests run.
+
+The reader carries the configuration and the result log; the exception layer carries a structured
+failure, which the interpreter distinguishes from an {name}`IO.Error` that escapes.
+-/
+abbrev TestM := ReaderT Context (ExceptT TestFailure IO)
+
+/-- A test: a {name}`TestM` action that succeeds unless it fails an assertion or raises an error. -/
+abbrev Test := TestM Unit
+
+/--
+Fails at the location recorded in the context. The runner seeds that with the test's own source
+range, so a failure with no more specific location still points at the test. This is the primitive
+the internal layer uses when no call site is available.
+-/
+def failHere (message : String) (detail? : Option String := none) : TestM α := do
+  throw { message, detail?, location? := some (← read).location }
+
+/--
+Fails at an explicit source location. The assertion language captures its call site with
+{lit}`here%` and reports through this primitive.
+-/
+def failAt (loc : Location) (message : String) (detail? : Option String := none) : TestM α :=
+  throw { message, detail?, location? := some loc }
+
+/-- Fails the current test, or named result, with a message and optional detail. -/
+def fail (message : String) (detail? : Option String := none)
+    (loc : Location := by exact here%) : TestM α :=
+  failAt loc message detail?
+
+/--
+{lit}`failure` fails the test at the context's location, and {lit}`<|>` recovers from an assertion
+failure by running the alternative. An escaping {name}`IO.Error` still propagates, so {lit}`<|>` does
+not mask a broken setup.
+-/
+instance : Alternative TestM where
+  failure := failHere "failure"
+  orElse x y := tryCatch x fun _ => y ()
+
+/-- All values supplied for a project option, in order; records that the option was read. -/
+def optionValues (name : String) : TestM (Array String) := do
+  let ctx ← read
+  ctx.usedOptions.modify (·.insert name)
+  return ctx.options.getD name #[]
+
+/-- The last value supplied for a project option, if any; records that the option was read. -/
+def option? (name : String) : TestM (Option String) :=
+  return (← optionValues name).back?
+
+/-- Whether a project option is present and not set to an explicit false value; records the read. -/
+def flag (name : String) : TestM Bool :=
+  return match (← optionValues name).back? with
+    | some v => v != "false" && v != "0" && v != "no"
+    | none => false
+
+/-- Builds a result for the current scope with the given status and duration. -/
+def Context.mkResult (ctx : Context) (status : Status) (durationMs : Nat := 0) : Result := {
+  package := ctx.package, moduleName := ctx.moduleName, test := ctx.test,
+  resultPath := ctx.resultPath, status, durationMs, description? := ctx.description?
+}
+
+/--
+The result a captured run contributes beyond any nested results it recorded.
+
+A raised error or a failed assertion becomes one error or failed result carrying the captured output.
+A clean run becomes one passing result with the output when it recorded no nested results; when it did
+record some, those results stand for it and it adds nothing of its own.
+-/
+def Context.resultOfOutcome (ctx : Context)
+    (outcome : Except IO.Error (Except TestFailure Unit)) (output : OutputLog) (durationMs : Nat)
+    (hasNested : Bool) : Option Result :=
+  match outcome with
+  | .error e => some { ctx.mkResult (.error (toString e)) durationMs with output }
+  | .ok (.error f) => some { ctx.mkResult (.fail f) durationMs with output }
+  | .ok (.ok ()) => if hasNested then none else some { ctx.mkResult .pass durationMs with output }
+
+/-- Records a skipped result for the current scope. -/
+def skip (reason : String) : TestM Unit := do
+  let ctx ← read
+  ctx.log.modify (·.push (ctx.mkResult (.skip reason)))
+
+/-- Writes a file, creating all parent directories if necessary. -/
+def writeFile (path : System.FilePath) (contents : String) : IO Unit := do
+  if let some parent := path.parent then IO.FS.createDirAll parent
+  IO.FS.writeFile path contents
+
+/-- Writes a binary file, creating all parent directories if necessary. -/
+def writeBinFile (path : System.FilePath) (contents : ByteArray) : IO Unit := do
+  if let some parent := path.parent then IO.FS.createDirAll parent
+  IO.FS.writeBinFile path contents
+
+/--
+The number of bytes in the {lit}`UTF-8` sequence a lead byte introduces, or {name}`none` for a
+continuation or invalid byte.
+-/
+private def utf8SeqLength (b : UInt8) : Option Nat :=
+  if b &&& 0x80 == 0 then some 1
+  else if b &&& 0xE0 == 0xC0 then some 2
+  else if b &&& 0xF0 == 0xE0 then some 3
+  else if b &&& 0xF8 == 0xF0 then some 4
+  else none
+
+/--
+Splits bytes into a prefix ready to decode and a tail that is the start of an unfinished
+{lit}`UTF-8` code point. Bytes that cannot be completed by any continuation go in the prefix, where
+decoding reports them as invalid.
+-/
+private def splitUtf8Tail (bytes : ByteArray) : ByteArray × ByteArray := Id.run do
+  for back in [1 : 4] do
+    if back > bytes.size then break
+    let i := bytes.size - back
+    if let some len := utf8SeqLength bytes[i]! then
+      if i + len > bytes.size then
+        return (bytes.extract 0 i, bytes.extract i bytes.size)
+      else
+        break
+  return (bytes, .empty)
+
+/--
+A stream that hands each write to a destination as a fragment tagged by the stream it came from.
+
+A write of raw bytes may end partway through a {lit}`UTF-8` code point; the trailing bytes wait in a
+buffer for the write that completes them. Bytes that decode to nothing valid are rejected. The
+returned action ends the capture, rejecting any buffered bytes whose code point never arrived.
+-/
+private def captureStream (emit : Output → IO Unit) (mk : String → Output) :
+    IO (IO.FS.Stream × IO Unit) := do
+  let pending ← IO.mkRef ByteArray.empty
+  let invalid : IO.Error :=
+    .userError "a raw byte write to a captured stream was not valid UTF-8"
+  let write (bytes : ByteArray) : IO Unit := do
+    let (ready, rest) := splitUtf8Tail ((← pending.get) ++ bytes)
+    match String.fromUTF8? ready with
+    | some s =>
+      pending.set rest
+      unless s.isEmpty do emit (mk s)
+    | none =>
+      pending.set .empty
+      throw invalid
+  let stream : IO.FS.Stream := {
+    -- A flush partway through a code point is not an error: the partial sequence stays buffered
+    -- for the write that completes it.
+    flush := pure ()
+    read := fun _ => pure .empty
+    write
+    getLine := pure ""
+    -- Text goes through the byte pathway, so output mixed from `putStr` and raw writes is
+    -- recorded in the order it was produced, and text interrupting an unfinished code point is
+    -- reported as the malformed stream it is.
+    putStr := fun s => write s.toUTF8
+    isTty := pure false
+  }
+  let close : IO Unit := do
+    unless (← pending.get).isEmpty do
+      pending.set .empty
+      throw invalid
+  return (stream, close)
+
+/--
+Runs a test action with the given context, capturing its outcome as data rather than letting it
+propagate. The action's stdout and stderr are recorded as text, in order and tagged by stream, and
+returned alongside the outcome. Each fragment is also handed to the context's output destination as
+it is written, so a live runner can stream output while the test runs.
+
+Output from tasks or subprocesses spawned by the test is not captured.
+-/
+def runCapturing (ctx : Context) (act : TestM Unit) :
+    IO (Except IO.Error (Except TestFailure Unit) × OutputLog) := do
+  let log ← IO.mkRef (#[] : Array Output)
+  -- The destination runs with the streams from before the outermost capture, so writing to stdout
+  -- from it reaches the runner instead of re-entering a capture at any level.
+  let real ←
+    match ctx.realStreams? with
+    | some streams => pure streams
+    | none => do pure { stdout := ← IO.getStdout, stderr := ← IO.getStderr : RealStreams }
+  let ctx := { ctx with realStreams? := some real }
+  let emit (o : Output) : IO Unit := do
+    log.modify (·.push o)
+    if let some dest := ctx.writeOutput then
+      unless ← ctx.outputFailed.get do
+        try
+          IO.withStdout real.stdout <| IO.withStderr real.stderr <| dest o
+        catch e =>
+          ctx.outputFailed.set true
+          -- Saying so can fail in turn, when the destination that just failed was stderr itself.
+          try real.stderr.putStr s!"warning: live output destination failed: {e}\n" catch _ => pure ()
+  let (outStream, outClose) ← captureStream emit .stdout
+  let (errStream, errClose) ← captureStream emit .stderr
+  -- Closing inside the captured action makes dangling bytes at the end of the test an error of the
+  -- test itself. When the test already failed, that failure is the report's verdict, and a
+  -- dangling-byte error at close does not displace it.
+  let body : IO (Except TestFailure Unit) := do
+    let r ← (act ctx).run
+    match r with
+    | .ok () =>
+      outClose
+      errClose
+    | .error _ =>
+      try outClose; errClose catch _ => pure ()
+    return r
+  let outcome ← IO.withStdout outStream <| IO.withStderr errStream <| body.toBaseIO
+  return (outcome, { log := ← log.get })
+
+/--
+Runs an action with stdout and stderr captured into a fresh log, then returns the captured text in
+order. The redirection is local to the action, so a test can make assertions about what the action
+wrote.
+-/
+def captureOutput (act : TestM Unit) : TestM OutputLog := do
+  let log ← IO.mkRef (#[] : Array Output)
+  let emit (o : Output) : IO Unit := log.modify (·.push o)
+  let completed ← IO.mkRef false
+  let (outStream, outClose) ← captureStream emit .stdout
+  let (errStream, errClose) ← captureStream emit .stderr
+  try
+    IO.withStdout outStream <| IO.withStderr errStream do
+      act
+      outClose
+      errClose
+    completed.set true
+  finally
+    -- An action that does not complete never receives this log, and what it wrote is what explains
+    -- the failure, so the fragments are handed to the enclosing capture instead.
+    unless ← completed.get do
+      for o in ← log.get do
+        match o with
+        | .stdout s => IO.print s
+        | .stderr s => IO.eprint s
+  return { log := ← log.get }
+
+/--
+Runs a named result within the current test.
+
+Its path extends the current path, and its failure is isolated from sibling results. If the action
+records no nested results and completes, it contributes one passing result; if it throws, it
+contributes one failed result or one that raised an error.
+-/
+def result (name : String) (act : TestM Unit) : TestM Unit :=
+  withReader (fun c => { c with resultPath := c.resultPath.push name }) do
+    let ctx ← read
+    let before := (← ctx.log.get).size
+    let start ← IO.monoMsNow
+    let (outcome, output) ← runCapturing ctx act
+    let stop ← IO.monoMsNow
+    let dur := stop - start
+    let after := (← ctx.log.get).size
+    if let some r := ctx.resultOfOutcome outcome output dur (after != before) then
+      ctx.log.modify (·.push r)
+
+/--
+Expects the action to fail an assertion. The current scope passes if it does and fails if it
+succeeds. An escaping {name}`IO.Error` is not an expected failure: it propagates and is reported as an
+error, so broken setup is not mistaken for a passing negative test.
+-/
+def expectFail (act : TestM Unit) (loc : Location := by exact here%) : TestM Unit := do
+  let ctx ← read
+  let before := (← ctx.log.get).size
+  let threw ←
+    try
+      act
+      pure false
+    catch _ =>
+      pure true
+  -- A nested `result` records a failure rather than propagating it, so the results the action
+  -- recorded are inspected too. Their failures are the expected failure and are dropped.
+  -- Everything else is retained because a recorded error is a broken setup rather than a failure.
+  let logged ← ctx.log.get
+  let added := logged.extract before logged.size
+  let failedInside := added.any (·.status matches .fail _)
+  ctx.log.set (logged.extract 0 before ++ added.filter (fun r => !(r.status matches .fail _)))
+  unless threw || failedInside do
+    failAt loc "expected the action to fail, but it passed"
diff --git a/src/errata/Errata/usage.txt b/src/errata/Errata/usage.txt
new file mode 100644
index 00000000..a9ffa278
--- /dev/null
+++ b/src/errata/Errata/usage.txt
@@ -0,0 +1,12 @@
+Errata test runner
+
+Usage:
+  lake run Errata.run                                      run every test in the package
+  lake run Errata.run LIBRARY...                           run the tests in the given libraries
+  lake run Errata.run LIBRARY... --test-options OPTION...  pass runner options after the marker
+
+Tokens before `--test-options` name libraries. A library is a bare `Library` in this package or a
+`package/Library` reaching into a dependency. Everything after the marker goes to the test runner.
+
+The runner documents its own options, including how to pass options to the tests themselves:
+  lake run Errata.run --test-options --help
diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean
index 28314873..f24dc963 100644
--- a/src/tests/TestMain.lean
+++ b/src/tests/TestMain.lean
@@ -357,6 +357,15 @@ def testBuildLog (_ : Config) : IO Unit := do
     throw <| IO.userError "redirected logging should still accumulate into the logger's buffers"
   IO.println "  All build-log tests passed."
 
+/-- Runs Errata's own tests, reporting them the way the Errata runner does. -/
+def testErrata (config : Config) : IO Unit := do
+  let verbosity := if config.verbose then Errata.Verbosity.quiet else .silent
+  let cfg ← Errata.mkContext (updateGolden := config.updateExpected)
+  let results ← Errata.run cfg errataTests
+  let failures ← Errata.humanReport verbosity results
+  unless failures == 0 do
+    throw <| IO.userError s!"{failures} Errata test(s) failed"
+
 open Verso.Integration in
 def tests := [
   testBuildLog,
@@ -380,7 +389,8 @@ def tests := [
   testLiterateConfig,
   testLiterateHtml,
   testLiterateHtmlMultiRoot,
-  testSetupLiterate
+  testSetupLiterate,
+  testErrata
 ]
 
 def getConfig (config : Config) : List String → IO Config
diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean
index 5bcdd422..52967abf 100644
--- a/src/tests/Tests.lean
+++ b/src/tests/Tests.lean
@@ -14,6 +14,7 @@ import Tests.DocVisibility
 import Tests.DocstringMissing
 import Tests.DocstringMissingLegacy
 import Tests.HighlightedToTeX
+import Tests.ErrataSuite
 import Tests.ExpanderSignatures
 import Tests.ExpanderSignaturesLegacy
 import Tests.Html
diff --git a/src/tests/Tests/ErrataSuite.lean b/src/tests/Tests/ErrataSuite.lean
new file mode 100644
index 00000000..ae0a5a21
--- /dev/null
+++ b/src/tests/Tests/ErrataSuite.lean
@@ -0,0 +1,12 @@
+/-
+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
+import all ErrataTests
+
+/-- Errata's own tests, gathered so that a driver outside the module system can run them. -/
+public def errataTests : Array Errata.TestEntry := getAllTests% "verso" ErrataTests