diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index a081d4d6..6aa2e6fb 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                       # 133 Elixir modules total
+Hypatia                       # 140 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
@@ -122,6 +122,7 @@ OutcomeTracker.record_outcome()         -- Feedback loop
 | `scorecard_ingestor.ex` | Ingests 20 OpenSSF Scorecard checks as local scan patterns |
 | `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`) |
 | `application.ex` | OTP Application supervisor for all GenServers |
 
 ### VCL Query Layer (lib/vcl/)
diff --git a/.github/workflows/escript-soundness.yml b/.github/workflows/escript-soundness.yml
index 20bc2afc..d78e59be 100644
--- a/.github/workflows/escript-soundness.yml
+++ b/.github/workflows/escript-soundness.yml
@@ -85,7 +85,7 @@ jobs:
       - name: Install jq
         run: |
           apt-get update -qq
-          apt-get install -y -qq jq git
+          apt-get install -y -qq jq git curl
 
       - name: Fetch source at the exact commit under test
         run: |
@@ -162,3 +162,26 @@ jobs:
             exit 1
           fi
           echo "Consumer-shaped invocation produced $(jq 'length' consumer.json) findings."
+
+      # HYP-01: every finding in CI output names its support. The schema's
+      # self-test runs first, so a schema that accepts everything cannot
+      # pass: it must refuse a pattern finding that claims "sound" (and six
+      # other bad shapes in test/fixtures/findings-schema/). Then the real
+      # consumer-shaped output above must satisfy schema/findings.ncl, whose
+      # LevelDerived contract re-derives every finding's level.
+      - name: Findings carry support, evidence and a derived level
+        working-directory: source
+        env:
+          NICKEL_VERSION: 1.11.0
+          NICKEL_SHA256: d40cd32b8374636fda8939a8e479616c7a1db57acb5ef5a9621e242ed8f5a361
+        run: |
+          set -euo pipefail
+          mkdir -p "$HOME/.local/bin"
+          curl -fsSL -o "$HOME/.local/bin/nickel" \
+            "https://github.com/tweag/nickel/releases/download/${NICKEL_VERSION}/nickel-x86_64-linux"
+          echo "${NICKEL_SHA256}  $HOME/.local/bin/nickel" | sha256sum -c -
+          chmod +x "$HOME/.local/bin/nickel"
+          export NICKEL="$HOME/.local/bin/nickel"
+          "$NICKEL" --version
+          bash scripts/check-findings-schema.sh --self-test
+          bash scripts/check-findings-schema.sh consumer.json
diff --git a/hypatia-cli-bash.sh b/hypatia-cli-bash.sh
index 653ea088..9b2712c8 100755
--- a/hypatia-cli-bash.sh
+++ b/hypatia-cli-bash.sh
@@ -77,6 +77,14 @@ FINDINGS_FILE=""
 FINDING_COUNT=0
 FIRST_FINDING=true
 
+# The level a finding is reported at, derived from its support and evidence
+# (Hypatia.Verdict.level/2; schema/findings.ncl derive_level): sound only for a
+# mechanical re-check that confirms, epi with evidence, belief without.
+VERDICT_LEVEL_JQ='def verdict_level:
+  if .support.kind == "mechanical" and .support.result == "confirms" then "sound"
+  elif (.evidence | length) > 0 then "epi"
+  else "belief" end;'
+
 init_findings() {
     FINDINGS_FILE=$(mktemp /tmp/hypatia-findings-XXXXXX.json)
     echo "[" > "$FINDINGS_FILE"
@@ -94,12 +102,22 @@ emit_finding() {
     [[ "$FIRST_FINDING" == "false" ]] && echo "," >> "$FINDINGS_FILE"
     FIRST_FINDING=false
 
+    # HYP-01: every finding names its support (schema/findings.ncl). A regex
+    # match is `pattern` support with one evidence token; `level` is derived
+    # by the same rule as Hypatia.Verdict.level/2, never written by hand.
     jq -n \
         --arg sev "$sev" --arg type "$type" --arg pattern "$pattern" \
         --arg file "$file" --argjson line "$line" --arg code "$code" \
         --arg cwe "$cwe" --arg fix "$fix" --argjson auto "$([ "$auto_fixable" = "true" ] && echo true || echo false)" \
-        '{severity:$sev, type:$type, pattern:$pattern, file:$file,
-          line:$line, code:$code, cwe:$cwe, fix:$fix, auto_fixable:$auto}' \
+        --arg version "$VERSION" \
+        "${VERDICT_LEVEL_JQ}"'
+        {severity:$sev, type:$type, pattern:$pattern, file:$file,
+          line:$line, code:$code, cwe:$cwe, fix:$fix, auto_fixable:$auto,
+          support:{kind:"pattern"},
+          evidence:[{rule:("bash/" + $pattern), rule_version:$version,
+                     span:{file:$file, start_line:$line, end_line:$line},
+                     observations:1}]}
+        | . + {level: verdict_level}' \
         >> "$FINDINGS_FILE"
 
     ((FINDING_COUNT++)) || true
@@ -923,7 +941,7 @@ scan_directory() {
               findings: $findings}'
     elif [[ "$format" == "github" ]]; then
         jq -r '.[] | select(. != {}) |
-            "::\(.severity) file=\(.file),line=\(.line)::\(.pattern) - \(.fix)"' \
+            "::\(.severity) file=\(.file),line=\(.line)::\(.pattern) - \(.fix) [\(.level): \(.support.kind)]"' \
             "$FINDINGS_FILE"
     else
         # Summary header
@@ -946,7 +964,7 @@ scan_directory() {
 
         # Group by type for readability
         jq -r '.[] | select(. != {}) |
-            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern))\n  \(.fix)\n"' \
+            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern); \(.level): \(.support.kind))\n  \(.fix)\n"' \
             "$FINDINGS_FILE"
     fi
 
@@ -989,7 +1007,7 @@ scan_file() {
         echo "$filtered"
     else
         echo "$filtered" | jq -r '.[] |
-            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern))\n  \(.fix)\n"'
+            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern); \(.level): \(.support.kind))\n  \(.fix)\n"'
     fi
 
     rm -f "$FINDINGS_FILE"
@@ -1064,7 +1082,7 @@ check_staged_files() {
 
     if [[ "$critical" -gt 0 ]]; then
         echo "$filtered" | jq -r '.[] | select(.severity == "critical") |
-            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern))\n  \(.fix)\n"'
+            "[\(.severity | ascii_upcase)] \(.file):\(.line)  (\(.pattern); \(.level): \(.support.kind))\n  \(.fix)\n"'
         log_error "Pre-commit BLOCKED: $critical critical issues in staged files"
         return 1
     elif [[ "$count" -gt 0 ]]; then
diff --git a/lib/hypatia/cli.ex b/lib/hypatia/cli.ex
index 38791bbc..0d06a4f8 100644
--- a/lib/hypatia/cli.ex
+++ b/lib/hypatia/cli.ex
@@ -293,6 +293,17 @@ defmodule Hypatia.CLI do
         "(#{breakdown}); exit #{exit_code}" <>
         if(config.exit_zero and total > 0, do: " (--exit-zero suppressed exit 1)", else: "")
     )
+
+    # A separate line, so the summary above keeps its shape for any caller
+    # that pattern-matches it. Levels are derived (Hypatia.Verdict), never
+    # stored by a rule.
+    levels = Hypatia.Verdict.level_counts(filtered)
+
+    IO.puts(
+      :stderr,
+      "[hypatia] verdict levels: sound=#{levels["sound"]}, epi=#{levels["epi"]}, " <>
+        "belief=#{levels["belief"]}"
+    )
   end
 
   defp env_flag?(name) do
@@ -311,7 +322,9 @@ defmodule Hypatia.CLI do
   @doc """
   Runs the selected rule modules against `repo_path` and returns normalized
   finding maps. Each map includes `rule_module`, `type`, `severity`, `file`,
-  `reason`, and `action`; line-aware findings may also include `line`.
+  `reason`, and `action`; line-aware findings may also include `line`. Every
+  map also carries the HYP-01 verdict fields `support`, `evidence` and the
+  derived `level` (`Hypatia.Verdict`, `schema/findings.ncl`).
   Findings covered by configured suppressions are excluded.
 
   ## Parameters
@@ -983,6 +996,10 @@ defmodule Hypatia.CLI do
         repo_path: repo_path
       )
     end)
+    # HYP-01: every finding names its support. Same funnel, exactly once, so
+    # no rule module can emit a finding without `support`, `evidence` and a
+    # derived `level` (schema/findings.ncl; Hypatia.Verdict).
+    |> Enum.map(&Hypatia.Verdict.annotate/1)
   end
 
   # ─── Code safety scanning ────────────────────────────────────────────
@@ -1223,7 +1240,7 @@ defmodule Hypatia.CLI do
   defp output(findings, "github") do
     # GitHub Actions annotation format
     Enum.each(findings, fn f ->
-      level =
+      annotation =
         case f.severity do
           "critical" -> "error"
           "high" -> "error"
@@ -1234,7 +1251,7 @@ defmodule Hypatia.CLI do
 
       file = Map.get(f, :file, "")
       reason = Map.get(f, :reason, "")
-      IO.puts("::#{level} file=#{file}::#{reason}")
+      IO.puts("::#{annotation} file=#{file}::#{reason} [#{Hypatia.Verdict.describe(f)}]")
     end)
   end
 
@@ -1251,7 +1268,7 @@ defmodule Hypatia.CLI do
         IO.puts(:stderr, "  [#{String.upcase(severity)}] (#{length(group)} findings)")
 
         Enum.each(group, fn f ->
-          IO.puts(:stderr, "    #{f.file}: #{f.reason}")
+          IO.puts(:stderr, "    #{f.file}: #{f.reason} [#{Hypatia.Verdict.describe(f)}]")
         end)
 
         IO.puts(:stderr, "")
diff --git a/lib/hypatia/sarif.ex b/lib/hypatia/sarif.ex
index e2c38593..42a46c67 100644
--- a/lib/hypatia/sarif.ex
+++ b/lib/hypatia/sarif.ex
@@ -130,6 +130,23 @@ defmodule Hypatia.SARIF do
         "partialFingerprints" => %{"hypatiaFindingHash/v1" => fingerprint}
       }
 
+      # HYP-01 verdict fields ride in the SARIF property bag (SARIF 2.1.0
+      # §3.8), outside the fingerprint, so annotating a finding never
+      # re-opens an alert code scanning has already triaged.
+      result =
+        case Map.get(finding, :level) || Map.get(finding, "level") do
+          nil ->
+            result
+
+          verdict_level ->
+            support = Map.get(finding, :support) || Map.get(finding, "support") || %{}
+
+            Map.put(result, "properties", %{
+              "hypatia.level" => verdict_level,
+              "hypatia.support" => Map.get(support, :kind) || Map.get(support, "kind")
+            })
+        end
+
       rules =
         Map.put_new(rules, rule_id, %{
           "id" => rule_id,
diff --git a/lib/hypatia/verdict.ex b/lib/hypatia/verdict.ex
new file mode 100644
index 00000000..64239940
--- /dev/null
+++ b/lib/hypatia/verdict.ex
@@ -0,0 +1,179 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+defmodule Hypatia.Verdict do
+  @moduledoc """
+  Every finding names its support (HYP-01).
+
+  The JSON mirror of `src/Hypatia/ABI/Verdict.idr`, which is normative, and of
+  `schema/findings.ncl`, the contract CI validates scan output against. Each
+  finding carries three fields:
+
+    * `support` — what its evidence supports:
+      `%{kind: "pattern"}` (a rule matched),
+      `%{kind: "observed", observations: n}` (a fleet count; rules.a2ml's
+      thresholds are belief formation, not soundness), or
+      `%{kind: "mechanical", ...}` (a prover re-check, with both digests);
+    * `evidence` — the tokens the finding was issued on: rule, rule version,
+      span, observation count;
+    * `level` — derived here and nowhere else: `"sound"` only for a
+      mechanical support whose re-check confirms; `"epi"` for any other
+      support with evidence; `"belief"` with no evidence at all.
+
+  Elixir rules carry the tag only. No rule is proved sound, so the honest
+  default for every rule-module finding is `pattern` / `epi`. The only way to
+  `"sound"` is `attach_recheck/3`, which refuses a re-check whose target is
+  not the finding's file or whose target digest does not match the bytes on
+  disk. It cannot re-run the prover; `scripts/recheck-lean-hole.sh` is the
+  pattern for checking the artefact digest against a fresh run.
+  """
+
+  @rule_version Mix.Project.config()[:version]
+
+  @provers ~w(lean4 idris2 agda coq)
+  @results ~w(confirms refutes)
+
+  @type level :: String.t()
+
+  @doc "The rule version stamped on evidence tokens (the hypatia version)."
+  @spec rule_version() :: String.t()
+  def rule_version, do: @rule_version
+
+  @doc """
+  Attach `support`, `evidence` and the derived `level` to a finding.
+
+  An existing `support` or `evidence` is kept; a `level` is always
+  recomputed, so a rule cannot assert one.
+  """
+  @spec annotate(map()) :: map()
+  def annotate(finding) when is_map(finding) do
+    support = Map.get(finding, :support) || %{kind: "pattern"}
+    evidence = Map.get(finding, :evidence) || [token(finding)]
+
+    finding
+    |> Map.put(:support, support)
+    |> Map.put(:evidence, evidence)
+    |> Map.put(:level, level(support, evidence))
+  end
+
+  @doc """
+  The evidence token a rule-module finding offers: the rule that fired, at
+  this hypatia version, over the finding's line (`0` when the finding is
+  file- or repository-level). `observations` is this scan's own single
+  observation; fleet-wide counts belong in an `observed` support.
+  """
+  @spec token(map()) :: map()
+  def token(finding) do
+    line =
+      case Map.get(finding, :line) do
+        n when is_integer(n) and n >= 0 -> n
+        _ -> 0
+      end
+
+    %{
+      rule: "#{Map.get(finding, :rule_module, "unknown")}/#{Map.get(finding, :type, "unknown")}",
+      rule_version: @rule_version,
+      span: %{file: to_string(Map.get(finding, :file, "")), start_line: line, end_line: line},
+      observations: 1
+    }
+  end
+
+  @doc """
+  Derive the level from support and evidence (`Verdict.idr` `level`;
+  `schema/findings.ncl` `derive_level`).
+  """
+  @spec level(map(), list()) :: level()
+  def level(%{kind: "mechanical", result: "confirms"}, _evidence), do: "sound"
+  def level(_support, [_ | _]), do: "epi"
+  def level(_support, []), do: "belief"
+
+  @doc """
+  Replace a finding's support with a prover re-check, if the re-check is
+  about this finding's file and its target digest matches the file under
+  `repo_path`.
+
+  `recheck` has string values for `:prover`, `:prover_version`, `:target`,
+  `:target_sha256`, `:artefact_sha256` and `:result`. A re-check that
+  `"refutes"` is attached as recorded and derives `"epi"`, not `"sound"`.
+  """
+  @spec attach_recheck(map(), map(), String.t()) :: {:ok, map()} | {:error, term()}
+  def attach_recheck(finding, recheck, repo_path) do
+    with :ok <- check_string(:target, recheck[:target]),
+         :ok <- check_string(:prover_version, recheck[:prover_version]),
+         :ok <- check_member(:prover, recheck[:prover], @provers),
+         :ok <- check_member(:result, recheck[:result], @results),
+         :ok <- check_digest(:target_sha256, recheck[:target_sha256]),
+         :ok <- check_digest(:artefact_sha256, recheck[:artefact_sha256]),
+         :ok <- check_same_target(finding, recheck),
+         {:ok, digest} <- file_sha256(Path.join(repo_path, recheck.target)),
+         :ok <- check_target_digest(digest, recheck.target_sha256) do
+      support =
+        recheck
+        |> Map.take([:prover, :prover_version, :target, :target_sha256, :artefact_sha256, :result])
+        |> Map.put(:kind, "mechanical")
+
+      {:ok, finding |> Map.put(:support, support) |> annotate()}
+    end
+  end
+
+  @doc """
+  One-line rendering of a finding's level and support, for text and
+  GitHub-annotation output. Derived from the record, never stored on it.
+  """
+  @spec describe(map()) :: String.t()
+  def describe(finding) do
+    support = Map.get(finding, :support) || %{kind: "pattern"}
+    evidence = Map.get(finding, :evidence) || []
+
+    basis =
+      case support do
+        %{kind: "mechanical"} = s -> "#{s.prover} #{s.prover_version} re-check #{s.result}"
+        %{kind: "observed", observations: n} -> "observed #{n}x"
+        %{kind: kind} -> to_string(kind)
+      end
+
+    "#{level(support, evidence)}: #{basis}"
+  end
+
+  @doc "Count findings by level, every level present (for the scan summary)."
+  @spec level_counts([map()]) :: %{level() => non_neg_integer()}
+  def level_counts(findings) do
+    Enum.reduce(findings, %{"sound" => 0, "epi" => 0, "belief" => 0}, fn f, acc ->
+      Map.update(acc, Map.get(f, :level, "belief"), 1, &(&1 + 1))
+    end)
+  end
+
+  defp check_string(field, value) do
+    if is_binary(value) and value != "", do: :ok, else: {:error, {:invalid, field, value}}
+  end
+
+  defp check_member(field, value, allowed) do
+    if value in allowed, do: :ok, else: {:error, {:invalid, field, value}}
+  end
+
+  defp check_digest(field, value) do
+    if is_binary(value) and value =~ ~r/\A[0-9a-f]{64}\z/,
+      do: :ok,
+      else: {:error, {:invalid, field, value}}
+  end
+
+  defp check_same_target(finding, recheck) do
+    if Path.expand(to_string(Map.get(finding, :file, "")), "/") ==
+         Path.expand(recheck.target, "/"),
+       do: :ok,
+       else: {:error, {:target_mismatch, Map.get(finding, :file), recheck.target}}
+  end
+
+  defp file_sha256(path) do
+    case File.read(path) do
+      {:ok, bytes} -> {:ok, :crypto.hash(:sha256, bytes) |> Base.encode16(case: :lower)}
+      {:error, reason} -> {:error, {:unreadable_target, path, reason}}
+    end
+  end
+
+  defp check_target_digest(actual, recorded) do
+    if actual == recorded,
+      do: :ok,
+      else: {:error, {:target_digest_mismatch, actual, recorded}}
+  end
+end
diff --git a/schema/README.adoc b/schema/README.adoc
index 808d0c12..cf56b2e5 100644
--- a/schema/README.adoc
+++ b/schema/README.adoc
@@ -1,12 +1,59 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
-= schema/ — Nickel Schema Files
+= schema/ — Findings schema (canonical)
 
-Nickel configuration schemas for Hypatia data structures.
+`schema/` is the canonical home of the *findings* schema (ruling 2026-10-14,
+HYP-01). `schemas/` holds unrelated contracts — the ruleset JSON Schema, the
+conflow `config.cue`, the Dragonfly cache layout — and no findings schema.
+Merging the two directories is a separate piece of work.
 
 == Files
 
-* `findings.ncl` — Schema for finding records emitted by the rules engine
-* `generate-findings.ncl` — Generator helpers for findings in tests and tooling
+* `findings.ncl` — the Nickel contract for what a scan emits: the escript's
+  JSON array (`Findings`) and the bash fallback's report (`BashReport`).
 
-These schemas are used for configuration validation and test fixture generation.
-The authoritative type definitions are in `src/Hypatia/ABI/Types.idr`.
+== The verdict fields
+
+Every finding carries three fields whose meaning is fixed by
+`src/Hypatia/ABI/Verdict.idr` (normative) and mirrored by
+`lib/hypatia/verdict.ex` and `hypatia-cli-bash.sh`:
+
+[cols="1,4"]
+|===
+|Field |Meaning
+
+|`support`
+|What the evidence supports. `pattern`: a rule matched. `observed`: a fleet
+observation count (the rules.a2ml thresholds, 5 to propose and 10 + 3 fixes to
+auto-approve, are belief-formation rules, not soundness proofs). `mechanical`:
+a prover re-checked the flagged file, with both digests recorded.
+
+|`evidence`
+|The tokens the finding was issued on: rule, rule version, span, observation
+count.
+
+|`level`
+|Derived, never written by a rule. `sound` only for a `mechanical` support
+whose re-check `confirms`; `epi` for any other support with evidence;
+`belief` with no evidence at all. The `LevelDerived` contract re-derives it
+and refuses a finding whose stored level disagrees.
+|===
+
+Today every rule-module finding is `pattern` / `epi`: Elixir rules carry the
+support tag, not a proof. `sound` is reachable only through
+`Hypatia.Verdict.attach_recheck/3`, and no scan path attaches a re-check yet.
+
+All records are open, so the fields are additive: consumers that read
+findings by key (the gitbot-fleet scripts, `.hypatia-baseline.json`
+matching) are unaffected.
+
+== Checking
+
+[source,bash]
+----
+scripts/check-findings-schema.sh --self-test         # fixtures in test/fixtures/findings-schema/
+scripts/check-findings-schema.sh findings.json       # escript output
+scripts/check-findings-schema.sh --bash report.json  # bash fallback output
+----
+
+CI runs the self-test and then validates the repository's own
+consumer-shaped scan (`escript-soundness.yml`, Nickel 1.11.0, SHA-256 pinned).
diff --git a/schema/findings.ncl b/schema/findings.ncl
index 9155f3d1..69f80dcb 100644
--- a/schema/findings.ncl
+++ b/schema/findings.ncl
@@ -1,76 +1,184 @@
 # SPDX-License-Identifier: MPL-2.0
-# Hypatia Security Findings Schema
-# Type-safe schema for scanner output
-
-let Severity = [| 'critical, 'high, 'medium, 'low, 'advisory |] in
-let FindingType = [|
-  'unsafe_crash,
-  'unsafe_panic,
-  'type_safety_bypass,
-  'cors_misconfiguration,
-  'auth_bypass,
-  'unverified_data,
-|] in
-
-let Finding = {
-  severity | Severity,
-  type | FindingType,
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Hypatia findings schema — the canonical contract for what a scan emits.
+#
+# Two producers, two envelopes, one verdict shape:
+#   * the escript (`hypatia-cli.sh scan --format json`) prints a bare array
+#     of `Finding`;
+#   * the bash fallback (hypatia-cli-bash.sh) prints a `BashReport`: an
+#     object with `submission_metadata` and an array of `BashFinding`.
+# Both carry the HYP-01 verdict fields — `support`, `evidence`, `level` —
+# whose meaning is fixed by src/Hypatia/ABI/Verdict.idr (the Idris2 ABI is
+# normative; this file mirrors it for JSON).
+#
+# Every record is open (`..`): consumers that read fields by name (the
+# gitbot-fleet scripts, .hypatia-baseline.json matching) are unaffected by
+# the verdict fields, and later additive fields do not break this contract.
+#
+# `level` is not free text.  `LevelDerived` re-derives it from `support` and
+# `evidence` and refuses a record whose stored level disagrees:
+#   sound  — support is `mechanical` and its re-check `confirms`;
+#   epi    — any other support, with at least one evidence token;
+#   belief — no evidence token at all (a Bayesian posterior alone).
+# A pattern match therefore can never be reported "sound".
+#
+# Check a file:  scripts/check-findings-schema.sh <findings.json>
+
+let one_of = fun allowed =>
+  std.contract.from_predicate (fun value => std.array.elem value allowed)
+in
+
+let severity_c = one_of ["critical", "high", "medium", "low", "info"] in
+
+let level_c = one_of ["sound", "epi", "belief"] in
+
+let sha256_c =
+  std.contract.from_predicate (fun s =>
+    std.is_string s && std.string.is_match "^[0-9a-f]{64}$" s)
+in
+
+let nat_c =
+  std.contract.from_predicate (fun n =>
+    std.is_number n && std.number.is_integer n && n >= 0)
+in
+
+# Some rule modules emit `"line": null` for file- or repo-level findings.
+let line_c =
+  std.contract.from_predicate (fun n =>
+    n == null || (std.is_number n && std.number.is_integer n && n >= 0))
+in
+
+# What a verdict's evidence supports (Verdict.idr `Support`).
+#   pattern    — a pattern matched: evidence that the pattern matched, and
+#                nothing more.
+#   observed   — the finding has been observed `observations` times across
+#                the fleet.  rules.a2ml proposes a rule at 5 observations and
+#                auto-approves at 10 + 3 successful fixes; those thresholds
+#                are BELIEF-FORMATION rules, not soundness proofs, and no
+#                count makes a finding sound.
+#   mechanical — a prover re-checked the flagged file; both digests are
+#                recorded so the re-check can be repeated and compared.
+let support_c =
+  std.contract.custom (fun label value =>
+    if !(std.is_record value) || !(std.record.has_field "kind" value) then
+      'Error { message = "support must be a record with a `kind` field" }
+    else if value.kind == "pattern" then
+      'Ok value
+    else if value.kind == "observed" then
+      'Ok (value | { kind | String, observations | nat_c, .. })
+    else if value.kind == "mechanical" then
+      'Ok (
+        value
+        | {
+          kind | String,
+          prover | one_of ["lean4", "idris2", "agda", "coq"],
+          prover_version | String,
+          target | String,
+          target_sha256 | sha256_c,
+          artefact_sha256 | sha256_c,
+          result | one_of ["confirms", "refutes"],
+          ..
+        }
+      )
+    else
+      'Error { message = "support.kind must be pattern, observed or mechanical" })
+in
+
+# One piece of evidence a rule offered (Verdict.idr `EvidenceToken`).
+let evidence_token_c = {
+  rule | String,
+  rule_version | String,
+  span | { file | String, start_line | nat_c, end_line | nat_c, .. },
+  observations | nat_c,
+  ..
+}
+in
+
+let derive_level_fn = fun support evidence =>
+  if support.kind == "mechanical" && support.result == "confirms" then
+    "sound"
+  else if std.array.length evidence > 0 then
+    "epi"
+  else
+    "belief"
+in
+
+let verdict_fields_c = {
+  support | support_c,
+  evidence | Array evidence_token_c,
+  level | level_c,
+  ..
+}
+in
+
+# `LevelDerived`: the stored level must be the derived one.
+let level_derived_c =
+  std.contract.custom (fun label value =>
+    let expected = derive_level_fn value.support value.evidence in
+    if value.level == expected then
+      'Ok value
+    else
+      'Error {
+        message = "level is \"%{value.level}\" but support and evidence derive \"%{expected}\"",
+      })
+in
+
+# A finding as the escript emits it.
+let escript_fields_c = {
+  rule_module | String,
+  type | String,
+  severity | severity_c,
+  file | String,
+  line | line_c | optional,
+  reason | String,
+  action | String,
+  ..
+}
+in
+
+# A finding as the bash fallback emits it.
+let bash_fields_c = {
+  severity | severity_c,
+  type | String,
   pattern | String,
   file | String,
-  line | Number,
+  line | nat_c,
   code | String,
   cwe | String,
   fix | String,
-} in
+  auto_fixable | Bool,
+  ..
+}
+in
 
-let ScanInfo = {
-  timestamp | String,
-  repository | String,
-  scanner_version | String,
-  scanned_files | Number,
-  total_findings | Number,
-} in
+let finding_c = std.contract.Sequence [escript_fields_c, verdict_fields_c, level_derived_c] in
 
-let FindingsReport = {
-  scan_info | ScanInfo,
-  findings | Array Finding,
-} in
+let bash_finding_c = std.contract.Sequence [bash_fields_c, verdict_fields_c, level_derived_c] in
 
 {
-  # Schema exports
-  Severity,
-  FindingType,
-  Finding,
-  ScanInfo,
-  FindingsReport,
-
-  # Helper function to create a finding
-  make_finding = fun severity type pattern file line code cwe fix =>
-    {
-      severity = severity,
-      type = type,
-      pattern = pattern,
-      file = file,
-      line = line,
-      code = code,
-      cwe = cwe,
-      fix = fix,
-    } | Finding,
-
-  # Helper to create scan info
-  make_scan_info = fun timestamp repository version files count =>
-    {
-      timestamp = timestamp,
-      repository = repository,
-      scanner_version = version,
-      scanned_files = files,
-      total_findings = count,
-    } | ScanInfo,
-
-  # Helper to create complete report
-  make_report = fun scan_info findings =>
-    {
-      scan_info = scan_info,
-      findings = findings,
-    } | FindingsReport,
+  Severity = severity_c,
+  Level = level_c,
+  Support = support_c,
+  EvidenceToken = evidence_token_c,
+  Finding = finding_c,
+  BashFinding = bash_finding_c,
+  derive_level = derive_level_fn,
+
+  # `hypatia-cli.sh scan --format json` (escript).
+  Findings = Array finding_c,
+
+  # `hypatia-cli-bash.sh scan --format json`.
+  BashReport = {
+    submission_metadata | {
+      repo | String,
+      timestamp | String,
+      scanner | String,
+      version | String,
+      finding_count | nat_c,
+      ..
+    },
+    findings | Array bash_finding_c,
+    ..
+  },
 }
diff --git a/schema/generate-findings.ncl b/schema/generate-findings.ncl
deleted file mode 100644
index 6d48d3ac..00000000
--- a/schema/generate-findings.ncl
+++ /dev/null
@@ -1,21 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# Hypatia Findings Generator
-# Generates type-safe JSON from scanner patterns
-
-let schema = import "findings.ncl" in
-
-# This will be populated by the bash scanner
-# Format: array of finding objects
-let findings_data | Array schema.Finding = std.deserialize 'Json in
-
-# Scan metadata (will be provided via environment)
-let scan_info = schema.make_scan_info
-  (std.string.from_enum (std.env.HYPATIA_TIMESTAMP))
-  (std.string.from_enum (std.env.HYPATIA_REPOSITORY))
-  "0.1.0"  # Scanner version
-  (std.string.to_number (std.string.from_enum (std.env.HYPATIA_FILES_SCANNED)))
-  (std.array.length findings_data)
-in
-
-# Generate complete report
-schema.make_report scan_info findings_data
diff --git a/scripts/check-findings-schema.sh b/scripts/check-findings-schema.sh
new file mode 100755
index 00000000..a45080cd
--- /dev/null
+++ b/scripts/check-findings-schema.sh
@@ -0,0 +1,107 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-findings-schema.sh — validate scan output against schema/findings.ncl.
+#
+#   scripts/check-findings-schema.sh <findings.json>          escript array
+#   scripts/check-findings-schema.sh --bash <report.json>     bash fallback
+#   scripts/check-findings-schema.sh --self-test              fixtures
+#
+# `nickel export` serialises the whole value, which forces every lazy
+# contract, so a pass means every finding carries `support`, `evidence` and a
+# `level` that agrees with them (schema/findings.ncl `LevelDerived`).
+#
+# --self-test runs the schema over test/fixtures/findings-schema/: every
+# `good-*` file must be accepted and every `bad-*` file refused, each with the
+# message its sidecar `<name>.expect` names — so a schema that accepts
+# everything cannot pass.
+#
+# Env:  NICKEL (default: nickel)
+# Exit: 0 = valid; 1 = invalid / a control misbehaved; 2 = usage/IO.
+
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 2
+
+nickel="${NICKEL:-nickel}"
+work=_build/check-findings-schema
+mkdir -p "$work"
+schema="$PWD/schema/findings.ncl"
+
+# validate <contract> <json-file> <log>  — 0 if the file satisfies the contract
+validate() {
+  local contract=$1 json=$2 log=$3 abs
+  abs="$(cd -- "$(dirname -- "$json")" && pwd)/$(basename -- "$json")"
+  printf 'let s = import "%s" in (import "%s") | s.%s\n' "$schema" "$abs" "$contract" \
+    >"$work/check.ncl"
+  "$nickel" export --format json "$work/check.ncl" >/dev/null 2>"$log"
+}
+
+contract_for() {
+  case "$(basename -- "$1")" in
+    *bash*) echo BashReport ;;
+    *) echo Findings ;;
+  esac
+}
+
+case "${1:-}" in
+  --self-test)
+    dir=test/fixtures/findings-schema
+    shopt -s nullglob
+    goods=("$dir"/good-*.json)
+    bads=("$dir"/bad-*.json)
+    shopt -u nullglob
+    if (( ${#goods[@]} == 0 || ${#bads[@]} == 0 )); then
+      echo "ERROR: $dir needs both good-*.json and bad-*.json fixtures" >&2
+      exit 1
+    fi
+    for f in "${goods[@]}"; do
+      log="$work/$(basename -- "$f" .json).log"
+      if ! validate "$(contract_for "$f")" "$f" "$log"; then
+        cat "$log"
+        echo "ERROR: schema refused valid fixture $f" >&2
+        exit 1
+      fi
+      echo "PASS: accepted $f"
+    done
+    for f in "${bads[@]}"; do
+      log="$work/$(basename -- "$f" .json).log"
+      expect_file="${f%.json}.expect"
+      [[ -f "$expect_file" ]] || { echo "ERROR: $f has no ${expect_file}" >&2; exit 1; }
+      expect="$(head -1 "$expect_file")"
+      if validate "$(contract_for "$f")" "$f" "$log"; then
+        echo "ERROR: schema accepted invalid fixture $f" >&2
+        exit 1
+      fi
+      if ! grep -qF -- "$expect" "$log" || grep -q 'error: import of' "$log"; then
+        cat "$log"
+        echo "ERROR: $f refused for the wrong reason (want: $expect)" >&2
+        exit 1
+      fi
+      echo "PASS: refused $f: $expect"
+    done
+    echo "PASS: findings schema self-test, ${#goods[@]} accepted, ${#bads[@]} refused"
+    ;;
+  --bash)
+    [[ -f "${2:-}" ]] || { echo "usage: $0 --bash <report.json>" >&2; exit 2; }
+    if ! validate BashReport "$2" "$work/bash.log"; then
+      cat "$work/bash.log"
+      echo "ERROR: $2 does not satisfy schema/findings.ncl BashReport" >&2
+      exit 1
+    fi
+    echo "PASS: $2 satisfies BashReport ($(jq '.findings | length' "$2") findings)"
+    ;;
+  "" | -*)
+    echo "usage: $0 <findings.json> | --bash <report.json> | --self-test" >&2
+    exit 2
+    ;;
+  *)
+    [[ -f "$1" ]] || { echo "ERROR: $1 not found" >&2; exit 2; }
+    if ! validate Findings "$1" "$work/findings.log"; then
+      cat "$work/findings.log"
+      echo "ERROR: $1 does not satisfy schema/findings.ncl Findings" >&2
+      exit 1
+    fi
+    echo "PASS: $1 satisfies Findings ($(jq 'length' "$1") findings; by level: $(jq -c 'group_by(.level) | map({(.[0].level): length}) | add // {}' "$1"))"
+    ;;
+esac
diff --git a/test/fixtures/findings-schema/bad-belief-with-evidence.expect b/test/fixtures/findings-schema/bad-belief-with-evidence.expect
new file mode 100644
index 00000000..cc3f94cc
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-belief-with-evidence.expect
@@ -0,0 +1 @@
+level is "belief" but support and evidence derive "epi"
diff --git a/test/fixtures/findings-schema/bad-belief-with-evidence.json b/test/fixtures/findings-schema/bad-belief-with-evidence.json
new file mode 100644
index 00000000..01116f79
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-belief-with-evidence.json
@@ -0,0 +1,27 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "pattern"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "belief"
+  }
+]
diff --git a/test/fixtures/findings-schema/bad-malformed-digest.expect b/test/fixtures/findings-schema/bad-malformed-digest.expect
new file mode 100644
index 00000000..50d166a1
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-malformed-digest.expect
@@ -0,0 +1 @@
+contract broken by the value of `artefact_sha256`
diff --git a/test/fixtures/findings-schema/bad-malformed-digest.json b/test/fixtures/findings-schema/bad-malformed-digest.json
new file mode 100644
index 00000000..f44ba6c6
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-malformed-digest.json
@@ -0,0 +1,33 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "mechanical",
+      "prover": "lean4",
+      "prover_version": "4.30.0",
+      "target": "src/example.lean",
+      "target_sha256": "5465a2710136d470469e3bc4351c27dd0a6d8a14f520fd7009f5f196351c72e7",
+      "artefact_sha256": "F5D4CF9E",
+      "result": "confirms"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "sound"
+  }
+]
diff --git a/test/fixtures/findings-schema/bad-missing-support.expect b/test/fixtures/findings-schema/bad-missing-support.expect
new file mode 100644
index 00000000..b8bf9563
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-missing-support.expect
@@ -0,0 +1 @@
+missing definition for `support`
diff --git a/test/fixtures/findings-schema/bad-missing-support.json b/test/fixtures/findings-schema/bad-missing-support.json
new file mode 100644
index 00000000..259cb239
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-missing-support.json
@@ -0,0 +1,24 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "epi"
+  }
+]
diff --git a/test/fixtures/findings-schema/bad-observed-sound.expect b/test/fixtures/findings-schema/bad-observed-sound.expect
new file mode 100644
index 00000000..7c58e70a
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-observed-sound.expect
@@ -0,0 +1 @@
+level is "sound" but support and evidence derive "epi"
diff --git a/test/fixtures/findings-schema/bad-observed-sound.json b/test/fixtures/findings-schema/bad-observed-sound.json
new file mode 100644
index 00000000..be5e23c3
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-observed-sound.json
@@ -0,0 +1,28 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "observed",
+      "observations": 5
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "sound"
+  }
+]
diff --git a/test/fixtures/findings-schema/bad-pattern-sound.expect b/test/fixtures/findings-schema/bad-pattern-sound.expect
new file mode 100644
index 00000000..7c58e70a
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-pattern-sound.expect
@@ -0,0 +1 @@
+level is "sound" but support and evidence derive "epi"
diff --git a/test/fixtures/findings-schema/bad-pattern-sound.json b/test/fixtures/findings-schema/bad-pattern-sound.json
new file mode 100644
index 00000000..1dd31a7b
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-pattern-sound.json
@@ -0,0 +1,27 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "pattern"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "sound"
+  }
+]
diff --git a/test/fixtures/findings-schema/bad-refuted-sound.expect b/test/fixtures/findings-schema/bad-refuted-sound.expect
new file mode 100644
index 00000000..7c58e70a
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-refuted-sound.expect
@@ -0,0 +1 @@
+level is "sound" but support and evidence derive "epi"
diff --git a/test/fixtures/findings-schema/bad-refuted-sound.json b/test/fixtures/findings-schema/bad-refuted-sound.json
new file mode 100644
index 00000000..e7fa2cdf
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-refuted-sound.json
@@ -0,0 +1,33 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "mechanical",
+      "prover": "lean4",
+      "prover_version": "4.30.0",
+      "target": "src/example.lean",
+      "target_sha256": "5465a2710136d470469e3bc4351c27dd0a6d8a14f520fd7009f5f196351c72e7",
+      "artefact_sha256": "f5d4cf9e8b96dd98cbf47d432fb83411dad3aa92dd37de1f21d30bebf1f03a31",
+      "result": "refutes"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "sound"
+  }
+]
diff --git a/test/fixtures/findings-schema/bad-unknown-level.expect b/test/fixtures/findings-schema/bad-unknown-level.expect
new file mode 100644
index 00000000..ab1a2d1b
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-unknown-level.expect
@@ -0,0 +1 @@
+contract broken by the value of `level`
diff --git a/test/fixtures/findings-schema/bad-unknown-level.json b/test/fixtures/findings-schema/bad-unknown-level.json
new file mode 100644
index 00000000..8641075e
--- /dev/null
+++ b/test/fixtures/findings-schema/bad-unknown-level.json
@@ -0,0 +1,27 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "pattern"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "proved"
+  }
+]
diff --git a/test/fixtures/findings-schema/good-bash-report.json b/test/fixtures/findings-schema/good-bash-report.json
new file mode 100644
index 00000000..56b43048
--- /dev/null
+++ b/test/fixtures/findings-schema/good-bash-report.json
@@ -0,0 +1,38 @@
+{
+  "submission_metadata": {
+    "repo": "example",
+    "timestamp": "2026-10-14T00:00:00+00:00",
+    "scanner": "hypatia",
+    "version": "2.0.0",
+    "finding_count": 1
+  },
+  "findings": [
+    {
+      "severity": "high",
+      "type": "unsafe_code",
+      "pattern": "example_rule",
+      "file": "src/example.rs",
+      "line": 3,
+      "code": "x",
+      "cwe": "CWE-0",
+      "fix": "y",
+      "auto_fixable": false,
+      "support": {
+        "kind": "pattern"
+      },
+      "evidence": [
+        {
+          "rule": "code_safety/example_rule",
+          "rule_version": "0.1.0",
+          "span": {
+            "file": "src/example.rs",
+            "start_line": 3,
+            "end_line": 3
+          },
+          "observations": 1
+        }
+      ],
+      "level": "epi"
+    }
+  ]
+}
diff --git a/test/fixtures/findings-schema/good-escript-sound.json b/test/fixtures/findings-schema/good-escript-sound.json
new file mode 100644
index 00000000..5d723f1c
--- /dev/null
+++ b/test/fixtures/findings-schema/good-escript-sound.json
@@ -0,0 +1,33 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "mechanical",
+      "prover": "lean4",
+      "prover_version": "4.30.0",
+      "target": "src/example.lean",
+      "target_sha256": "5465a2710136d470469e3bc4351c27dd0a6d8a14f520fd7009f5f196351c72e7",
+      "artefact_sha256": "f5d4cf9e8b96dd98cbf47d432fb83411dad3aa92dd37de1f21d30bebf1f03a31",
+      "result": "confirms"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "sound"
+  }
+]
diff --git a/test/fixtures/findings-schema/good-escript.json b/test/fixtures/findings-schema/good-escript.json
new file mode 100644
index 00000000..efd12595
--- /dev/null
+++ b/test/fixtures/findings-schema/good-escript.json
@@ -0,0 +1,68 @@
+[
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "pattern"
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "epi"
+  },
+  {
+    "rule_module": "structural_drift",
+    "type": "SD001",
+    "severity": "medium",
+    "file": ".",
+    "reason": "repo-level, no line",
+    "action": "review",
+    "support": {
+      "kind": "observed",
+      "observations": 5
+    },
+    "evidence": [
+      {
+        "rule": "code_safety/example_rule",
+        "rule_version": "0.1.0",
+        "span": {
+          "file": "src/example.rs",
+          "start_line": 3,
+          "end_line": 3
+        },
+        "observations": 1
+      }
+    ],
+    "level": "epi",
+    "baseline_status": "new"
+  },
+  {
+    "rule_module": "code_safety",
+    "type": "example_rule",
+    "severity": "high",
+    "file": "src/example.rs",
+    "line": 3,
+    "reason": "example",
+    "action": "flag",
+    "support": {
+      "kind": "observed",
+      "observations": 12
+    },
+    "evidence": [],
+    "level": "belief"
+  }
+]
diff --git a/test/verdict_test.exs b/test/verdict_test.exs
new file mode 100644
index 00000000..f44f517e
--- /dev/null
+++ b/test/verdict_test.exs
@@ -0,0 +1,196 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+defmodule Hypatia.VerdictTest do
+  @moduledoc """
+  HYP-01: every finding names its support, and its level is derived.
+
+  The Elixir mirror is checked against the two artefacts it mirrors rather
+  than against restated constants: the wire names of the levels are read out
+  of `src/Hypatia/ABI/Verdict.idr`, and the sound re-check is the one recorded
+  in the positive control `tests/accept/LeanHoleRecheckSound.idr` (whose
+  digests `scripts/recheck-lean-hole.sh` ties to a fresh Lean run).
+  """
+
+  use ExUnit.Case, async: true
+
+  alias Hypatia.Verdict
+
+  @repo_root Path.expand("..", __DIR__)
+  @abi Path.join(@repo_root, "src/Hypatia/ABI/Verdict.idr")
+  @control Path.join(@repo_root, "tests/accept/LeanHoleRecheckSound.idr")
+
+  defp control_recheck do
+    src = File.read!(@control)
+    [_, target] = Regex.run(~r/^fixturePath = "([^"]+)"/m, src)
+    [_, version] = Regex.run(~r/^  "(\d+\.\d+\.\d+)"$/m, src)
+    [_, target_sha] = Regex.run(~r/^  \(MkSha256 "([0-9a-f]{64})"\) -- targetHash$/m, src)
+    [_, artefact_sha] = Regex.run(~r/^  \(MkSha256 "([0-9a-f]{64})"\) -- artefactHash$/m, src)
+    [_, line] = Regex.run(~r/^ +\(MkSpan fixturePath (\d+) \d+\) \d+$/m, src)
+
+    {%{
+       prover: "lean4",
+       prover_version: version,
+       target: target,
+       target_sha256: target_sha,
+       artefact_sha256: artefact_sha,
+       result: "confirms"
+     }, String.to_integer(line)}
+  end
+
+  defp hole_finding(target, line) do
+    %{
+      rule_module: "code_safety",
+      type: "sorry",
+      severity: "critical",
+      file: target,
+      line: line,
+      reason: "sorry leaves proof hole",
+      action: "flag"
+    }
+  end
+
+  describe "level/2 mirrors Verdict.idr" do
+    test "the wire names are exactly the ABI's levelName strings" do
+      src = File.read!(@abi)
+
+      names =
+        Regex.scan(~r/^levelName Lv\w+ += "(\w+)"$/m, src, capture: :all_but_first)
+        |> List.flatten()
+        |> Enum.sort()
+
+      assert names == ["belief", "epi", "sound"]
+    end
+
+    test "only a confirming mechanical re-check is sound" do
+      token = [%{rule: "r/x"}]
+      assert Verdict.level(%{kind: "mechanical", result: "confirms"}, token) == "sound"
+      assert Verdict.level(%{kind: "mechanical", result: "refutes"}, token) == "epi"
+      assert Verdict.level(%{kind: "pattern"}, token) == "epi"
+      assert Verdict.level(%{kind: "observed", observations: 5}, token) == "epi"
+      assert Verdict.level(%{kind: "observed", observations: 10_000}, token) == "epi"
+    end
+
+    test "no evidence token is belief, whatever the support claims short of a re-check" do
+      assert Verdict.level(%{kind: "pattern"}, []) == "belief"
+      assert Verdict.level(%{kind: "observed", observations: 5}, []) == "belief"
+    end
+  end
+
+  describe "annotate/1" do
+    test "a rule-module finding is pattern-supported, with one token, at level epi" do
+      f = Verdict.annotate(%{rule_module: "code_safety", type: "x", file: "a.rs", line: 7})
+
+      assert f.support == %{kind: "pattern"}
+      assert f.level == "epi"
+
+      assert [
+               %{
+                 rule: "code_safety/x",
+                 rule_version: version,
+                 span: %{file: "a.rs", start_line: 7, end_line: 7},
+                 observations: 1
+               }
+             ] = f.evidence
+
+      assert version == Verdict.rule_version()
+    end
+
+    test "a file- or repo-level finding gets line 0 in its span" do
+      f = Verdict.annotate(%{rule_module: "git_state", type: "GS001", file: ".", line: nil})
+      assert [%{span: %{start_line: 0, end_line: 0}}] = f.evidence
+    end
+
+    test "a rule cannot assert its own level" do
+      forged = %{rule_module: "code_safety", type: "x", file: "a.rs", level: "sound"}
+      assert Verdict.annotate(forged).level == "epi"
+    end
+  end
+
+  describe "attach_recheck/3 — the only way to sound" do
+    test "the positive control's Lean re-check makes the fixture's finding sound" do
+      {recheck, line} = control_recheck()
+
+      assert {:ok, f} =
+               Verdict.attach_recheck(hole_finding(recheck.target, line), recheck, @repo_root)
+
+      assert f.level == "sound"
+      assert f.support.kind == "mechanical"
+      assert f.support.artefact_sha256 == recheck.artefact_sha256
+      assert Verdict.describe(f) == "sound: lean4 #{recheck.prover_version} re-check confirms"
+    end
+
+    test "the same finding without the re-check is epi" do
+      {recheck, line} = control_recheck()
+      assert Verdict.annotate(hole_finding(recheck.target, line)).level == "epi"
+    end
+
+    test "a refuting re-check is attached as recorded and derives epi" do
+      {recheck, line} = control_recheck()
+      refuted = %{recheck | result: "refutes"}
+
+      assert {:ok, f} =
+               Verdict.attach_recheck(hole_finding(recheck.target, line), refuted, @repo_root)
+
+      assert f.level == "epi"
+    end
+
+    test "a target digest that does not match the bytes on disk is refused" do
+      {recheck, line} = control_recheck()
+      forged = %{recheck | target_sha256: String.duplicate("0", 64)}
+
+      assert {:error, {:target_digest_mismatch, actual, _}} =
+               Verdict.attach_recheck(hole_finding(recheck.target, line), forged, @repo_root)
+
+      assert actual == recheck.target_sha256
+    end
+
+    test "a re-check of a different file is refused" do
+      {recheck, line} = control_recheck()
+
+      assert {:error, {:target_mismatch, "other.lean", _}} =
+               Verdict.attach_recheck(hole_finding("other.lean", line), recheck, @repo_root)
+    end
+
+    test "malformed re-checks are refused before any file is read" do
+      {recheck, line} = control_recheck()
+      finding = hole_finding(recheck.target, line)
+
+      assert {:error, {:invalid, :artefact_sha256, "F5D4"}} =
+               Verdict.attach_recheck(finding, %{recheck | artefact_sha256: "F5D4"}, @repo_root)
+
+      assert {:error, {:invalid, :prover, "z3"}} =
+               Verdict.attach_recheck(finding, %{recheck | prover: "z3"}, @repo_root)
+
+      assert {:error, {:invalid, :result, "maybe"}} =
+               Verdict.attach_recheck(finding, %{recheck | result: "maybe"}, @repo_root)
+    end
+  end
+
+  describe "CLI.collect_findings/2 — every finding names its support" do
+    test "each code_safety finding over the soundness fixtures carries the verdict fields" do
+      findings =
+        Path.join(@repo_root, "test/soundness/fixtures")
+        |> Hypatia.CLI.collect_findings([:code_safety])
+
+      assert findings != []
+
+      for f <- findings do
+        assert %{kind: "pattern"} = f.support
+        assert [%{rule: rule} | _] = f.evidence
+        assert rule == "code_safety/#{f.type}"
+        assert f.level == Verdict.level(f.support, f.evidence)
+        assert f.level == "epi"
+      end
+    end
+  end
+
+  describe "level_counts/1" do
+    test "always reports all three levels" do
+      assert Verdict.level_counts([]) == %{"sound" => 0, "epi" => 0, "belief" => 0}
+
+      assert Verdict.level_counts([%{level: "epi"}, %{level: "epi"}, %{level: "sound"}]) ==
+               %{"sound" => 1, "epi" => 2, "belief" => 0}
+    end
+  end
+end