diff --git a/docs/proposals/P-015-reachability-evidence.md b/docs/proposals/P-015-reachability-evidence.md
new file mode 100644
index 00000000..52c605dd
--- /dev/null
+++ b/docs/proposals/P-015-reachability-evidence.md
@@ -0,0 +1,97 @@
+# P-015 -- Reachability-slice evidence: explain the path, not just the point
+
+Status: **accepted, in progress** (model + SARIF builder landed; OwnIR wiring is the next patch)
+
+## Why
+
+Two academic works were proposed as inputs to Own.NET's design: **ReachHover**
+(a data-flow reachability UI; ICSME '23 + a 72-developer survey) and the
+**Optional Checker** (modular cooperating qualifier checkers via partial
+rely-guarantee; ASE '24). A review of that research landed on a sharper framing
+than the original "Rust-style borrow checker compiling to C#" pitch:
+
+> Optional Checker  -> how to build modular, checkable *contracts*
+> ReachHover        -> how to *explain* multi-file diagnostics
+> Own.NET           -> applies both to C#/WPF resources, lifetimes, XAML, DI
+
+The single most important realisation is that the "fact-based frontends -> one
+core -> explainable diagnostics" architecture the review recommends **already
+exists** in this repo (`ownir.py` facts, one core checker, several analyses).
+So the recommendation collapses to one concrete, high-leverage gap rather than a
+rewrite.
+
+## The gap (precise)
+
+A finding answers *that* something is wrong. The reachability question a
+developer actually asks is *why is this held, and through what?* Today:
+
+- `ownlang/ownir.py` `Finding` already carries `related` and emits SARIF
+  **`relatedLocations`** -- good, unordered secondary anchors (e.g. a DI
+  captive's consuming constructor).
+- But there are **no `codeFlows`** anywhere: the *ordered* retention path
+  (`singleton -> transient -> scoped`) that the DI checker already computes
+  (`CaptiveDependency.path` and friends) is dropped into the message **string**
+  instead of being emitted as a structured slice a SARIF/IDE consumer can walk.
+- The core `Diagnostic` (the `.own` path) had no structured secondary locations
+  at all -- only a primary line + caret, plus textual
+  `[consumed by ... at file:line]` riders.
+
+That ordered slice *is* the ReachHover idea. It is the highest-value, smallest
+change in the whole synthesis: the data is already computed; only the
+presentation is missing.
+
+## What this change adds
+
+1. **`ownlang/evidence.py`** -- a pure, dependency-free transform from an ordered
+   chain of `(file, line, label)` steps to the two SARIF constructs:
+   `related_locations(steps)` -> `relatedLocations`, `code_flow(steps)` ->
+   `codeFlows`, and `di_path_steps(path, loc_by_name, end_label)` which turns a
+   DI dependency path (service names) into ordered steps anchored at each
+   service's registration site. One vocabulary for every producer.
+2. **`ownlang/diagnostics.py`** -- `Diagnostic` gains a structured `evidence`
+   slice (`Evidence(line, label, file, role)`), the typed successor to the
+   textual riders, rendered as `note:` lines in both `render` and
+   `render_pretty`. Additive and backward compatible: an empty slice (the common
+   case) leaves existing output byte-for-byte unchanged.
+
+## The remaining wiring (next patch)
+
+The DI findings in `ownir.py` should pass the ordered slice through:
+
+- add `flow: tuple[tuple[str, int, str], ...] = ()` to `ownir.Finding`;
+- in `_sarif_result`, after the existing `relatedLocations`, splice
+  `result["codeFlows"] = evidence.code_flow(f.flow)` when non-empty;
+- in `_di_findings`, build `loc_by_name = {s.name: (s.file, s.line) ...}` once and
+  pass `flow=evidence.di_path_steps(c.path, loc_by_name, end_label)` per family
+  ("captures scoped service" for DI001, "leaked transient IDisposable" for DI004,
+  etc.).
+
+This is a ~10-line edit, intentionally kept out of this commit because
+`ownir.py` is large and must be edited where it can be run against its test
+suite (`build_sarif` has golden-file tests) rather than rewritten wholesale.
+
+## Staged plan (the review's priorities, mapped to this repo)
+
+- **P0 (this proposal)** -- reachability evidence for existing WPF/Event/Dispose/DI
+  findings: structured `relatedLocations` (done) + `codeFlows` slice (builder
+  done; OwnIR wiring next).
+- **P1** -- resource-protocol contracts as first-class declarations
+  (`resource Subscription { acquire: ev += h; release: ev -= h }`), building on
+  the existing `extern fn` per-parameter effects (`borrow`/`borrow_mut`/`consume`).
+- **P2** -- XAML -> .g.cs -> OwnIR join (`xaml_facts.py` already emits an
+  OwnIR-parallel envelope; the join is where the evidence slice spans XAML, the
+  generated `Connect()`, the code-behind handler and the view-model).
+- **P3** -- ArrayPool/Span borrow-like resource views (storage policies in
+  `buffers.py` already exist).
+- **P4** -- a real borrow/lifetime checker for OwnLang as a separate experimental
+  branch -- explicitly *not* the near-term roadmap.
+
+## Non-goals / honest scope
+
+- Not a "Rust borrow checker compiling to C#". The killer cases are C#/WPF
+  resource and lifetime audit (event leaks, `DispatcherTimer`, `IDisposable`
+  ownership, DI lifetime mismatch, pools), not memory safety.
+- Soundness is stated as: **sound for supported patterns, conservative when
+  facts are missing, runtime-correlated when static proof is insufficient** --
+  not whole-language soundness. The runtime-correlation arm already exists in
+  the audit subtree.
diff --git a/ownlang/diagnostics.py b/ownlang/diagnostics.py
index 66d8c4d8..48417161 100644
--- a/ownlang/diagnostics.py
+++ b/ownlang/diagnostics.py
@@ -1,6 +1,6 @@
 """Diagnostics for OwnLang. One place for every code and its human title.
 
-Numbering scheme (renumbered in this revision — see README changelog):
+Numbering scheme (renumbered in this revision -- see README changelog):
 
   001-013  flow-sensitive ownership & loan/permission violations
   020      unsupported construct (loops / async)
@@ -13,6 +13,14 @@
 different, sharper message than one that holds on only some path through a
 branch. That distinction was the reviewer's strongest point and it falls out
 naturally from the set-of-states lattice.
+
+A diagnostic can also carry an ordered *reachability slice* (``Evidence``): the
+chain of program points that explains *why* it holds -- where a resource was
+acquired, where a borrow escapes, where the missing release should go. This is
+the structured successor to the textual ``[consumed by ... at file:line]``
+riders the DI findings append: same information, but a place a tool can point at
+instead of a string to parse (P-015). See ``ownlang.evidence`` for the SARIF
+projection.
 """
 
 from __future__ import annotations
@@ -71,10 +79,39 @@ class Severity(Enum):
     "OWN040": "call to an undeclared function (unknown calls are forbidden)",
     "OWN041": "call argument mismatch",
     # ---- C# front-end resolution coverage (P-014; advisory) ----
-    "OWN050": "declaring type unresolved — leakage analysis skipped",
+    "OWN050": "declaring type unresolved -- leakage analysis skipped",
 }
 
 
+@dataclass(frozen=True)
+class Evidence:
+    """One secondary, structured location that explains a diagnostic -- a single step
+    in its reachability slice: where the resource was acquired, where a borrow
+    escapes, where the missing release should go, what consumed it. The primary
+    ``Diagnostic.line`` stays the anchor; evidence rides alongside it (rendered as
+    ``note:`` lines here; emitted as SARIF relatedLocations / codeFlows by
+    ``ownlang.evidence``).
+
+    This is the structured successor to the textual ``[consumed by ... at
+    file:line]`` riders: the same information, but a place a tool can point at
+    instead of a string to parse.
+    """
+
+    line: int
+    label: str
+    # the file of this step; None means "same file as the diagnostic's anchor".
+    file: str | None = None
+    # what this step is, for consumers that group/colour evidence: a plain "related"
+    # by default, or a resource-protocol role (acquired/released/escaped/consumed/step).
+    role: str = "related"
+
+    def render(self, anchor_file: str) -> str:
+        """A one-line ``note:`` rendering pointing at this step. ``anchor_file`` is
+        the diagnostic's own file, used when this step shares it (``file is None``)."""
+        where = self.file or anchor_file
+        return f"  note: {self.label} at {where}:{self.line}"
+
+
 @dataclass(frozen=True)
 class Diagnostic:
     code: str
@@ -85,9 +122,15 @@ class Diagnostic:
     # diagnostic is about, so the report attributes it by symbol, not by name.
     subject: str | None = None
     # the resource's human "kind" (e.g. "subscription token"), when the finding
-    # is about a tagged resource. Rendered as a ` [resource: <kind>]` suffix —
+    # is about a tagged resource. Rendered as a ` [resource: <kind>]` suffix --
     # domain-neutral metadata a later profile (e.g. WPF) keys off.
     resource_kind: str | None = None
+    # ordered reachability slice that explains this diagnostic (acquire site, escape
+    # site, missing-release point, consuming call). Empty for a single-point finding.
+    # Rendered as `note:` lines; a SARIF consumer maps it to relatedLocations /
+    # codeFlows via ownlang.evidence. Declared LAST so the positional constructor
+    # contract (code, message, line, severity, subject, resource_kind) is preserved.
+    evidence: tuple[Evidence, ...] = ()
 
     @property
     def title(self) -> str:
@@ -113,17 +156,26 @@ def _caret_col(self, src_line: str) -> int | None:
         stripped = len(src_line) - len(src_line.lstrip())
         return stripped + 1 if src_line.strip() else None
 
+    def _evidence_lines(self, filename: str) -> list[str]:
+        """The `note:` lines for this diagnostic's reachability slice, in order.
+        Empty when the finding carries no evidence (the common case), so the base
+        renderings stay byte-for-byte unchanged."""
+        return [e.render(filename) for e in self.evidence]
+
     def render(self, filename: str = "<input>") -> str:
-        """Plain one-line rendering: `file:line: severity: [code] message`."""
-        return (
+        """Plain rendering: `file:line: severity: [code] message`, followed by one
+        `note:` line per evidence step when present."""
+        head = (
             f"{filename}:{self.line}: {self.severity.value}: "
             f"[{self.code}] {self.message}{self._kind_suffix()}"
         )
+        return "\n".join([head, *self._evidence_lines(filename)])
 
     def render_pretty(self, filename: str, source: str) -> str:
         """A rustc-style rendering: a `file:line:col` header, the offending
-        source line, and a caret under the named identifier. Falls back to the
-        plain header when the line/column cannot be resolved."""
+        source line, a caret under the named identifier, and a `note:` line per
+        evidence step. Falls back to the plain header when the line/column cannot
+        be resolved."""
         lines = source.splitlines()
         src_line = lines[self.line - 1] if 1 <= self.line <= len(lines) else ""
         col = self._caret_col(src_line)
@@ -135,4 +187,5 @@ def render_pretty(self, filename: str, source: str) -> str:
             out.append(f"{gutter}{src_line}")
             if col:
                 out.append(" " * (len(gutter) + col - 1) + "^")
+        out.extend(self._evidence_lines(filename))
         return "\n".join(out)
diff --git a/ownlang/evidence.py b/ownlang/evidence.py
new file mode 100644
index 00000000..58069da8
--- /dev/null
+++ b/ownlang/evidence.py
@@ -0,0 +1,112 @@
+"""Reachability-slice evidence -> SARIF (P-015).
+
+A finding is only as useful as the *path* it shows. A bare "OWN014: lifetime
+promotion" or "DI001: captive dependency" tells a developer *that* something is
+wrong; it does not answer the question they actually ask -- *why is this value
+held, and through what?* (the data-flow reachability question ReachHover's study
+found developers ask many times a day). This module turns an ordered chain of
+program points into the two SARIF constructs that answer it:
+
+  * ``relatedLocations`` -- unordered secondary anchors ("acquired here",
+    "missing release here", "consuming constructor") that a consumer (GitHub
+    code scanning, an IDE hover) renders as clickable, labelled links beside
+    the primary location.
+  * ``codeFlows`` -- an *ordered* slice: step 1 -> step 2 -> ... -> the finding.
+    This is the reachability slice: e.g. a DI captive's
+    ``singleton -> transient -> scoped`` retention path, each hop a real source
+    location.
+
+It is deliberately a pure, dependency-free transform over ``(file, line, label)``
+triples so every producer in the core -- the OwnIR DI checker, the flow-sensitive
+ownership checker, a future XAML->.g.cs join -- emits the same shape and any
+consumer reads one vocabulary. Frontends produce facts; this is how the core
+*explains* its verdicts.
+
+The builders return plain SARIF fragments (no Own.NET types), so they compose
+into either ``ownlang.ownir.build_sarif`` (the C# extractor path) or the audit
+aggregator without a dependency either way.
+
+A step is only emitted when it has BOTH a resolvable line AND a non-empty file:
+an empty ``artifactLocation.uri`` makes the whole SARIF log unprocessable for
+GitHub code scanning, so a caller must resolve any "same file as the anchor"
+convention (e.g. ``diagnostics.Evidence(file=None)``) to a concrete path before
+building -- ``ownir.Finding`` already carries concrete paths.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Iterable
+from typing import Any
+
+# one evidence step: a source location plus the human label for what happens there.
+Step = tuple[str, int, str]   # (file, line, label)
+
+
+def _phys(file: str, line: int) -> dict[str, Any]:
+    """A SARIF ``physicalLocation`` for a 1-based line. ``region`` is omitted for a
+    file-level step (line < 1) so the location stays schema-valid rather than
+    carrying a bogus ``startLine``."""
+    loc: dict[str, Any] = {"artifactLocation": {"uri": file.replace("\\", "/")}}
+    if line >= 1:
+        loc["region"] = {"startLine": line}
+    return loc
+
+
+def related_locations(steps: Iterable[Step]) -> list[dict[str, Any]]:
+    """SARIF ``relatedLocations`` from evidence steps -- the unordered secondary
+    anchors. A step is dropped unless it has both a resolvable line and a non-empty
+    file: a related location with nowhere to point is noise, and an empty
+    ``artifactLocation.uri`` makes the SARIF log unprocessable for GitHub."""
+    return [
+        {"physicalLocation": _phys(f, ln), "message": {"text": label}}
+        for (f, ln, label) in steps if ln >= 1 and f
+    ]
+
+
+def code_flow(steps: Iterable[Step]) -> list[dict[str, Any]]:
+    """A SARIF ``codeFlows`` value (a one-element list) from an *ordered* slice of
+    evidence steps -- the reachability path that leads to the finding. A step is
+    dropped unless it has both a resolvable line and a non-empty file (see
+    ``related_locations``). Returns ``[]`` when no step survives, so a caller can
+    splice the result conditionally (``if flow: result["codeFlows"] = flow``)."""
+    locations: list[dict[str, Any]] = [
+        {"location": {"physicalLocation": _phys(f, ln), "message": {"text": label}}}
+        for (f, ln, label) in steps if ln >= 1 and f
+    ]
+    if not locations:
+        return []
+    return [{"threadFlows": [{"locations": locations}]}]
+
+
+def di_path_steps(path: tuple[str, ...],
+                  loc_by_name: dict[str, tuple[str, int]],
+                  end_label: str) -> tuple[Step, ...]:
+    """Turn a DI dependency *path* (service names, captor first, captured last)
+    into ordered evidence steps anchored at each service's registration site.
+
+    ``loc_by_name`` maps a service name to its ``(file, line)`` registration
+    location; a hop whose location is unknown is skipped (the slice stays ordered
+    and truthful -- a partial registration graph yields a partial, not a wrong,
+    path). The first hop is labelled the captor singleton, the last with
+    ``end_label`` (which differs per family: "captures scoped service", "leaked
+    transient IDisposable", ...), the middle hops as pass-through links.
+
+    This is the concrete reachability slice the DI checker already computes (the
+    ``path`` tuple on every captive finding) but today only renders into the
+    message text -- here it becomes a structured ``codeFlows``.
+    """
+    n = len(path)
+    steps: list[Step] = []
+    for i, name in enumerate(path):
+        loc = loc_by_name.get(name)
+        if loc is None:
+            continue
+        f, ln = loc
+        if i == 0:
+            label = f"singleton '{name}' (captor)"
+        elif i == n - 1:
+            label = f"{end_label} '{name}'"
+        else:
+            label = f"via '{name}'"
+        steps.append((f, ln, label))
+    return tuple(steps)
diff --git a/tests/test_diagnostics.py b/tests/test_diagnostics.py
new file mode 100644
index 00000000..c4e0bd07
--- /dev/null
+++ b/tests/test_diagnostics.py
@@ -0,0 +1,163 @@
+#!/usr/bin/env python3
+"""
+Diagnostic rendering tests (the `diagnostics` module, P-015 evidence slice).
+
+Pins two contracts that a downstream tool and the CLI both depend on:
+
+  1. The *empty-evidence invariant*: a diagnostic with no evidence (the common
+     case) renders byte-for-byte as it did before the evidence field existed, in
+     both the plain `render()` and the rustc-style `render_pretty()`. This is the
+     backward-compatibility promise the P-015 change is built on.
+  2. The *evidence slice*: a populated diagnostic appends exactly one `note:`
+     line per evidence step, in order, after the caret block; a step whose file
+     is None (the "same file as the anchor" convention) renders the diagnostic's
+     own filename.
+
+A short smoke test also pins the `ownlang.evidence` SARIF builders that the same
+slice feeds (lineless / empty-file steps are dropped so the SARIF log can never
+carry an empty artifactLocation.uri; a DI path is labelled captor-first).
+
+Run:  python tests/test_diagnostics.py
+      python tests/run_tests.py     (once folded into the suite aggregator)
+"""
+
+from __future__ import annotations
+
+import os
+import sys
+
+sys.path.insert(0, os.path.join(os.path.dirname(__file__), ".."))
+
+from ownlang import evidence
+from ownlang.diagnostics import Diagnostic, Evidence
+
+# a source whose line 3 names `b`, so render_pretty can place a caret under it.
+_SOURCE = "module M\nfn f() {\n    use b;\n}\n"
+
+
+def _empty_evidence_invariant() -> list[str]:
+    """render()/render_pretty() must be unchanged when evidence == ()."""
+    fails: list[str] = []
+    d = Diagnostic(code="OWN002", message="use 'b' after it was released", line=3)
+    if d.evidence != ():   # the default; the invariant is about this case
+        fails.append("a freshly constructed Diagnostic must default to no evidence")
+
+    plain = d.render("m.own")
+    if plain != "m.own:3: error: [OWN002] use 'b' after it was released":
+        fails.append(f"plain render changed for empty evidence: {plain!r}")
+    if "\n" in plain:
+        fails.append("plain render of an evidence-free diagnostic must be one line")
+
+    # Pin the FULL rustc-style output byte-for-byte, so a regression in the header,
+    # gutter or caret spacing is caught (not merely the absence of note: lines). The
+    # caret sits under `b`: it is at column 9 of the source line, rendered after the
+    # 6-char "  3 | " gutter, i.e. 6 + 9 - 1 = 14 leading spaces.
+    pretty = d.render_pretty("m.own", _SOURCE)
+    expected_pretty = "\n".join([
+        "m.own:3:9: error: [OWN002] use 'b' after it was released",
+        "  3 |     use b;",
+        " " * 14 + "^",
+    ])
+    if pretty != expected_pretty:
+        fails.append(f"pretty render changed for empty evidence: {pretty!r}")
+    return fails
+
+
+def _evidence_slice() -> list[str]:
+    """A populated slice appends ordered note: lines; file=None uses the anchor file."""
+    fails: list[str] = []
+    d = Diagnostic(
+        code="OWN001",
+        message="owned 'h' not released on all paths",
+        line=3,
+        evidence=(
+            Evidence(line=2, label="acquired here", role="acquired"),          # same file
+            Evidence(line=9, label="missing release", file="other.own", role="released"),
+        ),
+    )
+
+    notes = [ln for ln in d.render("m.own").splitlines() if ln.lstrip().startswith("note:")]
+    expected = [
+        "  note: acquired here at m.own:2",       # file=None -> the anchor's filename
+        "  note: missing release at other.own:9",
+    ]
+    if notes != expected:
+        fails.append(f"evidence note lines wrong/out of order: {notes!r}")
+
+    # the order must be stable: acquired before missing-release.
+    body = d.render("m.own")
+    if body.index("acquired here") > body.index("missing release"):
+        fails.append("evidence slice rendered out of order in render()")
+
+    pretty = d.render_pretty("m.own", _SOURCE)
+    pnotes = [ln for ln in pretty.splitlines() if ln.lstrip().startswith("note:")]
+    if pnotes != expected:
+        fails.append(f"render_pretty evidence lines wrong/out of order: {pnotes!r}")
+    # the notes come AFTER the caret, not before it.
+    lines = pretty.splitlines()
+    caret_idx = next(i for i, ln in enumerate(lines) if ln.strip().startswith("^"))
+    first_note_idx = next(i for i, ln in enumerate(lines) if ln.lstrip().startswith("note:"))
+    if first_note_idx <= caret_idx:
+        fails.append("render_pretty must place note: lines after the caret block")
+    return fails
+
+
+def _evidence_builders() -> list[str]:
+    """ownlang.evidence: drop unusable steps; label a DI path captor-first."""
+    fails: list[str] = []
+
+    steps = [
+        ("a.cs", 10, "acquired"),
+        ("", 11, "no file -> dropped"),       # empty file must not yield an empty uri
+        ("b.cs", 0, "no line -> dropped"),    # lineless step is noise
+    ]
+    rel = evidence.related_locations(steps)
+    if len(rel) != 1 or rel[0]["physicalLocation"]["artifactLocation"]["uri"] != "a.cs":
+        fails.append(f"related_locations should keep only the usable step: {rel!r}")
+    if any(loc["physicalLocation"]["artifactLocation"]["uri"] == "" for loc in rel):
+        fails.append("related_locations must never emit an empty artifactLocation.uri")
+
+    flow = evidence.code_flow(steps)
+    locs = flow[0]["threadFlows"][0]["locations"] if flow else []
+    if len(locs) != 1:
+        fails.append(f"code_flow should keep only the usable step: {flow!r}")
+    if evidence.code_flow([]) != []:
+        fails.append("code_flow of no steps must be [] so the caller can splice conditionally")
+    # all steps filtered out (empty file / no line) must still collapse to [],
+    # not a non-empty flow with zero locations.
+    all_dropped = [("", 11, "no file"), ("b.cs", 0, "no line")]
+    if evidence.code_flow(all_dropped) != []:
+        fails.append("code_flow must be [] when every supplied step is filtered out")
+    if evidence.related_locations(all_dropped) != []:
+        fails.append("related_locations must be [] when every supplied step is filtered out")
+
+    loc_by_name = {"App": ("app.cs", 1), "Mid": ("mid.cs", 2), "Scoped": ("db.cs", 3)}
+    di = evidence.di_path_steps(("App", "Mid", "Scoped"), loc_by_name, "captures scoped service")
+    if di[0] != ("app.cs", 1, "singleton 'App' (captor)"):
+        fails.append(f"di_path_steps must label the captor first: {di!r}")
+    if di[-1] != ("db.cs", 3, "captures scoped service 'Scoped'"):
+        fails.append(f"di_path_steps must label the captured last: {di!r}")
+    if di[1] != ("mid.cs", 2, "via 'Mid'"):
+        fails.append(f"di_path_steps must label middle hops as pass-through: {di!r}")
+    # an unknown hop is skipped, keeping the slice ordered and truthful.
+    di2 = evidence.di_path_steps(("App", "Gone", "Scoped"), loc_by_name, "captures scoped service")
+    if [s[0] for s in di2] != ["app.cs", "db.cs"]:
+        fails.append(f"di_path_steps must skip a hop with an unknown location: {di2!r}")
+    return fails
+
+
+def run() -> int:
+    """Run every diagnostics-rendering case; return 0/1."""
+    fails: list[str] = []
+    fails += _empty_evidence_invariant()
+    fails += _evidence_slice()
+    fails += _evidence_builders()
+    for f in fails:
+        print(f"DIAGNOSTICS FAIL: {f}")
+    print(f"diagnostics: {'PASS' if not fails else 'FAIL'} "
+          f"(evidence invariant + slice ordering + SARIF builders)")
+    return 1 if fails else 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(run())