diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index 6aa2e6fb..557e2780 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -13,7 +13,7 @@ Hypatia is the neurosymbolic CI/CD intelligence layer for the hyperpolymath ecos
 ## Architecture
 
 ```
-Hypatia                       # 140 Elixir modules total (`shopt -s globstar; ls lib/**/*.ex | wc -l`)
+Hypatia                       # 141 Elixir modules total (`shopt -s globstar; ls lib/**/*.ex | wc -l`)
 ├── Elixir pipeline          # core: pattern analysis, dispatch, learning
 ├── Merge orchestration       # 12 modules — leases, ledger, ticker (largest subsystem)
 ├── Kin subsystem             # 6 modules — contingency, arbiter, gate, watchdog
@@ -123,6 +123,7 @@ OutcomeTracker.record_outcome()         -- Feedback loop
 | `learning_scheduler.ex` | GenServer: polls outcomes every 5 min, drives feedback loop |
 | `self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery |
 | `hypatia/verdict.ex` | HYP-01: every finding names its `support`, `evidence` and a derived `level` (mirror of `Verdict.idr`; contract `schema/findings.ncl`) |
+| `hypatia/verdict/retraction.ex` | HYP-01: quarantine retracts the findings resting only on a quarantined rule/bot/prover (`Quarantine.retract_dependents/1`; mirror of `Retraction.idr`) |
 | `application.ex` | OTP Application supervisor for all GenServers |
 
 ### VCL Query Layer (lib/vcl/)
@@ -174,6 +175,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `FFI.idr` | GADT constructors for all C ABI functions + ffiReturnsApiResponse proof |
 | `RuleEngine.idr` | Rule-evaluation types |
 | `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
+| `Retraction.idr` | Quarantine as retraction (HYP-01): a token survives iff its support thins into what remains; a finding survives through one of its tokens. Transcribed from residual-evidence-types `Revision.agda` @ 97244f5 |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).
 The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the
@@ -277,6 +279,8 @@ into redoing finished work.
    are fully-built GenServers that **no dispatch path actually calls**. Treat the "3 safety
    systems" line in any older doc as describing capability, not enforcement. This is the most
    dangerous stale claim the docs used to make.
+   `Quarantine.retract_dependents/1` (HYP-01) is in the same position: implemented and tested,
+   called by no scan or dispatch path.
 3. **242 tests are dark and red.** The `:verisim_data` tag is excluded unconditionally in
    `test/test_helper.exs`, never included by any workflow, and `mix test --only verisim_data`
    yields **129 failures**. "The suite passes" is therefore scoped to 83% of it.
diff --git a/lib/dispatch_manifest.ex b/lib/dispatch_manifest.ex
index ff1bf426..45b62bc4 100644
--- a/lib/dispatch_manifest.ex
+++ b/lib/dispatch_manifest.ex
@@ -13,21 +13,85 @@ defmodule Hypatia.DispatchManifest do
   - recipe_id, confidence, fix_script (for eliminate)
   - proven_module (for substitute)
   - pattern_id, category, description, repo, severity
+  - facts: the verdict records the step derives from (HYP-01)
+
+  Facts derive workflows, never the reverse (HYP-01). Every step names the
+  fact it was derived from: the pattern it acts on, that pattern's support
+  (`observed` with the fleet occurrence count, or `pattern`) and the level
+  derived from them (`Hypatia.Verdict.level/2`). A step that can name no
+  fact is refused, and so is the whole manifest: `compile/1` returns
+  `{:error, {:factless_steps, steps}}` and `write/2` writes nothing, so
+  dispatch-runner.sh never sees a step that rests on nothing. A step's
+  Bayesian `confidence` is belief and stays in its own field; it is never a
+  fact.
   """
 
   alias Hypatia.TriangleRouter
+  alias Hypatia.Verdict
 
   require Logger
 
   @verisimdb_path Application.compile_env(:hypatia, :verisimdb_data_path, "data/verisim")
   @fix_scripts_dir Application.compile_env(:hypatia, :fix_scripts_dir, "scripts/fix-scripts")
 
+  @doc """
+  Compile routed actions into manifest steps, each naming its facts.
+
+  Returns `{:ok, steps}`, or `{:error, {:factless_steps, steps}}` naming
+  every step (its position, tier and pattern id) that could name no fact.
+  """
+  @spec compile(list()) :: {:ok, [map()]} | {:error, {:factless_steps, [map()]}}
+  def compile(routed_actions) do
+    lines =
+      Enum.flat_map(routed_actions, fn action ->
+        case action_to_manifest_entry(action) do
+          nil -> []
+          entries when is_list(entries) -> entries
+          entry -> [entry]
+        end
+      end)
+
+    factless =
+      lines
+      |> Enum.with_index()
+      |> Enum.filter(fn {entry, _} -> entry["facts"] == [] end)
+      |> Enum.map(fn {entry, index} ->
+        %{"step" => index, "tier" => entry["tier"], "pattern_id" => entry["pattern_id"]}
+      end)
+
+    case factless do
+      [] -> {:ok, lines}
+      steps -> {:error, {:factless_steps, steps}}
+    end
+  end
+
   @doc """
   Write a dispatch manifest from a list of routed actions.
-  Returns {:ok, path, stats} on success.
+
+  Returns `{:ok, path, stats}`, or `{:error, {:factless_steps, steps}}`
+  without writing anything when a step names no fact (`compile/1`).
+  `opts[:dispatch_dir]` overrides the directory (default
+  `<verisimdb_data_path>/dispatch`).
   """
-  def write(routed_actions) do
-    dispatch_dir = Path.join(@verisimdb_path, "dispatch")
+  def write(routed_actions, opts \\ []) do
+    case compile(routed_actions) do
+      {:ok, lines} ->
+        write_lines(
+          lines,
+          Keyword.get(opts, :dispatch_dir, Path.join(@verisimdb_path, "dispatch"))
+        )
+
+      {:error, {:factless_steps, steps}} = refused ->
+        Logger.error(
+          "Dispatch manifest REFUSED: #{length(steps)} step(s) name no fact " <>
+            "(#{inspect(Enum.take(steps, 5))}); nothing written"
+        )
+
+        refused
+    end
+  end
+
+  defp write_lines(lines, dispatch_dir) do
     File.mkdir_p!(dispatch_dir)
 
     manifest_path = Path.join(dispatch_dir, "pending.jsonl")
@@ -36,16 +100,6 @@ defmodule Hypatia.DispatchManifest do
     archive_name = "dispatch-#{Date.utc_today() |> Date.to_iso8601()}.jsonl"
     archive_path = Path.join(dispatch_dir, archive_name)
 
-    lines =
-      routed_actions
-      |> Enum.flat_map(fn action ->
-        case action_to_manifest_entry(action) do
-          nil -> []
-          entries when is_list(entries) -> entries
-          entry -> [entry]
-        end
-      end)
-
     content =
       Enum.map_join(lines, "\n", fn entry ->
         {:ok, json} = Jason.encode(entry)
@@ -103,6 +157,7 @@ defmodule Hypatia.DispatchManifest do
       "match" => Map.get(recipe, "match"),
       "replacement" => Map.get(recipe, "replacement"),
       "proven_module" => Map.get(recipe, "proven_module"),
+      "facts" => facts_for(pattern),
       "timestamp" => DateTime.utc_now() |> DateTime.to_iso8601()
     }
   end
@@ -126,6 +181,7 @@ defmodule Hypatia.DispatchManifest do
       "proven_module" => Map.get(recipe, "proven_module"),
       "proven_modules" => Map.get(recipe, "proven_modules", []),
       "formally_proven" => Map.get(recipe, "formally_proven", false),
+      "facts" => facts_for(pattern),
       "timestamp" => DateTime.utc_now() |> DateTime.to_iso8601()
     }
   end
@@ -145,12 +201,49 @@ defmodule Hypatia.DispatchManifest do
       "recipe_id" => nil,
       "confidence" => 0.0,
       "auto_fixable" => false,
+      "facts" => facts_for(finding),
       "timestamp" => DateTime.utc_now() |> DateTime.to_iso8601()
     }
   end
 
   defp action_to_manifest_entry(_), do: nil
 
+  # The verdict a step derives from. A registry pattern is evidence that a
+  # pattern matched, `occurrences` times across the fleet: `observed` support
+  # at level epi. Without a pattern id there is nothing to name, and the step
+  # is factless (compile/1 refuses the manifest).
+  defp facts_for(source) do
+    case Map.get(source, "id") do
+      id when is_binary(id) and id not in ["", "unknown"] ->
+        {support, observations} =
+          case Map.get(source, "occurrences") do
+            n when is_integer(n) and n > 0 -> {%{kind: "observed", observations: n}, n}
+            _ -> {%{kind: "pattern"}, 1}
+          end
+
+        evidence = [
+          %{
+            rule: "pattern_registry/#{id}",
+            rule_version: Verdict.rule_version(),
+            observations: observations
+          }
+        ]
+
+        [
+          %{
+            "pattern_id" => id,
+            "support" => Map.new(support, fn {k, v} -> {Atom.to_string(k), v} end),
+            "evidence" =>
+              Enum.map(evidence, &Map.new(&1, fn {k, v} -> {Atom.to_string(k), v} end)),
+            "level" => Verdict.level(support, evidence)
+          }
+        ]
+
+      _ ->
+        []
+    end
+  end
+
   defp get_repo(pattern_or_finding) do
     Map.get(pattern_or_finding, "routed_repo") ||
       case Map.get(pattern_or_finding, "repos_affected_list", []) do
diff --git a/lib/hypatia/verdict/retraction.ex b/lib/hypatia/verdict/retraction.ex
new file mode 100644
index 00000000..778dc14b
--- /dev/null
+++ b/lib/hypatia/verdict/retraction.ex
@@ -0,0 +1,139 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+defmodule Hypatia.Verdict.Retraction do
+  @moduledoc """
+  Quarantine as retraction (HYP-01).
+
+  Quarantining a bot or a rule retracts an assumption. Each evidence token a
+  finding was issued on rests on assumptions: `{:rule, "module/id"}` for the
+  rule that fired and, when the token names one, `{:bot, name}` for the bot
+  that reported it. A confirming prover re-check rests on `{:prover, name}`.
+
+  The rule is residual-evidence-types' `survives-retraction` /
+  `survives-dependent` (Revision.agda, pinned in `scripts/fetch-siblings.sh`),
+  transcribed in `src/Hypatia/ABI/Retraction.idr`:
+
+    * a token survives exactly when none of the assumptions it rests on has
+      been retracted (its support thins into what remains);
+    * a finding survives while one of its tokens does, or while it rests on a
+      confirming prover re-check whose prover is not retracted;
+    * a surviving finding keeps only its surviving tokens, and its level is
+      re-derived from them;
+    * a finding with nothing left is retracted, never silently downgraded:
+      it moves to the retracted list, with its original evidence kept for
+      audit and the retracted assumptions it rested on named
+      (`:retracted_by`, wire names from `name/1`).
+
+  Pure: the caller supplies the retracted assumptions
+  (`Hypatia.Safety.Quarantine.retracted_assumptions/0` reads them from the
+  quarantine table).
+  """
+
+  alias Hypatia.Verdict
+
+  @type assumption :: {:rule, String.t()} | {:bot, String.t()} | {:prover, String.t()}
+
+  @doc """
+  Wire name of an assumption (`"rule:<module>/<id>"`, `"bot:<name>"`,
+  `"prover:<name>"`), as written into `:retracted_by`.
+  """
+  @spec name(assumption()) :: String.t()
+  def name({kind, id}) when kind in [:rule, :bot, :prover], do: "#{kind}:#{id}"
+
+  @doc """
+  The assumption a quarantine key retracts: `"rule:<module>/<id>"` a rule,
+  `"prover:<name>"` a prover, anything else the bot of that name (the
+  quarantine table has always been keyed by bot name).
+  """
+  @spec parse(String.t()) :: assumption()
+  def parse("rule:" <> rule), do: {:rule, rule}
+  def parse("prover:" <> prover), do: {:prover, prover}
+  def parse("bot:" <> bot), do: {:bot, bot}
+  def parse(bot) when is_binary(bot), do: {:bot, bot}
+
+  @doc "The assumptions an evidence token rests on."
+  @spec token_support(map()) :: [assumption()]
+  def token_support(token) do
+    rule = [{:rule, to_string(Map.get(token, :rule, ""))}]
+
+    case Map.get(token, :bot) do
+      nil -> rule
+      bot -> rule ++ [{:bot, to_string(bot)}]
+    end
+  end
+
+  @doc "Does the token survive the retraction of `retracted`?"
+  @spec token_survives?(map(), MapSet.t(assumption())) :: boolean()
+  def token_survives?(token, retracted) do
+    token |> token_support() |> Enum.all?(&(not MapSet.member?(retracted, &1)))
+  end
+
+  @doc """
+  Split `findings` into those that survive the retraction of `retracted` and
+  those that do not. Returns `{kept, retracted_findings}`.
+  """
+  @spec retract([map()], Enumerable.t()) :: {[map()], [map()]}
+  def retract(findings, retracted) do
+    retracted = MapSet.new(retracted)
+
+    findings
+    |> Enum.map(&retract_one(&1, retracted))
+    |> Enum.split_with(&match?({:kept, _}, &1))
+    |> then(fn {kept, gone} ->
+      {Enum.map(kept, &elem(&1, 1)), Enum.map(gone, &elem(&1, 1))}
+    end)
+  end
+
+  defp retract_one(finding, retracted) do
+    evidence = Map.get(finding, :evidence) || []
+    {alive, dead} = Enum.split_with(evidence, &token_survives?(&1, retracted))
+    support = Map.get(finding, :support)
+    recheck_retracted? = recheck_retracted?(support, retracted)
+    # A re-check whose prover is retracted supports nothing any more: what
+    # is left is the pattern match its tokens record.
+    kept_support = if recheck_retracted?, do: %{kind: "pattern"}, else: support
+
+    cond do
+      dead == [] and not recheck_retracted? ->
+        {:kept, finding}
+
+      alive != [] or confirming_recheck?(kept_support) ->
+        {:kept,
+         finding
+         |> Map.put(:support, kept_support)
+         |> Map.put(:evidence, alive)
+         |> Map.put(:retracted_evidence, dead)
+         |> maybe_put(:retracted_support, recheck_retracted?, support)
+         |> Map.put(:level, Verdict.level(kept_support, alive))}
+
+      true ->
+        by = retracted_by(dead, retracted) ++ prover_retracted(support, recheck_retracted?)
+        {:retracted, Map.put(finding, :retracted_by, Enum.map(by, &name/1))}
+    end
+  end
+
+  defp confirming_recheck?(%{kind: "mechanical", result: "confirms"}), do: true
+  defp confirming_recheck?(_support), do: false
+
+  # Only a confirming re-check supports the finding, so only its prover can
+  # be retracted support; a refuting re-check never rested the finding on
+  # anything, and naming its prover in :retracted_by would be false.
+  defp recheck_retracted?(%{kind: "mechanical", result: "confirms", prover: prover}, retracted),
+    do: MapSet.member?(retracted, {:prover, prover})
+
+  defp recheck_retracted?(_support, _retracted), do: false
+
+  defp prover_retracted(%{prover: prover}, true), do: [{:prover, prover}]
+  defp prover_retracted(_support, false), do: []
+
+  defp maybe_put(map, _key, false, _value), do: map
+  defp maybe_put(map, key, true, value), do: Map.put(map, key, value)
+
+  defp retracted_by(tokens, retracted) do
+    tokens
+    |> Enum.flat_map(&token_support/1)
+    |> Enum.filter(&MapSet.member?(retracted, &1))
+    |> Enum.uniq()
+  end
+end
diff --git a/lib/pattern_analyzer.ex b/lib/pattern_analyzer.ex
index fe0f4897..6a61d645 100644
--- a/lib/pattern_analyzer.ex
+++ b/lib/pattern_analyzer.ex
@@ -76,11 +76,11 @@ defmodule Hypatia.PatternAnalyzer do
     # and aggregated confidence from all 5 neural networks.
     routed = enhance_with_neural(routed)
 
-    # Step 5: Dispatch routed actions to fleet
-    Enum.each(routed, &FleetDispatcher.dispatch_routed_action/1)
-
-    # Step 6: Write dispatch manifest (JSONL -- executable by dispatch-runner.sh)
-    {:ok, manifest_path, manifest_stats} = DispatchManifest.write(routed)
+    # Steps 5-6: Dispatch routed actions to the fleet and write the dispatch
+    # manifest (JSONL -- executable by dispatch-runner.sh). Both happen only
+    # when every step names its fact (HYP-01): a refused manifest dispatches
+    # nothing.
+    {manifest_path, manifest_stats} = dispatch_and_write(routed)
 
     Logger.info(
       "Manifest: #{manifest_stats.auto_execute} auto, #{manifest_stats.review} review, " <>
@@ -186,8 +186,7 @@ defmodule Hypatia.PatternAnalyzer do
 
     # Neural enhancement + dispatch
     all_routed = enhance_with_neural(all_routed)
-    Enum.each(all_routed, &FleetDispatcher.dispatch_routed_action/1)
-    {:ok, manifest_path, manifest_stats} = DispatchManifest.write(all_routed)
+    {manifest_path, manifest_stats} = dispatch_and_write(all_routed)
 
     summary =
       generate_summary(all_routed, scans)
@@ -392,4 +391,40 @@ defmodule Hypatia.PatternAnalyzer do
 
     patterns
   end
+
+  @doc false
+  # HYP-01: facts derive workflows. The manifest is compiled first, and the
+  # routed actions reach the fleet (and the manifest is written) only when
+  # every step names its fact. A refused manifest dispatches nothing and
+  # writes nothing; it is reported as a manifest that was not written (path
+  # nil, zero counts, the refused steps named) instead of crashing the
+  # pipeline on a match against {:ok, _, _}. `opts[:dispatch]` (default
+  # FleetDispatcher.dispatch_routed_action/1) and `opts[:dispatch_dir]` exist
+  # for the tests.
+  def dispatch_and_write(routed, opts \\ []) do
+    dispatch = Keyword.get(opts, :dispatch, &FleetDispatcher.dispatch_routed_action/1)
+    write_opts = Keyword.take(opts, [:dispatch_dir])
+
+    with {:ok, _steps} <- DispatchManifest.compile(routed),
+         :ok <- Enum.each(routed, dispatch),
+         {:ok, path, stats} <- DispatchManifest.write(routed, write_opts) do
+      {path, stats}
+    else
+      {:error, {:factless_steps, steps}} ->
+        Logger.error(
+          "Fleet dispatch skipped: #{length(steps)} routed action(s) name no fact; " <>
+            "nothing dispatched, no manifest written"
+        )
+
+        {nil,
+         %{
+           total: 0,
+           auto_execute: 0,
+           review: 0,
+           report_only: 0,
+           by_tier: %{eliminate: 0, substitute: 0, control: 0},
+           refused: {:factless_steps, steps}
+         }}
+    end
+  end
 end
diff --git a/lib/safety/quarantine.ex b/lib/safety/quarantine.ex
index 532be370..0421761a 100644
--- a/lib/safety/quarantine.ex
+++ b/lib/safety/quarantine.ex
@@ -22,6 +22,15 @@ defmodule Hypatia.Safety.Quarantine do
   - :soft quarantine expires after 24 hours
   - :hard quarantine expires after 72 hours
   - :permanent never expires automatically
+
+  Quarantine is retraction (HYP-01). Every quarantined key, at any level,
+  retracts an assumption: a bot name retracts that bot, `"rule:<module>/<id>"`
+  a rule, `"prover:<name>"` a prover. `retract_dependents/1` applies the
+  retraction to findings: those whose every evidence token rested on a
+  retracted assumption are retracted, and the rest keep only their surviving
+  tokens (`Hypatia.Verdict.Retraction`). A soft quarantine retracts too: it is
+  triggered by a high false-positive rate, which is exactly a reason to stop
+  trusting the findings, whatever the bot may still be dispatched.
   """
 
   use GenServer
@@ -84,6 +93,24 @@ defmodule Hypatia.Safety.Quarantine do
     GenServer.call(__MODULE__, :list)
   end
 
+  @doc """
+  The assumptions the current quarantine table retracts
+  (`Hypatia.Verdict.Retraction.parse/1` of every quarantined key).
+  """
+  def retracted_assumptions do
+    list_quarantined()
+    |> Map.keys()
+    |> MapSet.new(&Hypatia.Verdict.Retraction.parse/1)
+  end
+
+  @doc """
+  Retract the findings that rest only on quarantined bots, rules or provers.
+  Returns `{kept, retracted}`; see `Hypatia.Verdict.Retraction.retract/2`.
+  """
+  def retract_dependents(findings) do
+    Hypatia.Verdict.Retraction.retract(findings, retracted_assumptions())
+  end
+
   @doc "Get reroute target for a quarantined bot"
   def reroute_target(bot_name) do
     GenServer.call(__MODULE__, {:reroute, bot_name})
diff --git a/scripts/check-sibling-citations.sh b/scripts/check-sibling-citations.sh
index aabaf4f4..77ddd1bb 100755
--- a/scripts/check-sibling-citations.sh
+++ b/scripts/check-sibling-citations.sh
@@ -29,12 +29,27 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 2
 deps=_build/dependencies
 
 # citing module | sibling | file in sibling | definition
+# A row means "the citing module names this definition at the pin", whether
+# it transcribes it or says why it does not; the header is the authority on
+# which.
 citations=(
   "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|Warrant"
   "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|Epi"
   "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|SoundWarrant"
   "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|sound-epi"
   "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Applications/RapidNJSkip.agda|no-receipt-reflection"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Context.agda|_⊆_"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Context.agda|⊆-refl"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Context.agda|⊆-trans"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Context.agda|no-thinning-into-empty"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Revision.agda|Retraction"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Revision.agda|retract-⊆"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Revision.agda|Dependent"
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Revision.agda|survives-dependent"
+  # Named in Retraction.idr's header as deliberately NOT transcribed (it
+  # gives back Holds, which the Idris record drops); the row checks only that
+  # the name the header cites exists at the pin.
+  "src/Hypatia/ABI/Retraction.idr|residual-evidence-types|src/ResidualEvidence/Revision.agda|dependent-holds"
 )
 
 failures=0
diff --git a/scripts/check-verdicts.sh b/scripts/check-verdicts.sh
index 4c925f26..ba896bcd 100755
--- a/scripts/check-verdicts.sh
+++ b/scripts/check-verdicts.sh
@@ -10,7 +10,7 @@
 #
 #   1. the ABI package builds (the positive set, first: a broken toolchain or
 #      a missing import must never turn into a "successful" rejection);
-#   2. src/Hypatia/ABI/Verdict.idr contains no escape-hatch marker at all;
+#   2. Verdict.idr and Retraction.idr contain no escape-hatch marker at all;
 #   3. every module under tests/accept/ is ACCEPTED (positive controls);
 #   4. every module under tests/reject/ is REFUSED, and refused only at its
 #      declaration `invalid`, with the diagnostic its `-- EXPECT:` line
@@ -39,13 +39,15 @@ mkdir -p "$logs"
 "$idris2" --build src/abi/hypatia-abi.ipkg
 export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}"
 
-# 2. No escape hatch in the module the rejections are about.
-if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \
-     src/Hypatia/ABI/Verdict.idr; then
-  echo "ERROR: escape-hatch marker in src/Hypatia/ABI/Verdict.idr" >&2
-  exit 1
-fi
-echo "PASS: no escape-hatch marker in src/Hypatia/ABI/Verdict.idr"
+# 2. No escape hatch in the modules the rejections are about.
+for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr; do
+  if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \
+       "$module"; then
+    echo "ERROR: escape-hatch marker in $module" >&2
+    exit 1
+  fi
+  echo "PASS: no escape-hatch marker in $module"
+done
 
 shopt -s nullglob
 accepts=(tests/accept/*.idr)
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
index 7130b330..1ee02727 100755
--- a/scripts/fetch-siblings.sh
+++ b/scripts/fetch-siblings.sh
@@ -33,3 +33,5 @@ fetch() {
 mkdir -p "$deps"
 # HYP-01 verdict record (src/Hypatia/ABI/Verdict.idr): Warrant / Epi / SoundWarrant.
 fetch epistemic-types hyperpolymath/epistemic-types 6a68de3141a981d766fd006b312f0919ade334bf
+# HYP-01 quarantine as retraction (src/Hypatia/ABI/Retraction.idr): Revision.agda.
+fetch residual-evidence-types hyperpolymath/residual-evidence-types 97244f5cb63bd6697caff261b187b62e9788b692
diff --git a/src/Hypatia/ABI/Retraction.idr b/src/Hypatia/ABI/Retraction.idr
new file mode 100644
index 00000000..5d51fa51
--- /dev/null
+++ b/src/Hypatia/ABI/Retraction.idr
@@ -0,0 +1,161 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Hypatia ABI — Quarantine as retraction (HYP-01)
+--
+-- Quarantining a bot or a rule retracts an assumption.  Each evidence token
+-- a finding was issued on rests on assumptions: the rule that fired and,
+-- for a fleet finding, the bot that reported it; a confirming prover
+-- re-check rests on the prover.  A token survives a retraction exactly when
+-- its support thins into what remains, and a finding survives while one of
+-- its tokens does.  lib/hypatia/verdict/retraction.ex is the runtime mirror.
+--
+-- What is proved here (Idris2, %default total, no proof-bypass primitives):
+--   * `retractThin`: a retraction is a thinning read downwards;
+--   * `survivesDependent`: a token whose support thins into the retracted
+--     context still rests on the same support there;
+--   * `thinElem` / `retractedSupportDies`: a token whose support names an
+--     assumption absent from the remaining context does not survive;
+--   * `survivor` / `noTokensNoSurvival`: a finding survives exactly through
+--     one of its tokens, and a finding with no tokens has nothing to survive
+--     by.
+--
+-- Transcription source (read for the shape only, never imported):
+--   hyperpolymath/residual-evidence-types @ 97244f5cb63bd6697caff261b187b62e9788b692
+--   src/ResidualEvidence/Context.agda  — the thinning _⊆_ (done / keep /
+--     drop), ⊆-refl, ⊆-trans, no-thinning-into-empty
+--   src/ResidualEvidence/Revision.agda — Retraction (first / later),
+--     retract-⊆, Dependent, survives-dependent
+-- Hypatia cannot state a finding's claim as a type, so `Dependent` keeps the
+-- support and its thinning and drops the `Holds` field: what retraction acts
+-- on is the naming of the support, and that is what is transcribed.  For the
+-- same reason Revision.agda's dependent-holds (a Dependent gives back Holds)
+-- has no counterpart here.  The
+-- correspondence is ASSUMED, not checked; scripts/check-sibling-citations.sh
+-- checks only that the cited names exist at the pin.
+
+module Hypatia.ABI.Retraction
+
+import Data.List.Elem
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: Assumptions and thinnings
+------------------------------------------------------------------------
+
+||| What an evidence token can rest on.
+public export
+data Assumption = RuleA String | BotA String | ProverA String
+
+||| Order-preserving embedding: `Thin s g` says `g` assumes everything `s`
+||| does, in order, and possibly more (Context.agda `_⊆_`).
+public export
+data Thin : List a -> List a -> Type where
+  Done : Thin [] []
+  Keep : Thin s g -> Thin (x :: s) (x :: g)
+  Drop : Thin s g -> Thin s (x :: g)
+
+public export
+thinRefl : {g : List a} -> Thin g g
+thinRefl {g = []} = Done
+thinRefl {g = x :: g} = Keep thinRefl
+
+public export
+thinTrans : Thin s g -> Thin g h -> Thin s h
+thinTrans t Done = t
+thinTrans t (Drop t') = Drop (thinTrans t t')
+thinTrans (Keep t) (Keep t') = Keep (thinTrans t t')
+thinTrans (Drop t) (Keep t') = Drop (thinTrans t t')
+
+||| A non-empty context never thins into the empty one.
+public export
+noThinIntoEmpty : Thin (x :: s) [] -> Void
+noThinIntoEmpty Done impossible
+noThinIntoEmpty (Keep _) impossible
+noThinIntoEmpty (Drop _) impossible
+
+||| Every assumption of the smaller context occurs in the larger one.
+public export
+thinElem : Elem x s -> Thin s g -> Elem x g
+thinElem Here (Keep _) = Here
+thinElem (There e) (Keep t) = There (thinElem e t)
+thinElem e (Drop t) = There (thinElem e t)
+
+------------------------------------------------------------------------
+-- Section 2: Retraction
+------------------------------------------------------------------------
+
+||| `d` is `g` with exactly one assumption retracted, named by its position
+||| (Revision.agda `Retraction`).
+public export
+data Retraction : List a -> List a -> Type where
+  First : Retraction (x :: g) g
+  Later : Retraction g d -> Retraction (x :: g) (x :: d)
+
+||| The assumption a retraction removes.
+public export
+retracted : {0 a : Type} -> {g, d : List a} -> Retraction g d -> a
+retracted (First {x}) = x
+retracted (Later r) = retracted r
+
+||| A retraction is a thinning of the smaller context into the larger one
+||| (Revision.agda `retract-⊆`).
+public export
+retractThin : {d : List a} -> Retraction g d -> Thin d g
+retractThin First = Drop thinRefl
+retractThin {d = _ :: _} (Later r) = Keep (retractThin r)
+
+------------------------------------------------------------------------
+-- Section 3: Tokens rest on their support
+------------------------------------------------------------------------
+
+||| An evidence token under context `g`, naming the support it rests on
+||| (Revision.agda `Dependent`, without `Holds`).
+public export
+record Dependent (g : List a) where
+  constructor RestsOn
+  support : List a
+  thin    : Thin support g
+
+||| The whole context is always a support (Context.agda `⊆-refl`).
+public export
+restsOnAll : (g : List a) -> Dependent g
+restsOnAll g = RestsOn g thinRefl
+
+||| A token whose support thins into the retracted context survives, resting
+||| on the same support (Revision.agda `survives-dependent`).  The premise is
+||| against the retracted context `d`, never against `g`.
+public export
+survivesDependent : Retraction g d -> (dep : Dependent g)
+                 -> Thin (support dep) d -> Dependent d
+survivesDependent _ (RestsOn s _) avoid = RestsOn s avoid
+
+||| What retraction cannot do: a support naming an assumption that no longer
+||| occurs in the remaining context does not thin into it.
+public export
+retractedSupportDies : Elem x s -> Not (Elem x d) -> Not (Thin s d)
+retractedSupportDies e absent t = absent (thinElem e t)
+
+------------------------------------------------------------------------
+-- Section 4: Findings survive through a token
+------------------------------------------------------------------------
+
+||| Some token of a finding survives into `d`.
+public export
+data AnySurvives : (d : List a) -> List (Dependent g) -> Type where
+  HereS  : Thin (support t) d -> AnySurvives d (t :: ts)
+  ThereS : AnySurvives d ts -> AnySurvives d (t :: ts)
+
+||| A finding with no tokens has nothing to survive by.
+public export
+noTokensNoSurvival : AnySurvives d [] -> Void
+noTokensNoSurvival (HereS _) impossible
+noTokensNoSurvival (ThereS _) impossible
+
+||| A surviving finding hands back the token it survives by, as a token of
+||| the retracted context.
+public export
+survivor : Retraction g d -> {ts : List (Dependent g)} -> AnySurvives d ts -> Dependent d
+survivor r {ts = t :: _} (HereS avoid) = survivesDependent r t avoid
+survivor r {ts = _ :: _} (ThereS rest) = survivor r rest
diff --git a/src/abi/README.adoc b/src/abi/README.adoc
index 49e4c87e..46a642da 100644
--- a/src/abi/README.adoc
+++ b/src/abi/README.adoc
@@ -35,6 +35,7 @@ been undetectable, so the dead copy was deleted (issue #815, DEBT-REGISTER C-4).
 |`src/Hypatia/ABI/FFI.idr` |GADT constructors for all 7 C ABI functions + `ffiReturnsApiResponse` proof
 |`src/Hypatia/ABI/RuleEngine.idr` |Rule engine type definitions and proof obligations
 |`src/Hypatia/ABI/Verdict.idr` |Verdict records (HYP-01): every verdict names its support; `Sound` only from a confirming prover re-check. Gate: `just check-verdicts`
+|`src/Hypatia/ABI/Retraction.idr` |Quarantine as retraction (HYP-01): a finding survives a quarantine only through a token whose support is kept. Gate: `just check-verdicts`
 |`src/Hypatia/ABI/Gen.idr` |The generator: evaluates the ABI and emits the generated mirrors
 |===
 
diff --git a/src/abi/hypatia-abi.ipkg b/src/abi/hypatia-abi.ipkg
index 2ef9b51c..7a8964a9 100644
--- a/src/abi/hypatia-abi.ipkg
+++ b/src/abi/hypatia-abi.ipkg
@@ -23,6 +23,7 @@ modules = Hypatia.ABI.Types
         , Hypatia.ABI.FFI
         , Hypatia.ABI.RuleEngine
         , Hypatia.ABI.Verdict
+        , Hypatia.ABI.Retraction
 
 builddir = "../../build/abi"
 
diff --git a/test/dispatch_manifest_test.exs b/test/dispatch_manifest_test.exs
index 70d5b509..6f23bea1 100644
--- a/test/dispatch_manifest_test.exs
+++ b/test/dispatch_manifest_test.exs
@@ -45,4 +45,133 @@ defmodule Hypatia.DispatchManifestTest do
       assert stats.report_only >= 1
     end
   end
+
+  # HYP-01: facts derive workflows. The manifest is the workflow hypatia
+  # derives for dispatch-runner.sh; every step names its fact, and a step
+  # that names none refuses the whole manifest.
+  describe "facts (HYP-01)" do
+    @eliminate_recipe %{"id" => "recipe-x", "confidence" => 0.99, "auto_fixable" => true}
+
+    defp pattern(id, extra \\ %{}) do
+      Map.merge(
+        %{
+          "id" => id,
+          "category" => "CommandInjection",
+          "severity" => "High",
+          "routed_repo" => "test-repo"
+        },
+        extra
+      )
+    end
+
+    test "every step names the verdict it derives from" do
+      routed = [
+        {:eliminate, @eliminate_recipe, pattern("PA009-x", %{"occurrences" => 7})},
+        {:substitute, %{"id" => "r2", "confidence" => 0.9}, pattern("PA010-y")},
+        {:control, pattern("PA006-z")}
+      ]
+
+      assert {:ok, steps} = DispatchManifest.compile(routed)
+      assert length(steps) == 3
+
+      [elim, subst, ctrl] = steps
+
+      assert [
+               %{
+                 "pattern_id" => "PA009-x",
+                 "support" => %{"kind" => "observed", "observations" => 7},
+                 "level" => "epi",
+                 "evidence" => [%{"rule" => "pattern_registry/PA009-x"}]
+               }
+             ] = elim["facts"]
+
+      assert [%{"pattern_id" => "PA010-y", "support" => %{"kind" => "pattern"}}] =
+               subst["facts"]
+
+      assert [%{"pattern_id" => "PA006-z", "level" => "epi"}] = ctrl["facts"]
+
+      # Confidence is belief and stays in its own field: no fact carries it,
+      # and no fact is ever "sound".
+      for step <- steps, fact <- step["facts"] do
+        refute Map.has_key?(fact, "confidence")
+        assert fact["level"] != "sound"
+      end
+    end
+
+    test "the written manifest shows each step's facts", %{} do
+      dir = Path.join(System.tmp_dir!(), "hypatia-manifest-#{System.unique_integer([:positive])}")
+      on_exit(fn -> File.rm_rf(dir) end)
+
+      assert {:ok, path, %{total: 1}} =
+               DispatchManifest.write([{:control, pattern("PA006-z")}], dispatch_dir: dir)
+
+      [line] = path |> File.read!() |> String.split("\n", trim: true)
+      assert %{"facts" => [%{"pattern_id" => "PA006-z"}]} = Jason.decode!(line)
+    end
+
+    test "a factless step refuses the whole manifest, and nothing is written" do
+      dir = Path.join(System.tmp_dir!(), "hypatia-manifest-#{System.unique_integer([:positive])}")
+      on_exit(fn -> File.rm_rf(dir) end)
+
+      routed = [
+        {:control, pattern("PA006-z")},
+        {:control, Map.delete(pattern("ignored"), "id")},
+        {:eliminate, @eliminate_recipe, pattern("unknown")}
+      ]
+
+      assert {:error, {:factless_steps, steps}} = DispatchManifest.compile(routed)
+
+      assert [%{"step" => 1, "tier" => "control"}, %{"step" => 2, "tier" => "eliminate"}] =
+               steps
+
+      assert {:error, {:factless_steps, ^steps}} =
+               DispatchManifest.write(routed, dispatch_dir: dir)
+
+      refute File.exists?(Path.join(dir, "pending.jsonl"))
+    end
+  end
+
+  # The fleet must never receive a step the manifest refuses (HYP-01).
+  describe "PatternAnalyzer.dispatch_and_write/2" do
+    setup do
+      dir = Path.join(System.tmp_dir!(), "hypatia-dispatch-#{System.unique_integer([:positive])}")
+      on_exit(fn -> File.rm_rf(dir) end)
+      test_pid = self()
+      {:ok, dir: dir, dispatch: fn action -> send(test_pid, {:dispatched, action}) end}
+    end
+
+    test "a factless step dispatches nothing and writes nothing", %{dir: dir, dispatch: dispatch} do
+      routed = [
+        {:control, %{"id" => "PA006-z", "severity" => "High"}},
+        {:control, %{"severity" => "High"}}
+      ]
+
+      assert {nil, %{total: 0, refused: {:factless_steps, [%{"step" => 1}]}}} =
+               Hypatia.PatternAnalyzer.dispatch_and_write(routed,
+                 dispatch: dispatch,
+                 dispatch_dir: dir
+               )
+
+      refute_received {:dispatched, _}
+      refute File.exists?(Path.join(dir, "pending.jsonl"))
+    end
+
+    test "negative control: when every step names its fact, every action is dispatched",
+         %{dir: dir, dispatch: dispatch} do
+      routed = [
+        {:control, %{"id" => "PA006-z", "severity" => "High"}},
+        {:control, %{"id" => "PA007-w", "severity" => "High"}}
+      ]
+
+      assert {path, %{total: 2}} =
+               Hypatia.PatternAnalyzer.dispatch_and_write(routed,
+                 dispatch: dispatch,
+                 dispatch_dir: dir
+               )
+
+      assert File.exists?(path)
+      assert_received {:dispatched, {:control, %{"id" => "PA006-z"}}}
+      assert_received {:dispatched, {:control, %{"id" => "PA007-w"}}}
+    end
+  end
 end
diff --git a/test/retraction_test.exs b/test/retraction_test.exs
new file mode 100644
index 00000000..e5431abe
--- /dev/null
+++ b/test/retraction_test.exs
@@ -0,0 +1,195 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+defmodule Hypatia.RetractionTest do
+  @moduledoc """
+  HYP-01: quarantine is retraction.
+
+  The specification is residual-evidence-types' Revision.agda
+  (`survives-retraction`, `survives-dependent`), transcribed in
+  `src/Hypatia/ABI/Retraction.idr`; the Idris positive control
+  `tests/accept/IndependentTokenSurvives.idr` and expected rejection
+  `tests/reject/RetractedSupportSurvives.idr` are the same cases run here
+  through the runtime mirror.
+  """
+
+  # Quarantine is a named GenServer shared by the whole suite.
+  use ExUnit.Case, async: false
+
+  alias Hypatia.Safety.Quarantine
+  alias Hypatia.Verdict
+  alias Hypatia.Verdict.Retraction
+
+  defp finding(rules, opts \\ []) do
+    %{
+      rule_module: "code_safety",
+      type: "x",
+      file: "src/a.rs",
+      line: 3,
+      severity: "high",
+      reason: "r",
+      action: "flag",
+      evidence:
+        Enum.map(rules, fn rule ->
+          %{
+            rule: rule,
+            rule_version: Verdict.rule_version(),
+            span: %{file: "src/a.rs", start_line: 3, end_line: 3},
+            observations: 1
+          }
+          |> then(&if(bot = opts[:bot], do: Map.put(&1, :bot, bot), else: &1))
+        end)
+    }
+    |> Verdict.annotate()
+  end
+
+  describe "Retraction.retract/2 (pure)" do
+    test "a finding resting only on the retracted rule is retracted (RetractedSupportSurvives)" do
+      f = finding(["code_safety/rule_a"])
+
+      assert {[], [gone]} = Retraction.retract([f], [{:rule, "code_safety/rule_a"}])
+      assert gone.retracted_by == ["rule:code_safety/rule_a"]
+      # The original evidence is kept for audit, not erased.
+      assert gone.evidence == f.evidence
+    end
+
+    test "a finding corroborated by another rule survives through it (IndependentTokenSurvives)" do
+      f = finding(["code_safety/rule_a", "code_safety/rule_b"])
+
+      assert {[kept], []} = Retraction.retract([f], [{:rule, "code_safety/rule_a"}])
+      assert [%{rule: "code_safety/rule_b"}] = kept.evidence
+      assert [%{rule: "code_safety/rule_a"}] = kept.retracted_evidence
+      assert kept.level == "epi"
+    end
+
+    test "negative control: a finding that does not rest on the retracted rule is untouched" do
+      f = finding(["code_safety/rule_b"])
+      assert {[^f], []} = Retraction.retract([f], [{:rule, "code_safety/rule_a"}])
+    end
+
+    test "a token rests on its bot as well as its rule" do
+      f = finding(["code_safety/rule_a"], bot: "panicbot")
+
+      assert {[], [gone]} = Retraction.retract([f], [{:bot, "panicbot"}])
+      assert gone.retracted_by == ["bot:panicbot"]
+
+      assert {[^f], []} = Retraction.retract([f], [{:bot, "rhodibot"}])
+    end
+
+    test "a confirming re-check survives the quarantine of the rule that flagged it" do
+      sound =
+        finding(["code_safety/sorry"])
+        |> Map.put(:support, %{
+          kind: "mechanical",
+          prover: "lean4",
+          prover_version: "4.30.0",
+          target: "t.lean",
+          target_sha256: String.duplicate("a", 64),
+          artefact_sha256: String.duplicate("b", 64),
+          result: "confirms"
+        })
+        |> Verdict.annotate()
+
+      assert sound.level == "sound"
+
+      assert {[kept], []} = Retraction.retract([sound], [{:rule, "code_safety/sorry"}])
+      assert kept.evidence == []
+      assert kept.level == "sound"
+
+      # ...but not the quarantine of its prover: then nothing supports it.
+      assert {[], [gone]} =
+               Retraction.retract([sound], [{:rule, "code_safety/sorry"}, {:prover, "lean4"}])
+
+      assert Enum.sort(gone.retracted_by) == ["prover:lean4", "rule:code_safety/sorry"]
+
+      # A retracted prover with a surviving rule leaves a pattern match, at epi.
+      assert {[epi], []} = Retraction.retract([sound], [{:prover, "lean4"}])
+      assert epi.support == %{kind: "pattern"}
+      assert epi.level == "epi"
+      assert epi.retracted_support.kind == "mechanical"
+    end
+
+    test "a refuting re-check never supported the finding, so its prover is never named" do
+      refuted =
+        finding(["code_safety/sorry"])
+        |> Map.put(:support, %{
+          kind: "mechanical",
+          prover: "lean4",
+          prover_version: "4.30.0",
+          target: "t.lean",
+          target_sha256: String.duplicate("a", 64),
+          artefact_sha256: String.duplicate("b", 64),
+          result: "refutes"
+        })
+        |> Verdict.annotate()
+
+      assert refuted.level == "epi"
+
+      # Rule and prover both retracted: the finding rested only on the rule.
+      assert {[], [gone]} =
+               Retraction.retract([refuted], [{:rule, "code_safety/sorry"}, {:prover, "lean4"}])
+
+      assert gone.retracted_by == ["rule:code_safety/sorry"]
+
+      # Only the prover retracted: nothing the finding rested on is gone.
+      assert {[^refuted], []} = Retraction.retract([refuted], [{:prover, "lean4"}])
+    end
+
+    test "retracted_by is JSON-encodable" do
+      assert {[], [gone]} =
+               Retraction.retract([finding(["code_safety/rule_a"])], [
+                 {:rule, "code_safety/rule_a"}
+               ])
+
+      assert {:ok, _} = Jason.encode(gone)
+    end
+
+    test "quarantine keys parse to the assumptions they retract" do
+      assert Retraction.parse("rule:code_safety/sorry") == {:rule, "code_safety/sorry"}
+      assert Retraction.parse("prover:lean4") == {:prover, "lean4"}
+      assert Retraction.parse("rhodibot") == {:bot, "rhodibot"}
+      assert Retraction.name({:rule, "code_safety/sorry"}) == "rule:code_safety/sorry"
+    end
+  end
+
+  describe "Quarantine.retract_dependents/1" do
+    setup do
+      key = "rule:code_safety/retraction_test_#{System.unique_integer([:positive])}"
+      on_exit(fn -> Quarantine.release(key) end)
+      {:ok, key: key, rule: String.replace_prefix(key, "rule:", "")}
+    end
+
+    test "quarantining a rule retracts the findings that rested only on it", %{
+      key: key,
+      rule: rule
+    } do
+      only = finding([rule])
+      both = finding([rule, "code_safety/other"])
+      other = finding(["code_safety/other"])
+
+      # Before the quarantine, nothing is retracted.
+      assert {kept, []} = Quarantine.retract_dependents([only, both, other])
+      assert length(kept) == 3
+
+      Quarantine.quarantine(key, :hard, "retraction test")
+      # quarantine/3 is a cast; a call orders after it.
+      assert Map.has_key?(Quarantine.list_quarantined(), key)
+
+      assert {kept, [gone]} = Quarantine.retract_dependents([only, both, other])
+      assert gone.retracted_by == [key]
+      assert length(kept) == 2
+      assert Enum.all?(kept, &(&1.level == "epi"))
+
+      # Release restores the support: nothing is retracted any more.
+      Quarantine.release(key)
+      refute Map.has_key?(Quarantine.list_quarantined(), key)
+      assert {_, []} = Quarantine.retract_dependents([only, both, other])
+    end
+
+    test "a soft quarantine retracts too", %{key: key, rule: rule} do
+      Quarantine.quarantine(key, :soft, "high false-positive rate")
+      assert Map.has_key?(Quarantine.list_quarantined(), key)
+      assert {[], [_]} = Quarantine.retract_dependents([finding([rule])])
+    end
+  end
+end
diff --git a/tests/accept/IndependentTokenSurvives.idr b/tests/accept/IndependentTokenSurvives.idr
new file mode 100644
index 00000000..81f08e28
--- /dev/null
+++ b/tests/accept/IndependentTokenSurvives.idr
@@ -0,0 +1,50 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- POSITIVE CONTROL (HYP-01).  The counterpart of
+-- tests/reject/RetractedSupportSurvives.idr: a finding corroborated by two
+-- rules survives the quarantine of one of them, through the token of the
+-- other; the token that rested on the quarantined rule does not.
+-- test/retraction_test.exs runs the same case through the runtime mirror
+-- (Hypatia.Verdict.Retraction).
+
+module IndependentTokenSurvives
+
+import Data.List.Elem
+import Hypatia.ABI.Retraction
+
+%default total
+%unbound_implicits off
+
+ruleA : Assumption
+ruleA = RuleA "code_safety/rule_a"
+
+ruleB : Assumption
+ruleB = RuleA "code_safety/rule_b"
+
+ctx : List Assumption
+ctx = [ruleA, ruleB]
+
+-- Quarantining rule A retracts the first assumption.
+quarantineA : Retraction IndependentTokenSurvives.ctx [ruleB]
+quarantineA = First
+
+tokenA : Dependent IndependentTokenSurvives.ctx
+tokenA = RestsOn [ruleA] (Keep (Drop Done))
+
+tokenB : Dependent IndependentTokenSurvives.ctx
+tokenB = RestsOn [ruleB] (Drop (Keep Done))
+
+-- The finding survives, through token B.
+findingSurvives : AnySurvives [ruleB] [tokenA, tokenB]
+findingSurvives = ThereS (HereS (Keep Done))
+
+-- What it survives by is token B's support, now under the retracted context.
+survivesByB : support (survivor IndependentTokenSurvives.quarantineA IndependentTokenSurvives.findingSurvives) = [ruleB]
+survivesByB = Refl
+
+-- Token A does not survive: rule A is gone from [ruleB].
+tokenADies : Not (Thin [ruleA] [ruleB])
+tokenADies = retractedSupportDies Here (\e => case e of
+  Here impossible
+  There e' impossible)
diff --git a/tests/reject/RetractedSupportSurvives.idr b/tests/reject/RetractedSupportSurvives.idr
new file mode 100644
index 00000000..3dfe6fe8
--- /dev/null
+++ b/tests/reject/RetractedSupportSurvives.idr
@@ -0,0 +1,31 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- EXPECTED REJECTION (HYP-01).  scripts/check-verdicts.sh passes only if
+-- Idris2 refuses this module, and only at the declaration `invalid`.  Every
+-- other declaration must typecheck, so that the refusal is for the stated
+-- reason and not for a missing import or a typo.
+--
+-- Must fail: quarantining the rule retracts the only assumption the token
+-- rests on, so its support [rule] does not thin into the empty context and
+-- the token cannot survive (residual-evidence-types tests/reject/
+-- FalseRetraction, transcribed).
+--
+-- EXPECT: Mismatch between: [?x] and [].
+
+module RetractedSupportSurvives
+
+import Hypatia.ABI.Retraction
+
+%default total
+%unbound_implicits off
+
+rule : Assumption
+rule = RuleA "code_safety/example_rule"
+
+-- The token rests on the rule that fired.
+token : Dependent [rule]
+token = RestsOn [rule] (Keep Done)
+
+invalid : Dependent []
+invalid = survivesDependent (First {x = rule} {g = []}) token (Keep Done)
diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index 5a62f461..53e33165 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -181,6 +181,47 @@ correspondence is a transcription, not a checked proof |ASSUMED
 |`+src/Hypatia/ABI/Verdict.idr+` |Idris2 |Elixir rules carry a proof of
 their support tag. They carry the tag only (HYP-01, PR B); no Elixir rule
 is proved sound |OPEN
+
+|`+src/Hypatia/ABI/Retraction.idr+` |Idris2 |Quarantine as retraction:
+a retraction is a thinning (`+retractThin+`); a token whose support thins
+into the retracted context survives on the same support
+(`+survivesDependent+`); a support naming an assumption that no longer
+occurs does not (`+thinElem+`, `+retractedSupportDies+`); a finding
+survives exactly through one of its tokens (`+survivor+`,
+`+noTokensNoSurvival+`) |PROVEN
+
+|`+tests/reject/RetractedSupportSurvives.idr+` |Idris2 |Expected
+rejection: a token resting on the very rule a quarantine retracts is
+refused as surviving, at `+invalid+` |TESTED
+
+|`+tests/accept/IndependentTokenSurvives.idr+` |Idris2 |Positive
+control: a finding corroborated by two rules survives the quarantine of
+one through the other (`+findingSurvives+`, `+survivesByB+`), and the
+token that rested on the quarantined rule does not (`+tokenADies+`)
+|TESTED
+
+|`+src/Hypatia/ABI/Retraction.idr+` |Idris2 |Correspondence of
+`+Retraction+`, `+Dependent+`, `+survivesDependent+` to Revision.agda in
+hyperpolymath/residual-evidence-types @ 97244f5. Pin and names checked
+(`+sibling-citations+` CI job); transcription, not a checked proof
+|ASSUMED
+
+|Runtime mirror, lib/hypatia/verdict/retraction.ex |Elixir |Quarantine
+retracts the findings that rested only on a quarantined rule, bot or
+prover, keeps corroborated findings on their surviving tokens, and
+restores them on release: test/retraction_test.exs, with the
+untouched-finding negative control and two mutants killed |TESTED
+
+|Runtime wiring |Elixir |`Quarantine.retract_dependents/1` is called by
+a scan or dispatch path. It is not, like the rest of the safety systems
+(CLAUDE.md Known Gap 2) |OPEN
+
+|Derived workflow steps, lib/dispatch_manifest.ex |Elixir |Every
+dispatch-manifest step names the verdict it derives from, and a factless
+step refuses the whole manifest before anything is written:
+test/dispatch_manifest_test.exs. This is hypatia's own derived workflow;
+the Signalbox criterion has no Signalbox repository to apply to |TESTED
+(Signalbox: OPEN)
 |===
 
 === Properties Proven