From a4d403904aef2afce0cdee7a72578b44d6e83ba1 Mon Sep 17 00:00:00 2001
From: Taylor <tbuley@forbes.com>
Date: Wed, 29 Jul 2026 15:54:36 -0700
Subject: [PATCH 1/2] feat(formal): add Lean-backed logical evaluation

---
 .github/workflows/formal-maintenance.yml     |  72 ++++++++
 .github/workflows/pytest.yml                 |  12 ++
 .gitignore                                   |   1 +
 README.md                                    |  18 ++
 datasets/amfv_datasets/scraping/__init__.py  |   4 +
 datasets/amfv_datasets/scraping/html.py      |  57 ++++++-
 datasets/amfv_datasets/scraping/nice.py      | 168 ++++++++++++++++---
 datasets/test/test_scraping_html.py          |  43 +++++
 datasets/test/test_scraping_nice.py          | 147 +++++++++++++++-
 formal/AMFV.lean                             |   9 +
 formal/AMFV/Logic/Adversarial.lean           |  29 ++++
 formal/AMFV/LogicalEval.lean                 | 158 +++++++++++++++++
 formal/AMFV/ProofBoundary.lean               |  22 +++
 formal/AMFV/Scraping/ExtractionReceipt.lean  |  28 ++++
 formal/AMFV/Scraping/ListingAccounting.lean  |  31 ++++
 formal/AMFV/Scraping/UrlPolicy.lean          | 104 ++++++++++++
 formal/AMFV/Verification/CacheAdmission.lean |  50 ++++++
 formal/AMFV/Verification/Evaluation.lean     |  35 ++++
 formal/AMFV/Verification/Receipt.lean        | 107 ++++++++++++
 formal/AMFV/Verification/Verdict.lean        |  35 ++++
 formal/README.md                             |  44 +++++
 formal/fixtures/logical-eval.jsonl           |  16 ++
 lake-manifest.json                           |   6 +
 lakefile.toml                                |  12 ++
 lean-toolchain                               |   1 +
 tools/check_lean_specs.py                    | 117 +++++++++++++
 tools/check_logic_fixtures.py                |  49 ++++++
 27 files changed, 1342 insertions(+), 33 deletions(-)
 create mode 100644 .github/workflows/formal-maintenance.yml
 create mode 100644 formal/AMFV.lean
 create mode 100644 formal/AMFV/Logic/Adversarial.lean
 create mode 100644 formal/AMFV/LogicalEval.lean
 create mode 100644 formal/AMFV/ProofBoundary.lean
 create mode 100644 formal/AMFV/Scraping/ExtractionReceipt.lean
 create mode 100644 formal/AMFV/Scraping/ListingAccounting.lean
 create mode 100644 formal/AMFV/Scraping/UrlPolicy.lean
 create mode 100644 formal/AMFV/Verification/CacheAdmission.lean
 create mode 100644 formal/AMFV/Verification/Evaluation.lean
 create mode 100644 formal/AMFV/Verification/Receipt.lean
 create mode 100644 formal/AMFV/Verification/Verdict.lean
 create mode 100644 formal/README.md
 create mode 100644 formal/fixtures/logical-eval.jsonl
 create mode 100644 lake-manifest.json
 create mode 100644 lakefile.toml
 create mode 100644 lean-toolchain
 create mode 100644 tools/check_lean_specs.py
 create mode 100644 tools/check_logic_fixtures.py

diff --git a/.github/workflows/formal-maintenance.yml b/.github/workflows/formal-maintenance.yml
new file mode 100644
index 00000000..8641d6e3
--- /dev/null
+++ b/.github/workflows/formal-maintenance.yml
@@ -0,0 +1,72 @@
+name: Formal maintenance
+
+on:
+  workflow_dispatch:
+  schedule:
+    - cron: "17 8 * * 1"
+  push:
+    branches: [main]
+    paths:
+      - ".github/workflows/formal-maintenance.yml"
+      - "lean-toolchain"
+      - "lakefile.toml"
+      - "lake-manifest.json"
+      - "formal/**"
+      - "tools/check_lean_specs.py"
+      - "tools/check_logic_fixtures.py"
+      - "baseline/**/*.py"
+      - "datasets/**/*.py"
+      - "decomposer/**/*.py"
+      - "search/**/*.py"
+      - "training/**/*.py"
+      - "utils/**/*.py"
+      - "verifier/**/*.py"
+  pull_request:
+    paths:
+      - ".github/workflows/formal-maintenance.yml"
+      - "lean-toolchain"
+      - "lakefile.toml"
+      - "lake-manifest.json"
+      - "formal/**"
+      - "tools/check_lean_specs.py"
+      - "tools/check_logic_fixtures.py"
+      - "baseline/**/*.py"
+      - "datasets/**/*.py"
+      - "decomposer/**/*.py"
+      - "search/**/*.py"
+      - "training/**/*.py"
+      - "utils/**/*.py"
+      - "verifier/**/*.py"
+
+permissions:
+  contents: read
+
+concurrency:
+  group: formal-maintenance-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  maintain:
+    name: Lean 4.32 proof and conformance gate
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+
+      - name: Install pinned Lean toolchain
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: false
+          test: false
+          lint: false
+
+      - name: Build without warnings
+        run: lake build --wfail
+
+      - name: Check theorem links, tests, dependencies, and axiom footprints
+        run: python3 tools/check_lean_specs.py
+
+      - name: Replay shared logical evaluation fixtures
+        run: python3 tools/check_logic_fixtures.py
diff --git a/.github/workflows/pytest.yml b/.github/workflows/pytest.yml
index 88c3199c..660d238c 100644
--- a/.github/workflows/pytest.yml
+++ b/.github/workflows/pytest.yml
@@ -17,6 +17,12 @@ on:
       - "verifier/**"
       - "baseline/**"
       - "training/**"
+      - "formal/**"
+      - "tools/check_lean_specs.py"
+      - "tools/check_logic_fixtures.py"
+      - "lakefile.toml"
+      - "lake-manifest.json"
+      - "lean-toolchain"
   pull_request:
     paths:
       - ".github/workflows/pytest.yml"
@@ -30,6 +36,12 @@ on:
       - "verifier/**"
       - "baseline/**"
       - "training/**"
+      - "formal/**"
+      - "tools/check_lean_specs.py"
+      - "tools/check_logic_fixtures.py"
+      - "lakefile.toml"
+      - "lake-manifest.json"
+      - "lean-toolchain"
 
 jobs:
   test:
diff --git a/.gitignore b/.gitignore
index 83972fad..0ec5c62d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -205,6 +205,7 @@ tempCodeRunnerFile.py
 
 # Ruff stuff:
 .ruff_cache/
+.lake/
 
 # PyPI configuration file
 .pypirc
diff --git a/README.md b/README.md
index 8721bae3..05a62eef 100644
--- a/README.md
+++ b/README.md
@@ -26,3 +26,21 @@ Following Baichuan-M3, the task is split into three models across four steps:
 | [`training`](training/README.md)   | Training experiments and recipes for the above | Independent |
 
 The **Workspace** column marks membership in the root `uv` workspace. Independent packages (`baseline`, `training`) are excluded so they can evolve on their own.
+
+## Formal logical evaluation
+
+AMFV uses a dependency-free Lean 4.32.0 library to model structural invariants
+at high-risk boundaries such as source URL admission, scraper accounting,
+verification receipts, cache freshness, and evaluation success.
+
+```sh
+lake build --wfail
+python3 tools/check_lean_specs.py
+python3 tools/check_logic_fixtures.py
+```
+
+Python functions annotated with `# lean-spec:` are backed by a named theorem
+and an adversarial runtime test. This establishes conformance to the modeled
+invariant; it does not claim that Lean verifies Python bytecode, arbitrary HTML,
+medical truth, or corpus completeness. See [`formal/README.md`](formal/README.md)
+for the maintenance workflow and proof boundaries.
diff --git a/datasets/amfv_datasets/scraping/__init__.py b/datasets/amfv_datasets/scraping/__init__.py
index cd7cdb06..f3631f9d 100644
--- a/datasets/amfv_datasets/scraping/__init__.py
+++ b/datasets/amfv_datasets/scraping/__init__.py
@@ -20,7 +20,9 @@
 from amfv_datasets.scraping.nice import (
     GuidanceListingPage,
     GuidanceRef,
+    GuidelineExtractionReceipt,
     NiceFetchError,
+    OmittedSection,
     build_guideline_text,
     guidance_ref_from_url,
     list_published_guidance,
@@ -30,9 +32,11 @@
 
 __all__ = [
     "GuidanceRef",
+    "GuidelineExtractionReceipt",
     "GuidanceListingPage",
     "LinkMode",
     "NiceFetchError",
+    "OmittedSection",
     "OutputFormat",
     "ScrapeError",
     "ScrapeRun",
diff --git a/datasets/amfv_datasets/scraping/html.py b/datasets/amfv_datasets/scraping/html.py
index 2bd1c968..272c8948 100644
--- a/datasets/amfv_datasets/scraping/html.py
+++ b/datasets/amfv_datasets/scraping/html.py
@@ -3,9 +3,9 @@
 from __future__ import annotations
 
 import re
-from collections.abc import Iterable
+from collections.abc import Collection, Iterable
 from enum import StrEnum
-from urllib.parse import urljoin
+from urllib.parse import urljoin, urlsplit, urlunsplit
 
 from lxml import html as lxml_html
 from markdownify import MarkdownConverter
@@ -40,17 +40,46 @@ def clean_text(value: str, *, drop_numeric_citations: bool = True) -> str:
     return _WHITESPACE_RE.sub(" ", text).strip()
 
 
-def absolute_unique_urls(urls: Iterable[str], *, base_url: str) -> list[str]:
+def absolute_unique_urls(
+    urls: Iterable[str],
+    *,
+    base_url: str,
+    allowed_schemes: Collection[str] = ("http", "https"),
+    allowed_hosts: Collection[str] | None = None,
+) -> list[str]:
     """Normalize URLs against a base URL and remove duplicates.
 
     Args:
         urls: Raw URL values to normalize.
         base_url: Base URL used for relative links.
+        allowed_schemes: URL schemes that may be returned.
+        allowed_hosts: Optional exact hostname allowlist. When set, URLs with
+            credentials or non-default ports are rejected.
     """
+    normalized_schemes = {scheme.lower() for scheme in allowed_schemes}
+    normalized_hosts = {host.lower() for host in allowed_hosts} if allowed_hosts is not None else None
     seen: set[str] = set()
     normalized_urls: list[str] = []
     for raw_url in urls:
-        url = urljoin(base_url, raw_url).split("#")[0].split("?")[0]
+        parsed = urlsplit(urljoin(base_url, raw_url))
+        scheme = parsed.scheme.lower()
+        if scheme not in normalized_schemes:
+            continue
+        try:
+            port = parsed.port
+        except ValueError:
+            continue
+        if normalized_hosts is not None:
+            default_port = 80 if scheme == "http" else 443 if scheme == "https" else None
+            if (
+                parsed.hostname is None
+                or parsed.hostname.lower() not in normalized_hosts
+                or parsed.username is not None
+                or parsed.password is not None
+                or port not in {None, default_port}
+            ):
+                continue
+        url = urlunsplit(parsed._replace(query="", fragment=""))
         if url in seen:
             continue
         seen.add(url)
@@ -58,19 +87,35 @@ def absolute_unique_urls(urls: Iterable[str], *, base_url: str) -> list[str]:
     return normalized_urls
 
 
-def first_matching_urls(html_text: str, *, xpaths: Iterable[str], base_url: str) -> list[str]:
+def first_matching_urls(
+    html_text: str,
+    *,
+    xpaths: Iterable[str],
+    base_url: str,
+    allowed_schemes: Collection[str] = ("http", "https"),
+    allowed_hosts: Collection[str] | None = None,
+) -> list[str]:
     """Return normalized URLs from the first XPath with matches.
 
     Args:
         html_text: HTML page text to parse.
         xpaths: XPath expressions that return URL strings.
         base_url: Base URL used for relative links.
+        allowed_schemes: URL schemes that may be returned.
+        allowed_hosts: Optional exact hostname allowlist.
     """
     doc = lxml_html.fromstring(html_text)
     for xpath in xpaths:
         urls = doc.xpath(xpath)
         if urls:
-            return absolute_unique_urls(urls, base_url=base_url)
+            normalized_urls = absolute_unique_urls(
+                urls,
+                base_url=base_url,
+                allowed_schemes=allowed_schemes,
+                allowed_hosts=allowed_hosts,
+            )
+            if normalized_urls:
+                return normalized_urls
     return []
 
 
diff --git a/datasets/amfv_datasets/scraping/nice.py b/datasets/amfv_datasets/scraping/nice.py
index 79d5bb69..b9c92851 100644
--- a/datasets/amfv_datasets/scraping/nice.py
+++ b/datasets/amfv_datasets/scraping/nice.py
@@ -38,7 +38,7 @@
     default_client,
     scrape_listing_documents,
 )
-from amfv_datasets.scraping.html import LinkMode, document_title, first_matching_urls, html_to_markdown
+from amfv_datasets.scraping.html import LinkMode, absolute_unique_urls, document_title, html_to_markdown
 from amfv_datasets.scraping.nextjs import script_json_by_id
 
 BASE_URL = "https://www.nice.org.uk"
@@ -75,6 +75,7 @@
 )
 _NUMBERED_HEADING_RE = re.compile(r"^\s*\d+(?:\.\d+)*\s+")
 _SKIP_CHAPTER_SUFFIXES = ("finding-more-information-and-committee-details",)
+_NICE_HOSTS = ("nice.org.uk", "www.nice.org.uk")
 
 
 class _NiceScrapeStrategy(StrEnum):
@@ -99,12 +100,48 @@ class GuidanceRef:
 
 @dataclass(frozen=True)
 class GuidanceListingPage:
-    """A NICE published-guidance listing page."""
+    """A NICE published-guidance listing page.
+
+    `total` is NICE's source-reported count before AMFV filters unsupported
+    guidance types. It is not an exact count of eligible or emitted documents.
+    """
 
     refs: list[GuidanceRef]
     total: int | None
 
 
+@dataclass(frozen=True)
+class OmittedSection:
+    """A discovered source section intentionally omitted from the document."""
+
+    url: str
+    reason: str
+
+
+@dataclass(frozen=True)
+class GuidelineExtractionReceipt:
+    """Auditable result of extracting overview/chapter source sections."""
+
+    content: str
+    section_count: int
+    title: str
+    discovered_count: int
+    retained_urls: tuple[str, ...]
+    omitted_sections: tuple[OmittedSection, ...]
+    transformations: tuple[str, ...]
+
+    # lean-spec: AMFV.Scraping.ExtractionReceipt.accounted_receipt_matches_disposition_count
+    def is_accounted(self) -> bool:
+        """Return whether disposition cardinalities match the discovered count."""
+        return self.discovered_count == len(self.retained_urls) + len(self.omitted_sections)
+
+
+@dataclass(frozen=True)
+class _ChapterLinkDiscovery:
+    accepted: tuple[str, ...]
+    rejected: tuple[OmittedSection, ...]
+
+
 def _listing_url(*, page: int) -> str:
     return f"{BASE_URL}/guidance/published?sp=on&pa={page}"
 
@@ -149,20 +186,12 @@ def _parse_listing(html_text: str) -> GuidanceListingPage:
             logger.debug("Skipping unsupported NICE guidance type %s for %s", prefix, ref)
             continue
         slug = ref.lower()
-        path = doc.get("pathAndQuery") or _page_path(ref=ref, slug=slug)
-        page_url = (
-            _page_url(ref=ref, slug=slug)
-            if prefix in _ADVICE_PREFIXES
-            else f"{BASE_URL}{path}"
-            if path.startswith("/")
-            else path
-        )
         refs.append(
             GuidanceRef(
                 ref=ref,
                 slug=slug,
                 title=(doc.get("title") or ref).strip(),
-                page_url=page_url,
+                page_url=_page_url(ref=ref, slug=slug),
             )
         )
     total = results.get("resultCount")
@@ -181,14 +210,38 @@ def list_published_guidance(client: httpx.Client, page: int = 1) -> GuidanceList
     return _parse_listing(response.text)
 
 
-def _chapter_links(html_text: str, slug: str) -> list[str]:
-    """Return absolute chapter URLs from a guidance overview table of contents."""
+# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_respects_source_boundary
+def _chapter_links(html_text: str, slug: str) -> _ChapterLinkDiscovery:
+    """Return accepted and rejected chapter URLs from a table of contents."""
     chapter_path_match = f"contains(@href, '/guidance/{slug}/chapter/') or contains(@href, '/advice/{slug}/chapter/')"
     nav_xpaths = (
         f"//*[contains(concat(' ', normalize-space(@class), ' '), ' stacked-nav ')]//a[{chapter_path_match}]/@href",
         f"//ul[contains(concat(' ', normalize-space(@class), ' '), ' nav-list ')]//li//a[{chapter_path_match}]/@href",
     )
-    return first_matching_urls(html_text, xpaths=nav_xpaths, base_url=BASE_URL)
+    doc = lxml_html.fromstring(html_text)
+    rejected: list[OmittedSection] = []
+    for xpath in nav_xpaths:
+        raw_urls = doc.xpath(xpath)
+        if not raw_urls:
+            continue
+        authority_accepted = absolute_unique_urls(raw_urls, base_url=BASE_URL, allowed_hosts=_NICE_HOSTS)
+        accepted = [url for url in authority_accepted if _is_scoped_chapter_url(url, slug)]
+        for raw_url in raw_urls:
+            normalized = absolute_unique_urls([raw_url], base_url=BASE_URL, allowed_hosts=_NICE_HOSTS)
+            if normalized and _is_scoped_chapter_url(normalized[0], slug):
+                continue
+            normalized_rejection = absolute_unique_urls([raw_url], base_url=BASE_URL)
+            rejected_url = normalized_rejection[0] if normalized_rejection else raw_url
+            reason = "out_of_scope_url" if normalized else "unsafe_url"
+            rejected.append(OmittedSection(url=rejected_url, reason=reason))
+        if accepted:
+            return _ChapterLinkDiscovery(accepted=tuple(accepted), rejected=tuple(dict.fromkeys(rejected)))
+    return _ChapterLinkDiscovery(accepted=(), rejected=tuple(dict.fromkeys(rejected)))
+
+
+def _is_scoped_chapter_url(url: str, slug: str) -> bool:
+    path = urlparse(url).path.lower()
+    return path.startswith(f"/guidance/{slug}/chapter/") or path.startswith(f"/advice/{slug}/chapter/")
 
 
 def _overview_markdown(html_text: str, *, ref: GuidanceRef, link_mode: LinkMode) -> str:
@@ -283,7 +336,19 @@ def build_guideline_text(
         link_mode: Whether links are kept as markdown links or stripped to their
             visible text (default: LinkMode.KEEP).
     """
-    overview = client.get(ref.page_url)
+    receipt = _build_guideline_receipt(client, ref, link_mode=link_mode)
+    return receipt.content, receipt.section_count, receipt.title
+
+
+def _build_guideline_receipt(
+    client: httpx.Client,
+    ref: GuidanceRef,
+    *,
+    link_mode: LinkMode = LinkMode.KEEP,
+) -> GuidelineExtractionReceipt:
+    """Scrape a guideline and account for retained and omitted sections."""
+    page_url = _validated_page_url(ref)
+    overview = client.get(page_url)
     overview.raise_for_status()
     title = (
         ref.title
@@ -294,28 +359,61 @@ def build_guideline_text(
             suffixes=(" | Guidance | NICE", " | Advice | NICE"),
         )
     )
-    chapter_urls = _chapter_links(overview.text, ref.slug)
-    if not chapter_urls:
+    chapter_links = _chapter_links(overview.text, ref.slug)
+    if not chapter_links.accepted:
         raise NiceFetchError(f"No chapters found for guidance '{ref.ref}'")
 
     sections: list[str] = []
+    retained_urls: list[str] = []
+    omitted_sections = list(chapter_links.rejected)
     overview_markdown = _overview_markdown(overview.text, ref=ref, link_mode=link_mode)
     if overview_markdown:
         sections.append(overview_markdown)
+        retained_urls.append(page_url)
+    else:
+        overview_reason = (
+            "overview_omitted_by_source_policy" if _ref_prefix(ref.ref) in {"ES", "MIB"} else "empty_overview"
+        )
+        omitted_sections.append(OmittedSection(url=page_url, reason=overview_reason))
 
-    for url in chapter_urls:
+    for url in chapter_links.accepted:
         if _is_skipped_chapter(url):
+            omitted_sections.append(OmittedSection(url=url, reason="non_content_chapter"))
             continue
         chapter = client.get(url)
         chapter.raise_for_status()
         markdown = _chapter_markdown(chapter.text, link_mode=link_mode)
         if markdown:
             sections.append(markdown)
+            retained_urls.append(url)
+        else:
+            omitted_sections.append(OmittedSection(url=url, reason="empty_chapter"))
 
     content = "\n\n".join(sections).strip()
     if not content:
         raise NiceFetchError(f"No readable content for guidance '{ref.ref}'")
-    return content, len(sections), title
+    transformations = [
+        "canonicalize_chapter_urls",
+        "convert_html_to_markdown",
+        "drop_numeric_citation_markers",
+        "filter_overview_boilerplate",
+        "normalize_numbered_headings",
+        "normalize_whitespace",
+    ]
+    if link_mode is LinkMode.STRIP:
+        transformations.append("strip_links")
+    receipt = GuidelineExtractionReceipt(
+        content=content,
+        section_count=len(sections),
+        title=title,
+        discovered_count=1 + len(chapter_links.accepted) + len(chapter_links.rejected),
+        retained_urls=tuple(retained_urls),
+        omitted_sections=tuple(omitted_sections),
+        transformations=tuple(transformations),
+    )
+    if not receipt.is_accounted():
+        raise AssertionError(f"Incomplete extraction receipt for guidance '{ref.ref}'")
+    return receipt
 
 
 def scrape_guideline(
@@ -332,19 +430,25 @@ def scrape_guideline(
         link_mode: Whether links are kept as markdown links or stripped to their
             visible text (default: LinkMode.KEEP).
     """
-    content, section_count, title = build_guideline_text(client, ref, link_mode=link_mode)
+    receipt = _build_guideline_receipt(client, ref, link_mode=link_mode)
     return ScrapedDocument(
         source="nice",
         external_id=f"nice-{ref.slug}",
-        title=title,
-        url=ref.page_url,
-        content=content,
-        section_count=section_count,
+        title=receipt.title,
+        url=_validated_page_url(ref),
+        content=receipt.content,
+        section_count=receipt.section_count,
         metadata={
             "ref": ref.ref,
             "slug": ref.slug,
             "prefix": _ref_prefix(ref.ref),
             "scrape_strategy": _scrape_strategy(ref),
+            "retained_urls": list(receipt.retained_urls),
+            "omitted_sections": [
+                {"url": omitted.url, "reason": omitted.reason} for omitted in receipt.omitted_sections
+            ],
+            "transformations": list(receipt.transformations),
+            "discovered_section_count": receipt.discovered_count,
         },
     )
 
@@ -362,6 +466,13 @@ def _page_url(*, ref: str, slug: str) -> str:
     return f"{BASE_URL}{_page_path(ref=ref, slug=slug)}"
 
 
+def _validated_page_url(ref: GuidanceRef) -> str:
+    validated = guidance_ref_from_url(ref.page_url)
+    if validated.ref != ref.ref.upper() or validated.slug != ref.slug.lower():
+        raise NiceFetchError(f"Guidance reference {ref.ref!r} does not match its NICE page URL {ref.page_url!r}")
+    return validated.page_url
+
+
 def _scrape_strategy(ref: GuidanceRef) -> str:
     prefix = _ref_prefix(ref.ref)
     if prefix in _ADVICE_PREFIXES:
@@ -371,6 +482,7 @@ def _scrape_strategy(ref: GuidanceRef) -> str:
     return _NiceScrapeStrategy.CHAPTER.value
 
 
+# lean-spec: AMFV.Scraping.ListingAccounting.source_total_is_not_exact_after_filtering
 def scrape_nice(
     *,
     documents: int | None,
@@ -386,6 +498,9 @@ def scrape_nice(
         link_mode: Whether links are kept as markdown links or stripped to their
             visible text (default: LinkMode.KEEP).
         url: NICE source URL to scrape as a single document (default: None).
+
+    Listing runs report an indeterminate total because NICE's source count
+    includes guidance types filtered out by AMFV. Single-URL runs report one.
     """
     if url is not None:
 
@@ -397,9 +512,8 @@ def scrape_url() -> Iterable[ScrapedDocument]:
 
     with default_client() as client:
         first_page = list_published_guidance(client, page=1)
-    total = first_page.total if documents is None or first_page.total is None else min(documents, first_page.total)
     return ScrapeRun(
-        total=total,
+        total=None,
         documents=scrape_listing_documents(
             documents=documents,
             client_factory=default_client,
@@ -414,11 +528,13 @@ def scrape_url() -> Iterable[ScrapedDocument]:
 __all__ = [
     "BASE_URL",
     "DOCUMENT_DELAY_SECONDS",
+    "GuidelineExtractionReceipt",
     "GuidanceListingPage",
     "NICE_DATASET_DISPLAY_NAME",
     "NICE_DATASET_NAME",
     "GuidanceRef",
     "NiceFetchError",
+    "OmittedSection",
     "build_guideline_text",
     "guidance_ref_from_url",
     "list_published_guidance",
diff --git a/datasets/test/test_scraping_html.py b/datasets/test/test_scraping_html.py
index d34a8fa3..3a7f3428 100644
--- a/datasets/test/test_scraping_html.py
+++ b/datasets/test/test_scraping_html.py
@@ -23,6 +23,32 @@ def test_absolute_unique_urls_normalizes_relative_urls() -> None:
     ) == ["https://example.org/guidance/ng1", "https://example.org/guidance/ng2"]
 
 
+# lean-spec-test: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority
+def test_absolute_unique_urls_enforces_authority_policy() -> None:
+    """Host policies reject lookalike paths, credentials, and unusual ports."""
+    assert absolute_unique_urls(
+        [
+            "/guidance/ng1/chapter/recommendations?tab=contents",
+            "https://evil.example/guidance/ng1/chapter/recommendations",
+            "https://user@www.nice.org.uk/guidance/ng1/chapter/credentials",
+            "https://www.nice.org.uk:444/guidance/ng1/chapter/port",
+            "javascript:/guidance/ng1/chapter/script",
+            "https://www.nice.org.uk/guidance/ng1/chapter/recommendations#duplicate",
+        ],
+        base_url="https://www.nice.org.uk",
+        allowed_hosts=("nice.org.uk", "www.nice.org.uk"),
+    ) == ["https://www.nice.org.uk/guidance/ng1/chapter/recommendations"]
+
+
+def test_absolute_unique_urls_canonicalization_is_idempotent() -> None:
+    """Canonical URLs remain unchanged when normalized again."""
+    first_pass = absolute_unique_urls(
+        ["/guidance/ng1?tab=contents#heading"],
+        base_url="https://example.org",
+    )
+    assert absolute_unique_urls(first_pass, base_url="https://example.org") == first_pass
+
+
 def test_first_matching_urls_uses_first_xpath_with_matches() -> None:
     """URL extraction falls back across XPath selectors."""
     html_text = """
@@ -39,6 +65,23 @@ def test_first_matching_urls_uses_first_xpath_with_matches() -> None:
     ) == ["https://example.org/first"]
 
 
+def test_first_matching_urls_falls_back_when_policy_rejects_first_xpath() -> None:
+    """Rejected candidates do not prevent an accepted fallback selector."""
+    html_text = """
+    <html>
+      <nav><a href="https://evil.example/guidance/ng1/chapter/lookalike">Bad</a></nav>
+      <main><a href="/guidance/ng1/chapter/good">Good</a></main>
+    </html>
+    """
+
+    assert first_matching_urls(
+        html_text,
+        xpaths=("//nav/a/@href", "//main/a/@href"),
+        base_url="https://www.nice.org.uk",
+        allowed_hosts=("nice.org.uk", "www.nice.org.uk"),
+    ) == ["https://www.nice.org.uk/guidance/ng1/chapter/good"]
+
+
 def test_document_title_uses_heading_and_strips_suffix() -> None:
     """Document titles are read from common title locations."""
     html_text = "<html><h1>Guideline | Guidance | NICE</h1><title>Fallback</title></html>"
diff --git a/datasets/test/test_scraping_nice.py b/datasets/test/test_scraping_nice.py
index e6b9f464..a0b146b1 100644
--- a/datasets/test/test_scraping_nice.py
+++ b/datasets/test/test_scraping_nice.py
@@ -1,17 +1,23 @@
 """Tests for NICE scraping helpers."""
 
 import json
+from contextlib import nullcontext
 
 import httpx
+import pytest
 
+from amfv_datasets.scraping import nice as nice_module
 from amfv_datasets.scraping.html import LinkMode
 from amfv_datasets.scraping.nice import (
     BASE_URL,
     GuidanceListingPage,
     GuidanceRef,
+    NiceFetchError,
     build_guideline_text,
     guidance_ref_from_url,
     list_published_guidance,
+    scrape_guideline,
+    scrape_nice,
 )
 
 
@@ -31,7 +37,7 @@ def test_list_published_guidance_parses_next_data_listing() -> None:
                         {
                             "guidanceRef": "TA999",
                             "title": "Technology appraisal",
-                            "pathAndQuery": "/guidance/ta999",
+                            "pathAndQuery": "https://evil.example/guidance/ta999",
                         },
                         {
                             "guidanceRef": "QS1",
@@ -305,3 +311,142 @@ def handler(request: httpx.Request) -> httpx.Response:
         "## Quality statements\n\n"
         "Statement text."
     )
+
+
+# lean-spec-test: AMFV.Scraping.UrlPolicy.accepted_chapter_respects_source_boundary
+def test_chapter_discovery_rejects_cross_guidance_normalization() -> None:
+    """Canonicalization cannot move a chapter link into another guidance scope."""
+    overview = """
+        <nav class="stacked-nav">
+          <a href="/guidance/ng1/chapter/../../ng2/chapter/recommendations">Traversal</a>
+          <a href="/guidance/ng1/chapter/recommendations">Good</a>
+        </nav>
+    """
+    discovery = nice_module._chapter_links(overview, "ng1")
+
+    assert discovery.accepted == ("https://www.nice.org.uk/guidance/ng1/chapter/recommendations",)
+    assert discovery.rejected == (
+        nice_module.OmittedSection(
+            url="https://www.nice.org.uk/guidance/ng2/chapter/recommendations",
+            reason="out_of_scope_url",
+        ),
+    )
+
+
+# lean-spec-test: AMFV.Scraping.ExtractionReceipt.accounted_receipt_matches_disposition_count
+def test_scrape_guideline_rejects_off_domain_chapter_and_records_omissions() -> None:
+    """Only allowed NICE chapters are fetched and every discovered omission is recorded."""
+    pages = {
+        "https://www.nice.org.uk/guidance/ng1": """
+            <html>
+              <h1>Guideline</h1>
+              <h2>Overview</h2>
+              <div><p>Useful overview.</p></div>
+              <nav class="stacked-nav">
+                <a href="https://evil.example/guidance/ng1/chapter/lookalike">Lookalike</a>
+                <a href="/guidance/ng1/chapter/../../ng2/chapter/recommendations">Traversal</a>
+                <a href="/guidance/ng1/chapter/recommendations?tab=contents">Recommendations</a>
+                <a href="/guidance/ng1/chapter/finding-more-information-and-committee-details">Details</a>
+              </nav>
+            </html>
+        """,
+        "https://www.nice.org.uk/guidance/ng1/chapter/recommendations": """
+            <div class="chapter"><h2>1 Recommendation</h2><p>Do the safe thing [1].</p></div>
+        """,
+    }
+    fetched: list[str] = []
+
+    def handler(request: httpx.Request) -> httpx.Response:
+        url = str(request.url)
+        fetched.append(url)
+        return httpx.Response(200, text=pages[url])
+
+    client = httpx.Client(transport=httpx.MockTransport(handler))
+    document = scrape_guideline(
+        client,
+        GuidanceRef(
+            ref="NG1",
+            slug="ng1",
+            title="NG1",
+            page_url="https://www.nice.org.uk/guidance/ng1",
+        ),
+    )
+
+    assert all("evil.example" not in url for url in fetched)
+    assert document.metadata["retained_urls"] == [
+        "https://www.nice.org.uk/guidance/ng1",
+        "https://www.nice.org.uk/guidance/ng1/chapter/recommendations",
+    ]
+    assert document.metadata["omitted_sections"] == [
+        {
+            "url": "https://evil.example/guidance/ng1/chapter/lookalike",
+            "reason": "unsafe_url",
+        },
+        {
+            "url": "https://www.nice.org.uk/guidance/ng2/chapter/recommendations",
+            "reason": "out_of_scope_url",
+        },
+        {
+            "url": "https://www.nice.org.uk/guidance/ng1/chapter/finding-more-information-and-committee-details",
+            "reason": "non_content_chapter",
+        },
+    ]
+    assert document.metadata["transformations"] == [
+        "canonicalize_chapter_urls",
+        "convert_html_to_markdown",
+        "drop_numeric_citation_markers",
+        "filter_overview_boilerplate",
+        "normalize_numbered_headings",
+        "normalize_whitespace",
+    ]
+    assert document.metadata["discovered_section_count"] == 5
+
+
+def test_scrape_guideline_rejects_off_domain_overview_before_fetch() -> None:
+    """Manually constructed references cannot redirect the overview fetch."""
+    fetched: list[str] = []
+
+    def handler(request: httpx.Request) -> httpx.Response:
+        fetched.append(str(request.url))
+        return httpx.Response(200, text="<html></html>")
+
+    client = httpx.Client(transport=httpx.MockTransport(handler))
+
+    with pytest.raises(NiceFetchError, match="NICE guidance URL"):
+        scrape_guideline(
+            client,
+            GuidanceRef(
+                ref="NG1",
+                slug="ng1",
+                title="Guideline",
+                page_url="https://evil.example/guidance/ng1",
+            ),
+        )
+
+    assert fetched == []
+
+
+# lean-spec-test: AMFV.Scraping.ListingAccounting.source_total_is_not_exact_after_filtering
+def test_scrape_nice_does_not_claim_filtered_source_total(monkeypatch) -> None:
+    """A source count that includes filtered guidance is not an exact run total."""
+    listing = GuidanceListingPage(
+        refs=[
+            GuidanceRef(
+                ref="NG1",
+                slug="ng1",
+                title="Guideline",
+                page_url="https://www.nice.org.uk/guidance/ng1",
+            )
+        ],
+        total=6,
+    )
+    monkeypatch.setattr(
+        "amfv_datasets.scraping.nice.default_client",
+        lambda: nullcontext(object()),
+    )
+    monkeypatch.setattr(
+        "amfv_datasets.scraping.nice.list_published_guidance",
+        lambda _client, page=1: listing,
+    )
+
+    assert scrape_nice(documents=5).total is None
diff --git a/formal/AMFV.lean b/formal/AMFV.lean
new file mode 100644
index 00000000..a123324c
--- /dev/null
+++ b/formal/AMFV.lean
@@ -0,0 +1,9 @@
+import AMFV.Logic.Adversarial
+import AMFV.Scraping.ExtractionReceipt
+import AMFV.Scraping.ListingAccounting
+import AMFV.Scraping.UrlPolicy
+import AMFV.Verification.CacheAdmission
+import AMFV.Verification.Evaluation
+import AMFV.Verification.Receipt
+import AMFV.Verification.Verdict
+import AMFV.ProofBoundary
diff --git a/formal/AMFV/Logic/Adversarial.lean b/formal/AMFV/Logic/Adversarial.lean
new file mode 100644
index 00000000..d39e14a9
--- /dev/null
+++ b/formal/AMFV/Logic/Adversarial.lean
@@ -0,0 +1,29 @@
+set_option autoImplicit false
+
+namespace AMFV.Logic.Adversarial
+
+abbrev Gate (α : Type) := α → Bool
+
+def Blindspot {α : Type} (gate unsafePred : Gate α) : Prop :=
+  ∃ candidate, unsafePred candidate = true ∧ gate candidate = true
+
+def Sound {α : Type} (gate unsafePred : Gate α) : Prop :=
+  ∀ candidate, gate candidate = true → unsafePred candidate = false
+
+theorem witnessed_blindspot_refutes_sound {α : Type} {gate unsafePred : Gate α}
+    (witness : Blindspot gate unsafePred) : ¬Sound gate unsafePred := by
+  intro sound
+  obtain ⟨candidate, unsafeTrue, admitted⟩ := witness
+  have unsafeFalse := sound candidate admitted
+  simp_all
+
+def hardened {α : Type} (gate unsafePred : Gate α) : Gate α :=
+  fun candidate => gate candidate && !unsafePred candidate
+
+theorem hardened_gate_rejects_unsafe {α : Type} (gate unsafePred : Gate α) :
+    Sound (hardened gate unsafePred) unsafePred := by
+  intro candidate admitted
+  simp [hardened] at admitted
+  exact admitted.2
+
+end AMFV.Logic.Adversarial
diff --git a/formal/AMFV/LogicalEval.lean b/formal/AMFV/LogicalEval.lean
new file mode 100644
index 00000000..97c9243f
--- /dev/null
+++ b/formal/AMFV/LogicalEval.lean
@@ -0,0 +1,158 @@
+import AMFV
+import Lean
+
+set_option autoImplicit false
+
+namespace AMFV.LogicalEval
+
+open AMFV.Verification
+open Lean
+
+def schemaVersion := "amfv.logic.v1"
+def maxLogicalTime : Nat := 253402300799
+
+def getField (json : Json) (name : String) : Except String Json :=
+  json.getObjVal? name
+
+def getString (json : Json) (name : String) : Except String String := do
+  (← getField json name).getStr?
+
+def getNat (json : Json) (name : String) : Except String Nat := do
+  (← getField json name).getNat?
+
+def getLogicalTime (json : Json) (name : String) : Except String Nat := do
+  let value ← getNat json name
+  if value ≤ maxLogicalTime then
+    pure value
+  else
+    throw s!"logical timestamp {name} exceeds the supported UTC range"
+
+def getBool (json : Json) (name : String) : Except String Bool := do
+  (← getField json name).getBool?
+
+def getNatList (json : Json) (name : String) : Except String (List Nat) := do
+  let values ← (← getField json name).getArr?
+  values.toList.mapM Json.getNat?
+
+def parseVerdict (value : String) : Except String Verdict.Verdict :=
+  match value with
+  | "strongly_supported" => .ok .stronglySupported
+  | "weakly_supported" => .ok .weaklySupported
+  | "unclear" => .ok .unclear
+  | "weakly_unsubstantiated" => .ok .weaklyUnsubstantiated
+  | "strongly_unsubstantiated" => .ok .stronglyUnsubstantiated
+  | _ => .error s!"unknown verdict {value}"
+
+def receiptViolations (receipt : Receipt.Receipt) : List String :=
+  let unknown :=
+    if Receipt.referencesKnownEvidence receipt then [] else ["unknown_evidence_id"]
+  let overlap :=
+    if Receipt.evidenceDisjoint receipt then [] else ["overlapping_evidence_id"]
+  let duplicate :=
+    if Receipt.evidenceUnique receipt then [] else ["duplicate_evidence_id"]
+  let extreme :=
+    if Receipt.extremeVerdictHasWitness receipt then [] else ["extreme_verdict_without_witness"]
+  let directional :=
+    if Receipt.directionalVerdictHasWitness receipt then [] else ["directional_verdict_without_witness"]
+  unknown ++ overlap ++ duplicate ++ extreme ++ directional
+
+def evaluateReceipt (json : Json) : Except String (List String) := do
+  let receipt : Receipt.Receipt := {
+    knownEvidence := ← getNatList json "known_evidence"
+    supporting := ← getNatList json "supporting"
+    contradicting := ← getNatList json "contradicting"
+    missingContext := ← getBool json "missing_context"
+    verdict := ← parseVerdict (← getString json "verdict")
+  }
+  pure (receiptViolations receipt)
+
+def cacheViolations (entry : CacheAdmission.Entry) (query : CacheAdmission.Query) : List String :=
+  let claim :=
+    if entry.claimKey == query.claimKey then [] else ["claim_mismatch"]
+  let scope :=
+    if entry.scopeKey == query.scopeKey then [] else ["scope_mismatch"]
+  let evidence :=
+    if entry.evidenceCount > 0 then [] else ["empty_evidence"]
+  let trace :=
+    if entry.traceCount > 0 then [] else ["empty_trace"]
+  let future :=
+    if entry.verifiedAt ≤ query.asOf then [] else ["verified_in_future"]
+  let stale :=
+    if query.asOf ≤ entry.validUntil then [] else ["stale_entry"]
+  let interval :=
+    if entry.verifiedAt ≤ entry.validUntil then [] else ["invalid_validity_interval"]
+  claim ++ scope ++ evidence ++ trace ++ interval ++ future ++ stale
+
+def evaluateCache (json : Json) : Except String (List String) := do
+  let entry : CacheAdmission.Entry := {
+    claimKey := ← getNat json "entry_claim_key"
+    scopeKey := ← getNat json "entry_scope_key"
+    verifiedAt := ← getLogicalTime json "verified_at"
+    validUntil := ← getLogicalTime json "valid_until"
+    evidenceCount := ← getNat json "evidence_count"
+    traceCount := ← getNat json "trace_count"
+  }
+  let query : CacheAdmission.Query := {
+    claimKey := ← getNat json "query_claim_key"
+    scopeKey := ← getNat json "query_scope_key"
+    asOf := ← getLogicalTime json "as_of"
+  }
+  pure (cacheViolations entry query)
+
+def evaluationViolations (result : Evaluation.CaseResult) : List String :=
+  let retrieval :=
+    if result.retrievalHit then [] else ["retrieval_miss"]
+  let verdict :=
+    if result.verdictMatch then [] else ["verdict_mismatch"]
+  let score :=
+    if result.scorePass then [] else ["score_failure"]
+  retrieval ++ verdict ++ score
+
+def evaluateCase (json : Json) : Except String (List String) := do
+  let result : Evaluation.CaseResult := {
+    retrievalHit := ← getBool json "retrieval_hit"
+    verdictMatch := ← getBool json "verdict_match"
+    scorePass := ← getBool json "score_pass"
+  }
+  pure (evaluationViolations result)
+
+def evaluate (json : Json) : Except String (List String) := do
+  let schema ← getString json "schema"
+  if schema != schemaVersion then
+    throw s!"unsupported schema {schema}"
+  match ← getString json "kind" with
+  | "verifier_receipt" => evaluateReceipt json
+  | "cache_admission" => evaluateCache json
+  | "evaluation_case" => evaluateCase json
+  | kind => throw s!"unknown logical record kind {kind}"
+
+def response (violations : List String) : Json :=
+  Json.mkObj [
+    ("valid", Json.bool violations.isEmpty),
+    ("violations", Json.arr (violations.toArray.map Json.str))
+  ]
+
+def errorResponse (message : String) : Json :=
+  Json.mkObj [
+    ("valid", Json.bool false),
+    ("violations", Json.arr #[Json.str "invalid_input"]),
+    ("error", Json.str message)
+  ]
+
+def evaluateLine (line : String) : Json :=
+  match Json.parse line >>= evaluate with
+  | .ok violations => response violations
+  | .error message => errorResponse message
+
+partial def processLines (input : IO.FS.Stream) : IO Unit := do
+  let line ← input.getLine
+  if line.isEmpty then
+    pure ()
+  else
+    IO.println (Json.compress (evaluateLine line.trimAscii.toString))
+    processLines input
+
+end AMFV.LogicalEval
+
+def main : IO Unit := do
+  AMFV.LogicalEval.processLines (← IO.getStdin)
diff --git a/formal/AMFV/ProofBoundary.lean b/formal/AMFV/ProofBoundary.lean
new file mode 100644
index 00000000..d848ebe9
--- /dev/null
+++ b/formal/AMFV/ProofBoundary.lean
@@ -0,0 +1,22 @@
+set_option autoImplicit false
+
+namespace AMFV.ProofBoundary
+
+structure StructuralReceipt where
+  safeAuthority : Bool
+  accounted : Bool
+
+def structurallyValid (receipt : StructuralReceipt) : Bool :=
+  receipt.safeAuthority && receipt.accounted
+
+def validReceipt : StructuralReceipt where
+  safeAuthority := true
+  accounted := true
+
+theorem structural_validity_does_not_force_medical_truth :
+    ¬(∀ medicalTruth : Bool, structurallyValid validReceipt = true → medicalTruth = true) := by
+  intro forcesTruth
+  have falseIsTrue := forcesTruth false rfl
+  contradiction
+
+end AMFV.ProofBoundary
diff --git a/formal/AMFV/Scraping/ExtractionReceipt.lean b/formal/AMFV/Scraping/ExtractionReceipt.lean
new file mode 100644
index 00000000..5d7cd825
--- /dev/null
+++ b/formal/AMFV/Scraping/ExtractionReceipt.lean
@@ -0,0 +1,28 @@
+set_option autoImplicit false
+
+namespace AMFV.Scraping.ExtractionReceipt
+
+structure Receipt where
+  discovered : Nat
+  retained : Nat
+  omitted : Nat
+
+def Accounted (receipt : Receipt) : Prop :=
+  receipt.discovered = receipt.retained + receipt.omitted
+
+def silentOmission : Receipt where
+  discovered := 3
+  retained := 1
+  omitted := 1
+
+theorem silent_omission_is_not_accounted :
+    ¬Accounted silentOmission := by
+  change ¬(3 = 2)
+  decide
+
+theorem accounted_receipt_matches_disposition_count (receipt : Receipt)
+    (isAccounted : Accounted receipt) :
+    receipt.discovered = receipt.retained + receipt.omitted :=
+  isAccounted
+
+end AMFV.Scraping.ExtractionReceipt
diff --git a/formal/AMFV/Scraping/ListingAccounting.lean b/formal/AMFV/Scraping/ListingAccounting.lean
new file mode 100644
index 00000000..3e643b92
--- /dev/null
+++ b/formal/AMFV/Scraping/ListingAccounting.lean
@@ -0,0 +1,31 @@
+set_option autoImplicit false
+
+namespace AMFV.Scraping.ListingAccounting
+
+structure Inventory where
+  sourceTotal : Nat
+  eligibleTotal : Nat
+  emittedTotal : Nat
+
+def HonestExactTotal (inventory : Inventory) : Prop :=
+  inventory.sourceTotal = inventory.eligibleTotal
+
+def filteredExample : Inventory where
+  sourceTotal := 6
+  eligibleTotal := 5
+  emittedTotal := 5
+
+theorem source_total_is_not_exact_after_filtering :
+    ¬HonestExactTotal filteredExample := by
+  change ¬(6 = 5)
+  decide
+
+theorem emitted_under_cap (eligible cap : Nat) :
+    Nat.min eligible cap ≤ cap :=
+  Nat.min_le_right eligible cap
+
+theorem emitted_not_above_eligible (eligible cap : Nat) :
+    Nat.min eligible cap ≤ eligible :=
+  Nat.min_le_left eligible cap
+
+end AMFV.Scraping.ListingAccounting
diff --git a/formal/AMFV/Scraping/UrlPolicy.lean b/formal/AMFV/Scraping/UrlPolicy.lean
new file mode 100644
index 00000000..e79a08f0
--- /dev/null
+++ b/formal/AMFV/Scraping/UrlPolicy.lean
@@ -0,0 +1,104 @@
+set_option autoImplicit false
+
+namespace AMFV.Scraping.UrlPolicy
+
+inductive Scheme where
+  | http
+  | https
+  | other
+  deriving DecidableEq
+
+inductive Authority where
+  | nice
+  | other
+  deriving DecidableEq
+
+structure Candidate where
+  scheme : Scheme
+  authority : Authority
+  chapterPath : Bool
+  sameGuidance : Bool
+  hasCredentials : Bool
+  hasNondefaultPort : Bool
+  hasQuery : Bool
+  hasFragment : Bool
+  deriving DecidableEq
+
+def canonicalize (candidate : Candidate) : Candidate :=
+  { candidate with hasQuery := false, hasFragment := false }
+
+def pathOnlyGate (candidate : Candidate) : Bool :=
+  candidate.chapterPath
+
+def acceptedChapter (candidate : Candidate) : Bool :=
+  candidate.chapterPath &&
+    candidate.sameGuidance &&
+    (candidate.scheme == .http || candidate.scheme == .https) &&
+    candidate.authority == .nice &&
+    !candidate.hasCredentials &&
+    !candidate.hasNondefaultPort
+
+theorem canonicalize_idempotent (candidate : Candidate) :
+    canonicalize (canonicalize candidate) = canonicalize candidate := by
+  cases candidate
+  rfl
+
+theorem canonicalize_preserves_authority (candidate : Candidate) :
+    (canonicalize candidate).authority = candidate.authority := by
+  rfl
+
+theorem accepted_chapter_has_allowed_authority (candidate : Candidate)
+    (accepted : acceptedChapter candidate = true) :
+    candidate.authority = .nice := by
+  cases candidate with
+  | mk scheme authority chapterPath sameGuidance hasCredentials hasNondefaultPort hasQuery hasFragment =>
+      cases authority with
+      | nice => rfl
+      | other =>
+          cases scheme <;>
+            cases chapterPath <;>
+              cases sameGuidance <;>
+                cases hasCredentials <;>
+                  cases hasNondefaultPort <;>
+                    cases accepted
+
+theorem accepted_chapter_matches_guidance (candidate : Candidate)
+    (accepted : acceptedChapter candidate = true) :
+    candidate.sameGuidance = true := by
+  cases candidate with
+  | mk scheme authority chapterPath sameGuidance hasCredentials hasNondefaultPort hasQuery hasFragment =>
+      cases sameGuidance with
+      | false =>
+          cases scheme <;>
+            cases authority <;>
+              cases chapterPath <;>
+                cases hasCredentials <;>
+                  cases hasNondefaultPort <;>
+                    cases accepted
+      | true => rfl
+
+theorem accepted_chapter_respects_source_boundary (candidate : Candidate)
+    (accepted : acceptedChapter candidate = true) :
+    candidate.authority = .nice ∧ candidate.sameGuidance = true :=
+  ⟨accepted_chapter_has_allowed_authority candidate accepted,
+    accepted_chapter_matches_guidance candidate accepted⟩
+
+def offAuthorityChapter : Candidate where
+  scheme := .https
+  authority := .other
+  chapterPath := true
+  sameGuidance := true
+  hasCredentials := false
+  hasNondefaultPort := false
+  hasQuery := false
+  hasFragment := false
+
+theorem path_only_gate_has_off_authority_blindspot :
+    pathOnlyGate offAuthorityChapter = true ∧ offAuthorityChapter.authority = .other := by
+  decide
+
+theorem hardened_gate_closes_off_authority_blindspot :
+    acceptedChapter offAuthorityChapter = false := by
+  decide
+
+end AMFV.Scraping.UrlPolicy
diff --git a/formal/AMFV/Verification/CacheAdmission.lean b/formal/AMFV/Verification/CacheAdmission.lean
new file mode 100644
index 00000000..a3b7930c
--- /dev/null
+++ b/formal/AMFV/Verification/CacheAdmission.lean
@@ -0,0 +1,50 @@
+set_option autoImplicit false
+
+namespace AMFV.Verification.CacheAdmission
+
+structure Entry where
+  claimKey : Nat
+  scopeKey : Nat
+  verifiedAt : Nat
+  validUntil : Nat
+  evidenceCount : Nat
+  traceCount : Nat
+
+structure Query where
+  claimKey : Nat
+  scopeKey : Nat
+  asOf : Nat
+
+def admissible (entry : Entry) (query : Query) : Bool :=
+  entry.claimKey == query.claimKey &&
+    entry.scopeKey == query.scopeKey &&
+    entry.evidenceCount > 0 &&
+    entry.traceCount > 0 &&
+    entry.verifiedAt ≤ query.asOf &&
+    query.asOf ≤ entry.validUntil
+
+def staleEntry : Entry where
+  claimKey := 7
+  scopeKey := 3
+  verifiedAt := 10
+  validUntil := 20
+  evidenceCount := 2
+  traceCount := 1
+
+def lateQuery : Query where
+  claimKey := 7
+  scopeKey := 3
+  asOf := 21
+
+def hashAndScopeOnly (entry : Entry) (query : Query) : Bool :=
+  entry.claimKey == query.claimKey && entry.scopeKey == query.scopeKey
+
+theorem hash_scope_only_accepts_stale_entry :
+    hashAndScopeOnly staleEntry lateQuery = true := by
+  decide
+
+theorem admissible_rejects_stale_entry :
+    admissible staleEntry lateQuery = false := by
+  decide
+
+end AMFV.Verification.CacheAdmission
diff --git a/formal/AMFV/Verification/Evaluation.lean b/formal/AMFV/Verification/Evaluation.lean
new file mode 100644
index 00000000..c9729167
--- /dev/null
+++ b/formal/AMFV/Verification/Evaluation.lean
@@ -0,0 +1,35 @@
+set_option autoImplicit false
+
+namespace AMFV.Verification.Evaluation
+
+structure CaseResult where
+  retrievalHit : Bool
+  verdictMatch : Bool
+  scorePass : Bool
+
+def casePass (result : CaseResult) : Bool :=
+  result.retrievalHit && result.verdictMatch && result.scorePass
+
+def twoFactorPass (result : CaseResult) : Bool :=
+  result.retrievalHit && result.scorePass
+
+def wrongVerdict : CaseResult where
+  retrievalHit := true
+  verdictMatch := false
+  scorePass := true
+
+theorem case_pass_implies_all_checks (result : CaseResult)
+    (passed : casePass result = true) :
+    result.retrievalHit = true ∧ result.verdictMatch = true ∧ result.scorePass = true := by
+  simp [casePass] at passed
+  exact ⟨passed.1.1, passed.1.2, passed.2⟩
+
+theorem two_factor_gate_accepts_wrong_verdict :
+    twoFactorPass wrongVerdict = true := by
+  decide
+
+theorem three_factor_gate_rejects_wrong_verdict :
+    casePass wrongVerdict = false := by
+  decide
+
+end AMFV.Verification.Evaluation
diff --git a/formal/AMFV/Verification/Receipt.lean b/formal/AMFV/Verification/Receipt.lean
new file mode 100644
index 00000000..f51ef6fa
--- /dev/null
+++ b/formal/AMFV/Verification/Receipt.lean
@@ -0,0 +1,107 @@
+import AMFV.Verification.Verdict
+
+set_option autoImplicit false
+
+namespace AMFV.Verification.Receipt
+
+open AMFV.Verification.Verdict
+
+structure Receipt where
+  knownEvidence : List Nat
+  supporting : List Nat
+  contradicting : List Nat
+  missingContext : Bool
+  verdict : Verdict
+
+def containsNat (identifier : Nat) : List Nat → Bool
+  | [] => false
+  | candidate :: rest => Nat.beq identifier candidate || containsNat identifier rest
+
+def referencesKnownEvidence (receipt : Receipt) : Bool :=
+  receipt.supporting.all (fun identifier => containsNat identifier receipt.knownEvidence) &&
+    receipt.contradicting.all (fun identifier => containsNat identifier receipt.knownEvidence)
+
+def evidenceDisjoint (receipt : Receipt) : Bool :=
+  receipt.supporting.all (fun identifier => !containsNat identifier receipt.contradicting)
+
+def noDuplicates : List Nat → Bool
+  | [] => true
+  | identifier :: rest => !containsNat identifier rest && noDuplicates rest
+
+def evidenceUnique (receipt : Receipt) : Bool :=
+  noDuplicates receipt.supporting && noDuplicates receipt.contradicting
+
+def extremeVerdictHasWitness (receipt : Receipt) : Bool :=
+  match receipt.verdict with
+  | .stronglySupported =>
+      !receipt.supporting.isEmpty && receipt.contradicting.isEmpty && !receipt.missingContext
+  | .stronglyUnsubstantiated =>
+      !receipt.contradicting.isEmpty && receipt.supporting.isEmpty && !receipt.missingContext
+  | .weaklySupported => true
+  | .unclear => true
+  | .weaklyUnsubstantiated => true
+
+def directionalVerdictHasWitness (receipt : Receipt) : Bool :=
+  match receipt.verdict with
+  | .weaklySupported => !receipt.supporting.isEmpty
+  | .weaklyUnsubstantiated => !receipt.contradicting.isEmpty
+  | .stronglySupported => true
+  | .unclear => true
+  | .stronglyUnsubstantiated => true
+
+def valid (receipt : Receipt) : Bool :=
+  referencesKnownEvidence receipt &&
+    evidenceDisjoint receipt &&
+    evidenceUnique receipt &&
+    extremeVerdictHasWitness receipt &&
+    directionalVerdictHasWitness receipt
+
+def unknownEvidenceReceipt : Receipt where
+  knownEvidence := [1]
+  supporting := [2]
+  contradicting := []
+  missingContext := false
+  verdict := .stronglySupported
+
+def overlappingEvidenceReceipt : Receipt where
+  knownEvidence := [1]
+  supporting := [1]
+  contradicting := [1]
+  missingContext := false
+  verdict := .unclear
+
+def unwitnessedStrongReceipt : Receipt where
+  knownEvidence := []
+  supporting := []
+  contradicting := []
+  missingContext := true
+  verdict := .stronglySupported
+
+def duplicateEvidenceReceipt : Receipt where
+  knownEvidence := [1]
+  supporting := [1, 1]
+  contradicting := []
+  missingContext := false
+  verdict := .weaklySupported
+
+theorem unknown_evidence_invalid : valid unknownEvidenceReceipt = false := by
+  rfl
+
+theorem overlapping_evidence_invalid : valid overlappingEvidenceReceipt = false := by
+  rfl
+
+theorem strong_verdict_requires_witness : valid unwitnessedStrongReceipt = false := by
+  rfl
+
+theorem duplicate_evidence_invalid : valid duplicateEvidenceReceipt = false := by
+  rfl
+
+theorem known_counterexamples_invalid :
+    valid unknownEvidenceReceipt = false ∧
+      valid overlappingEvidenceReceipt = false ∧
+      valid duplicateEvidenceReceipt = false ∧
+      valid unwitnessedStrongReceipt = false := by
+  exact ⟨unknown_evidence_invalid, overlapping_evidence_invalid, duplicate_evidence_invalid,
+    strong_verdict_requires_witness⟩
+
+end AMFV.Verification.Receipt
diff --git a/formal/AMFV/Verification/Verdict.lean b/formal/AMFV/Verification/Verdict.lean
new file mode 100644
index 00000000..7044de7f
--- /dev/null
+++ b/formal/AMFV/Verification/Verdict.lean
@@ -0,0 +1,35 @@
+set_option autoImplicit false
+
+namespace AMFV.Verification.Verdict
+
+inductive Verdict where
+  | stronglySupported
+  | weaklySupported
+  | unclear
+  | weaklyUnsubstantiated
+  | stronglyUnsubstantiated
+  deriving DecidableEq
+
+def score : Verdict → Int
+  | .stronglySupported => 2
+  | .weaklySupported => 1
+  | .unclear => 0
+  | .weaklyUnsubstantiated => -1
+  | .stronglyUnsubstantiated => -2
+
+def reverse : Verdict → Verdict
+  | .stronglySupported => .stronglyUnsubstantiated
+  | .weaklySupported => .weaklyUnsubstantiated
+  | .unclear => .unclear
+  | .weaklyUnsubstantiated => .weaklySupported
+  | .stronglyUnsubstantiated => .stronglySupported
+
+theorem reverse_score (verdict : Verdict) :
+    score (reverse verdict) = -score verdict := by
+  cases verdict <;> decide
+
+theorem unclear_is_not_strongly_unsubstantiated :
+    Verdict.unclear ≠ Verdict.stronglyUnsubstantiated := by
+  decide
+
+end AMFV.Verification.Verdict
diff --git a/formal/README.md b/formal/README.md
new file mode 100644
index 00000000..e19b525e
--- /dev/null
+++ b/formal/README.md
@@ -0,0 +1,44 @@
+# AMFV logical evaluation
+
+This directory contains small, executable models of AMFV's structural
+invariants. The models use Lean's standard library only and are pinned to Lean
+4.32.0.
+
+```sh
+lake build --wfail
+python3 tools/check_lean_specs.py
+python3 tools/check_logic_fixtures.py
+```
+
+## What a proof link means
+
+A Python annotation such as
+`# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority`
+links an implementation decision to a named theorem. Lean proves the theorem
+about the model. Python regression tests exercise the corresponding production
+behavior against the same counterexample and carry a matching
+`# lean-spec-test:` annotation. CI requires each target to be a theorem with an
+empty axiom footprint. The annotation does not claim that Lean verifies Python
+bytecode, arbitrary web pages, clinical truth, or corpus completeness.
+
+## Maintenance workflow
+
+1. Reduce the disputed behavior to a finite model.
+2. Add a concrete counterexample showing the old gate admits a bad state.
+3. State and prove the hardened invariant without placeholders.
+4. Patch the runtime and add a regression test using the same counterexample.
+5. Place a `lean-spec` annotation directly above the supported Python symbol.
+6. Run the two commands above together with pytest and Ruff.
+
+Keep theorems narrow and operational. The repository checker rejects Lake
+dependencies, proof placeholders, assumption declarations, tagged definitions,
+tagged theorems with axiom dependencies, and proof links without paired runtime
+tests.
+
+## Logical evaluator
+
+`lake exe amfv_logic` reads one `amfv.logic.v1` JSON object per line and emits
+one structural result per line. Supported kinds are `verifier_receipt`,
+`cache_admission`, and `evaluation_case`. The evaluator reports stable
+violation codes for CI and development tooling. It does not judge medical
+claims or evidence content.
diff --git a/formal/fixtures/logical-eval.jsonl b/formal/fixtures/logical-eval.jsonl
new file mode 100644
index 00000000..82b9f3f4
--- /dev/null
+++ b/formal/fixtures/logical-eval.jsonl
@@ -0,0 +1,16 @@
+{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1,2],"supporting":[1],"contradicting":[],"missing_context":false,"verdict":"strongly_supported","expected_valid":true,"expected_violations":[]}
+{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1],"supporting":[2],"contradicting":[],"missing_context":false,"verdict":"strongly_supported","expected_valid":false,"expected_violations":["unknown_evidence_id"]}
+{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1],"supporting":[1],"contradicting":[1],"missing_context":false,"verdict":"unclear","expected_valid":false,"expected_violations":["overlapping_evidence_id"]}
+{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[1],"supporting":[1,1],"contradicting":[],"missing_context":false,"verdict":"weakly_supported","expected_valid":false,"expected_violations":["duplicate_evidence_id"]}
+{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[],"supporting":[],"contradicting":[],"missing_context":true,"verdict":"strongly_supported","expected_valid":false,"expected_violations":["extreme_verdict_without_witness"]}
+{"schema":"amfv.logic.v1","kind":"verifier_receipt","known_evidence":[],"supporting":[],"contradicting":[],"missing_context":false,"verdict":"weakly_supported","expected_valid":false,"expected_violations":["directional_verdict_without_witness"]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":20,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":15,"expected_valid":true,"expected_violations":[]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7e0,"entry_scope_key":3e0,"verified_at":1e1,"valid_until":2e1,"evidence_count":2e0,"trace_count":1e0,"query_claim_key":7e0,"query_scope_key":3e0,"as_of":1.5e1,"expected_valid":true,"expected_violations":[]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":20,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":21,"expected_valid":false,"expected_violations":["stale_entry"]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":20,"evidence_count":0,"trace_count":0,"query_claim_key":7,"query_scope_key":4,"as_of":9,"expected_valid":false,"expected_violations":["scope_mismatch","empty_evidence","empty_trace","verified_in_future"]}
+{"schema":"amfv.logic.v1","kind":"evaluation_case","retrieval_hit":true,"verdict_match":true,"score_pass":true,"expected_valid":true,"expected_violations":[]}
+{"schema":"amfv.logic.v1","kind":"evaluation_case","retrieval_hit":true,"verdict_match":false,"score_pass":true,"expected_valid":false,"expected_violations":["verdict_mismatch"]}
+{"schema":"amfv.logic.v2","kind":"evaluation_case","retrieval_hit":true,"verdict_match":true,"score_pass":true,"expected_valid":false,"expected_violations":["invalid_input"]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":10,"valid_until":null,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":15,"expected_valid":false,"expected_violations":["invalid_input"]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":20,"valid_until":10,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":15,"expected_valid":false,"expected_violations":["invalid_validity_interval","verified_in_future","stale_entry"]}
+{"schema":"amfv.logic.v1","kind":"cache_admission","entry_claim_key":7,"entry_scope_key":3,"verified_at":1000000000000000000000000000000,"valid_until":1000000000000000000000000000001,"evidence_count":2,"trace_count":1,"query_claim_key":7,"query_scope_key":3,"as_of":1000000000000000000000000000000,"expected_valid":false,"expected_violations":["invalid_input"]}
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 00000000..cef90821
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "amfv",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 00000000..ebdf9d0d
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,12 @@
+name = "amfv"
+version = "0.1.0"
+defaultTargets = ["AMFV", "amfv_logic"]
+
+[[lean_lib]]
+name = "AMFV"
+srcDir = "formal"
+
+[[lean_exe]]
+name = "amfv_logic"
+srcDir = "formal"
+root = "AMFV.LogicalEval"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 00000000..94b9f495
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.32.0
diff --git a/tools/check_lean_specs.py b/tools/check_lean_specs.py
new file mode 100644
index 00000000..0649c8a1
--- /dev/null
+++ b/tools/check_lean_specs.py
@@ -0,0 +1,117 @@
+#!/usr/bin/env python3
+"""Check Lean proof hygiene and resolve Python ``lean-spec`` annotations."""
+
+from __future__ import annotations
+
+import json
+import re
+import subprocess
+import sys
+import tempfile
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+FORMAL_ROOT = ROOT / "formal"
+PYTHON_ROOTS = ("baseline", "datasets", "decomposer", "search", "training", "utils", "verifier")
+TAG_RE = re.compile(r"^\s*#\s*lean-spec:\s*([A-Za-z_][A-Za-z0-9_.]*)\s*$")
+TEST_TAG_RE = re.compile(r"^\s*#\s*lean-spec-test:\s*([A-Za-z_][A-Za-z0-9_.]*)\s*$")
+DECL_RE = re.compile(r"^\s*(?:async\s+)?(?:def|class)\s+[A-Za-z_][A-Za-z0-9_]*")
+FORBIDDEN_RE = re.compile(
+    r"^\s*(?:(?:private|protected|noncomputable|unsafe)\s+)*(?:axiom|constant|opaque)\s+"
+    r"|\b(?:by\s+)?(?:sorry|admit)\b"
+)
+
+
+def fail(message: str) -> None:
+    """Print a checker failure and terminate."""
+    raise SystemExit(message)
+
+
+def check_formal_hygiene() -> None:
+    """Reject proof placeholders and assumption declarations."""
+    failures: list[str] = []
+    for path in sorted(FORMAL_ROOT.rglob("*.lean")):
+        for line_number, line in enumerate(path.read_text().splitlines(), start=1):
+            code = line.split("--", 1)[0]
+            if FORBIDDEN_RE.search(code):
+                failures.append(f"{path.relative_to(ROOT)}:{line_number}: forbidden proof escape")
+    if failures:
+        fail("\n".join(failures))
+    manifest = json.loads((ROOT / "lake-manifest.json").read_text())
+    if manifest.get("packages") != []:
+        fail("formal library must remain dependency-free")
+
+
+def collect_tags() -> list[str]:
+    """Collect annotations and ensure they are attached to Python declarations."""
+    tags: list[str] = []
+    test_tags: set[str] = set()
+    failures: list[str] = []
+    for source_root in PYTHON_ROOTS:
+        for path in sorted((ROOT / source_root).rglob("*.py")):
+            lines = path.read_text().splitlines()
+            for index, line in enumerate(lines):
+                match = TAG_RE.match(line)
+                test_match = TEST_TAG_RE.match(line)
+                if test_match:
+                    if index + 1 >= len(lines) or not DECL_RE.match(lines[index + 1]):
+                        failures.append(
+                            f"{path.relative_to(ROOT)}:{index + 1}: "
+                            "lean-spec-test must immediately precede a test function"
+                        )
+                    test_tags.add(test_match.group(1))
+                if not match:
+                    continue
+                if index + 1 >= len(lines) or not DECL_RE.match(lines[index + 1]):
+                    failures.append(
+                        f"{path.relative_to(ROOT)}:{index + 1}: lean-spec must immediately precede a function or class"
+                    )
+                tags.append(match.group(1))
+    if failures:
+        fail("\n".join(failures))
+    if not tags:
+        fail("no lean-spec annotations found")
+    untested_tags = sorted(set(tags) - test_tags)
+    if untested_tags:
+        fail("lean-spec annotations without paired runtime tests:\n" + "\n".join(untested_tags))
+    return tags
+
+
+def resolve_tags(tags: list[str]) -> None:
+    """Ask Lean to resolve every referenced declaration."""
+    source = "import AMFV\n\n" + "\n".join(
+        f"set_option pp.proofs false in\n#print {tag}\n#print axioms {tag}" for tag in sorted(set(tags))
+    )
+    source += "\n"
+    with tempfile.NamedTemporaryFile("w", suffix=".lean", dir=ROOT, delete=False) as handle:
+        handle.write(source)
+        check_path = Path(handle.name)
+    try:
+        result = subprocess.run(
+            ["lake", "env", "lean", str(check_path)],
+            cwd=ROOT,
+            text=True,
+            capture_output=True,
+            check=False,
+        )
+    finally:
+        check_path.unlink(missing_ok=True)
+    if result.returncode:
+        sys.stderr.write(result.stdout)
+        sys.stderr.write(result.stderr)
+        fail("one or more lean-spec annotations do not resolve")
+    for tag in set(tags):
+        if f"theorem {tag} " not in result.stdout:
+            fail(f"lean-spec target is not a theorem: {tag}")
+        if f"'{tag}' depends on axioms:" in result.stdout:
+            fail(f"lean-spec theorem has an axiom dependency: {tag}")
+
+
+def main() -> None:
+    """Run all formal-source checks."""
+    check_formal_hygiene()
+    resolve_tags(collect_tags())
+
+
+if __name__ == "__main__":
+    main()
diff --git a/tools/check_logic_fixtures.py b/tools/check_logic_fixtures.py
new file mode 100644
index 00000000..fe7c4ef8
--- /dev/null
+++ b/tools/check_logic_fixtures.py
@@ -0,0 +1,49 @@
+#!/usr/bin/env python3
+"""Run shared JSONL fixtures through the Lean logical evaluator."""
+
+from __future__ import annotations
+
+import json
+import subprocess
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+FIXTURES = ROOT / "formal" / "fixtures" / "logical-eval.jsonl"
+
+
+def main() -> None:
+    """Evaluate every fixture and compare stable result fields."""
+    lines = [line for line in FIXTURES.read_text().splitlines() if line.strip()]
+    records = [json.loads(line) for line in lines]
+    process = subprocess.run(
+        ["lake", "exe", "amfv_logic"],
+        cwd=ROOT,
+        input="\n".join(lines) + "\n",
+        text=True,
+        capture_output=True,
+        check=False,
+    )
+    if process.returncode:
+        raise SystemExit(process.stderr or process.stdout)
+    outputs = [json.loads(line) for line in process.stdout.splitlines() if line.strip()]
+    if len(outputs) != len(records):
+        raise SystemExit(f"expected {len(records)} oracle responses; got {len(outputs)}")
+    failures: list[str] = []
+    for index, (record, output) in enumerate(zip(records, outputs, strict=True), start=1):
+        expected = {
+            "valid": record["expected_valid"],
+            "violations": record["expected_violations"],
+        }
+        actual = {
+            "valid": output.get("valid"),
+            "violations": output.get("violations"),
+        }
+        if actual != expected:
+            failures.append(f"fixture {index}: expected {expected!r}; got {actual!r}")
+    if failures:
+        raise SystemExit("\n".join(failures))
+    print(f"{len(records)} logical-evaluation fixtures passed")
+
+
+if __name__ == "__main__":
+    main()

From a1d5dd4fcebd6e8aa608c1353284875fe611ba83 Mon Sep 17 00:00:00 2001
From: Taylor <tbuley@forbes.com>
Date: Wed, 29 Jul 2026 19:05:31 -0700
Subject: [PATCH 2/2] docs: add formal logic maintenance guide

---
 FORMAL_LOGIC.md  | 305 +++++++++++++++++++++++++++++++++++++++++++++++
 README.md        |   7 +-
 formal/README.md |  15 +--
 3 files changed, 315 insertions(+), 12 deletions(-)
 create mode 100644 FORMAL_LOGIC.md

diff --git a/FORMAL_LOGIC.md b/FORMAL_LOGIC.md
new file mode 100644
index 00000000..8f71926d
--- /dev/null
+++ b/FORMAL_LOGIC.md
@@ -0,0 +1,305 @@
+# Maintaining AMFV's formal logic
+
+AMFV uses Lean to specify and test structural rules at boundaries where an
+ordinary program can return plausible-looking but invalid data. The current
+models cover source URL admission, scraper accounting, verification receipts,
+cache admission, and evaluation success.
+
+This is an engineering layer, not a claim that AMFV is wholly verified. Lean
+proves properties of the finite models in `formal/`. Python tests and shared
+fixtures connect those models to runtime behavior.
+
+## Why this layer exists
+
+Medical fact verification depends on more than a model's final score. The
+system must also preserve where evidence came from, which evidence a receipt
+uses, whether cached work belongs to the same scope, and whether an evaluation
+actually agrees with its reference.
+
+These rules are:
+
+- small enough to state precisely;
+- important enough that silent failure is expensive;
+- stable enough to serve as interfaces between components; and
+- easy to under-test if only happy paths are exercised.
+
+Lean gives these rules an executable, reviewable definition. It is a
+development and CI dependency only; AMFV's Python runtime does not invoke Lean.
+
+## What is and is not proved
+
+The Lean library proves the named theorems about the types and functions
+declared under `formal/`. The repository then checks that selected Python
+symbols point to real theorems and have paired runtime tests.
+
+This establishes a maintained correspondence. It does not prove:
+
+- arbitrary Python bytecode correct;
+- arbitrary HTML or JSON correctly parsed;
+- a medical claim true or false;
+- evidence clinically sufficient;
+- a source corpus complete; or
+- the network, clock, or upstream source trustworthy.
+
+When adding a theorem, state its assumptions in its types or surrounding
+documentation. Do not describe a model property as a property of the whole
+application unless the runtime bridge actually enforces it.
+
+## Repository layout
+
+| Path | Responsibility |
+| --- | --- |
+| `lean-toolchain` | Pins the exact Lean release used locally and in CI. |
+| `lakefile.toml` | Declares the `AMFV` library and `amfv_logic` executable. |
+| `lake-manifest.json` | Records the dependency-free Lake project state. |
+| `formal/AMFV.lean` | Imports the public formal library. |
+| `formal/AMFV/Logic/` | General adversarial logical gates. |
+| `formal/AMFV/Scraping/` | URL policy and scraper-accounting models. |
+| `formal/AMFV/Verification/` | Receipt, cache, verdict, and evaluation models. |
+| `formal/AMFV/LogicalEval.lean` | JSONL logical-evaluation executable. |
+| `formal/AMFV/ProofBoundary.lean` | Explicit statements about the proof boundary. |
+| `formal/fixtures/logical-eval.jsonl` | Shared Lean/Python conformance cases. |
+| `tools/check_lean_specs.py` | Proof hygiene, dependency, tag, test, and axiom checks. |
+| `tools/check_logic_fixtures.py` | Replays shared fixtures through Lean. |
+| `.github/workflows/formal-maintenance.yml` | Pull-request, push, scheduled, and manual gate. |
+
+The formal project intentionally uses only Lean's standard library. Keeping the
+model small and dependency-free makes it easier for maintainers to audit and
+keeps CI failures attributable to this repository.
+
+## Local setup
+
+Install Lean through `elan`, Lean's toolchain manager. From the repository root,
+confirm that the pinned version is selected:
+
+```sh
+lean --version
+lake --version
+cat lean-toolchain
+```
+
+`elan` reads `lean-toolchain` automatically. The expected pin is
+`leanprover/lean4:v4.32.0`.
+
+Install the Python development environment separately:
+
+```sh
+uv sync --dev
+```
+
+No Lean package installation is required. A successful first build downloads
+or selects the pinned toolchain and builds the local project:
+
+```sh
+lake build --wfail
+```
+
+## The normal maintenance loop
+
+Use the same counterexample from discovery through proof and runtime repair:
+
+1. Identify a structural state that AMFV must reject or account for.
+2. Reduce it to the smallest finite model that preserves the failure.
+3. Add the counterexample to Lean and show why the old gate is insufficient.
+4. State and prove a narrow invariant for the repaired gate.
+5. Patch the Python boundary that enforces the rule.
+6. Add a focused Python regression test using the same counterexample.
+7. Link the runtime symbol and test to the theorem.
+8. Add or update shared JSONL fixtures when the rule is part of the logical
+   evaluator protocol.
+9. Run the full maintenance gate before requesting review.
+
+Prefer a theorem about one admission or accounting decision over a theorem that
+recreates an entire Python subsystem. Small models are easier to review, reuse,
+and keep aligned.
+
+## Linking Python to a theorem
+
+Put a `lean-spec` comment immediately above the supported Python function or
+class:
+
+```python
+# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority
+def is_allowed_chapter(...):
+    ...
+```
+
+Put the matching `lean-spec-test` comment immediately above a pytest test:
+
+```python
+# lean-spec-test: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority
+def test_rejects_off_domain_chapter(...):
+    ...
+```
+
+The fully qualified name must resolve to a Lean `theorem`, not merely a
+definition. Every runtime tag must have at least one paired test tag.
+
+`tools/check_lean_specs.py` enforces that:
+
+- both annotations are attached directly to Python declarations;
+- each runtime annotation has a paired runtime test;
+- every named declaration exists and is a theorem;
+- tagged theorems have an empty axiom footprint;
+- Lean sources contain no `sorry`, `admit`, `axiom`, `constant`, or `opaque`
+  proof escape; and
+- `lake-manifest.json` contains no external packages.
+
+If a Python symbol implements several independent rules, use a small validating
+function for each rule instead of making one annotation stand for an ambiguous
+bundle of behavior.
+
+## Shared logical-evaluation fixtures
+
+`lake exe amfv_logic` accepts one `amfv.logic.v1` JSON object per line and emits
+one result per line. Supported input kinds are:
+
+- `verifier_receipt`;
+- `cache_admission`; and
+- `evaluation_case`.
+
+Each fixture in `formal/fixtures/logical-eval.jsonl` includes
+`expected_valid` and `expected_violations`. Violation codes are part of the
+developer-facing protocol: keep them stable unless a deliberate protocol change
+is documented and applied to both implementations.
+
+When extending the protocol:
+
+1. define the rule and violation code in the Lean model;
+2. update `formal/AMFV/LogicalEval.lean`;
+3. update the Python mirror;
+4. add valid, invalid, boundary, and malformed fixtures;
+5. make both implementations return the same ordered result; and
+6. run both the Lean fixture replay and Python conformance tests.
+
+Fixtures should include the smallest counterexample, not just realistic large
+objects. For time rules, cover exact boundaries, unreasonable values, UTC
+normalization, and daylight-saving folds where applicable. For collections,
+cover missing fields, wrong shapes, unknown identifiers, duplicates, overlaps,
+and empty directional evidence.
+
+## Required checks
+
+Run these commands from the repository root:
+
+```sh
+lake build --wfail
+python3 tools/check_lean_specs.py
+python3 tools/check_logic_fixtures.py
+uv run pytest
+uv run ruff check .
+uv run ruff format --check .
+```
+
+When changing a package's public or packaging surface, also build that package,
+for example:
+
+```sh
+uv build --package amfv-verifier
+```
+
+`--wfail` is intentional: new Lean warnings are maintenance failures rather
+than deferred cleanup.
+
+## Continuous maintenance
+
+`.github/workflows/formal-maintenance.yml` runs when formal files, proof-link
+tools, the workflow itself, or Python component files change. It also runs every
+Monday and can be started manually with `workflow_dispatch`.
+
+The workflow:
+
+1. checks out the repository;
+2. installs the version from `lean-toolchain`;
+3. builds Lean with warnings treated as errors;
+4. verifies theorem links, paired tests, dependencies, and axiom footprints;
+5. replays the shared logical-evaluation fixtures.
+
+The scheduled run is a drift detector. Do not solve a scheduled failure by
+loosening a theorem, deleting a counterexample, or weakening the checker. First
+identify whether the toolchain, model, runtime link, or fixture protocol drifted.
+
+## Updating Lean
+
+Treat a Lean upgrade as its own pull request:
+
+1. change `lean-toolchain` to the intended exact release;
+2. run `lake update` to refresh `lake-manifest.json`;
+3. run every required check above;
+4. inspect warnings and proof changes rather than applying broad mechanical
+   rewrites;
+5. confirm `packages` remains empty in `lake-manifest.json`;
+6. record meaningful language or behavior changes in the pull-request body.
+
+Do not use an unpinned channel such as `stable` or `nightly`. Do not add Mathlib
+or another Lean dependency merely to shorten a small proof; propose that change
+explicitly with its maintenance and supply-chain cost.
+
+## Diagnosing failures
+
+### A `lean-spec` target does not resolve
+
+Import its module from `formal/AMFV.lean`, check the fully qualified namespace,
+and run:
+
+```sh
+lake env lean formal/AMFV.lean
+python3 tools/check_lean_specs.py
+```
+
+### A theorem has an axiom dependency
+
+Inspect it directly:
+
+```lean
+#print axioms AMFV.Namespace.theorem_name
+```
+
+Remove the assumption or proof escape. Do not suppress the checker.
+
+### Lean and Python disagree on a fixture
+
+Reduce the failing record to the smallest JSON object that still disagrees.
+Then compare:
+
+```sh
+lake exe amfv_logic < formal/fixtures/logical-eval.jsonl
+python3 tools/check_logic_fixtures.py
+uv run pytest
+```
+
+Determine whether the model, Python mirror, or expected protocol result is
+wrong. The formal implementation is not automatically authoritative about
+medical meaning; the intended rule must be reviewed.
+
+### CI passes locally but fails on the schedule
+
+Confirm the checked-in toolchain and manifest match the local environment, then
+rerun with a clean Lake build directory if necessary. If the failure is caused
+by an upstream action change, pin or repair the workflow in a focused pull
+request rather than bypassing the formal gate.
+
+## Review checklist
+
+Before merging a formal-logic change, verify:
+
+- [ ] The motivating bad state is concrete and reproducible.
+- [ ] The model is smaller than the runtime behavior it constrains.
+- [ ] Assumptions and proof boundaries are explicit.
+- [ ] The theorem has no proof placeholders or axiom dependencies.
+- [ ] The Python enforcement point has a `lean-spec` tag.
+- [ ] A focused regression test has the matching `lean-spec-test` tag.
+- [ ] Shared fixtures cover both acceptance and rejection when applicable.
+- [ ] Violation codes and protocol changes are deliberate and documented.
+- [ ] Lean remains a development/CI dependency, not a runtime dependency.
+- [ ] All required local and CI checks pass.
+
+## Choosing the next proof target
+
+Good targets are deterministic admission, accounting, freshness, scope, and
+agreement rules whose failure can silently contaminate later stages. Avoid
+using Lean to restate broad product intent or to make claims about clinical
+truth that require empirical evidence.
+
+The practical question is: **what invalid state could still look valid to the
+next component?** Start there.
diff --git a/README.md b/README.md
index 05a62eef..9767ef11 100644
--- a/README.md
+++ b/README.md
@@ -42,5 +42,8 @@ python3 tools/check_logic_fixtures.py
 Python functions annotated with `# lean-spec:` are backed by a named theorem
 and an adversarial runtime test. This establishes conformance to the modeled
 invariant; it does not claim that Lean verifies Python bytecode, arbitrary HTML,
-medical truth, or corpus completeness. See [`formal/README.md`](formal/README.md)
-for the maintenance workflow and proof boundaries.
+medical truth, or corpus completeness.
+
+See [`FORMAL_LOGIC.md`](FORMAL_LOGIC.md) for the complete developer and
+maintenance guide. The shorter [`formal/README.md`](formal/README.md) is a
+directory-level quick reference.
diff --git a/formal/README.md b/formal/README.md
index e19b525e..f3ad9c4d 100644
--- a/formal/README.md
+++ b/formal/README.md
@@ -4,13 +4,17 @@ This directory contains small, executable models of AMFV's structural
 invariants. The models use Lean's standard library only and are pinned to Lean
 4.32.0.
 
+The canonical developer guide is [`../FORMAL_LOGIC.md`](../FORMAL_LOGIC.md).
+Read it before adding a model, changing the JSONL protocol, linking a Python
+boundary, or updating the Lean toolchain.
+
 ```sh
 lake build --wfail
 python3 tools/check_lean_specs.py
 python3 tools/check_logic_fixtures.py
 ```
 
-## What a proof link means
+## Quick reference
 
 A Python annotation such as
 `# lean-spec: AMFV.Scraping.UrlPolicy.accepted_chapter_has_allowed_authority`
@@ -21,15 +25,6 @@ behavior against the same counterexample and carry a matching
 empty axiom footprint. The annotation does not claim that Lean verifies Python
 bytecode, arbitrary web pages, clinical truth, or corpus completeness.
 
-## Maintenance workflow
-
-1. Reduce the disputed behavior to a finite model.
-2. Add a concrete counterexample showing the old gate admits a bad state.
-3. State and prove the hardened invariant without placeholders.
-4. Patch the runtime and add a regression test using the same counterexample.
-5. Place a `lean-spec` annotation directly above the supported Python symbol.
-6. Run the two commands above together with pytest and Ruff.
-
 Keep theorems narrow and operational. The repository checker rejects Lake
 dependencies, proof placeholders, assumption declarations, tagged definitions,
 tagged theorems with axiom dependencies, and proof links without paired runtime