README: transparency-log section notes entry 13 (self-attestation) + leaf scope block

Deployed instance now 13 leaves; entry 13 attests the log's own
accumulator machinery; the producer emits a per-leaf scope block.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

README.md

@@ -146,6 +146,16 @@ The log uses:
 - OpenSSL Ed25519 signatures today.
 - An explicit `ML-DSA-65` / FIPS 204 signature slot that is `unavailable` unless the host has a real backend. If an agent policy requires both signatures, verification fails closed.
 
+The deployed instance ([ltl.zkdefi.org](https://ltl.zkdefi.org),
+mirror [`lean-transparency-log`](https://github.com/saymrwulf/lean-transparency-log))
+is live at **13 leaves**. Entry 13 (2026-07-16) attests the log's own
+accumulator machinery — a kernel-checked mechanization of the log's
+security analysis ([`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified)),
+appended into the log itself and scoped to the mechanized model. The
+producer path that generated it now emits a `scope` block into each leaf
+(guarantees / exclusions / deployment-constraints), so a leaf carries its
+own honest scope, not just a claim card.
+
 Example:
 
 ```bash

examples/repos.yaml

@@ -65,3 +65,159 @@ repos:
     known_exclusions:
       - full fieldImplementation certificate unless present and axiom-clean
       - production-ready Pallas arithmetic unless add/mul/reduce/square/invert are proven
+
+  - name: ltl-accumulator-verified
+    url: https://github.com/saymrwulf/ltl-accumulator-verified.git
+    kind: merkle_accumulator
+    verification_dir: verification
+    verified_backend: rfc9162-sha256/lean-model
+    env_script: ~/aeneas-toolchain/env.sh
+    lean_project_dir: $AENEAS_HOME/backends/lean
+    lean_guard: verification/lean-guard
+    known_status: >-
+      Attestation scope: this corpus kernel-checks the listed theorems about
+      the mechanized recursive accumulator model. Correspondence with the
+      deployed inclusion verifier is supported by finite differential testing
+      over the pinned families. The deployed consistency verifier is not
+      extensionally equal to the model; applying the mechanized soundness
+      result to the deployed consumer flow additionally relies on an
+      unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15).
+    known_exclusions:
+      - SHA-256 collision resistance (the single opaque boundary axiom; soundness theorems CONSTRUCT collisions)
+      - deployed-verifier extensional equality (KNOWN-GAPS 14/15 - lied-size divergence, one-sided; refinement invariant unmechanized)
+      - signature/STH layer and evidence transferability (gap 4)
+      - asymptotic cost claims (gap 9)
+    axiom_imports:
+      - Proofs.Basic
+      - Proofs.Completeness
+      - Proofs.Extract
+      - Proofs.Descent
+      - Proofs.Consistency
+      - Proofs.Binding3
+      - Proofs.Refactor
+      - Proofs.Theorem3
+      - Proofs.PinStore
+    certificates:
+      - LTLAcc.ConsRec
+      - LTLAcc.Hash
+      - LTLAcc.IsCollision
+      - LTLAcc.MTH
+      - LTLAcc.MTH_single
+      - LTLAcc.MTH_split
+      - LTLAcc.Path
+      - LTLAcc.Root
+      - LTLAcc.Root_left
+      - LTLAcc.Root_one
+      - LTLAcc.Root_one_cons
+      - LTLAcc.Root_right
+      - LTLAcc.acceptCons
+      - LTLAcc.acceptCons_sound
+      - LTLAcc.acceptIncl
+      - LTLAcc.acceptIncl_complete
+      - LTLAcc.acceptIncl_sound
+      - LTLAcc.consRecBinding
+      - LTLAcc.consRec_base_false_eq
+      - LTLAcc.consRec_base_true_eq
+      - LTLAcc.consRec_some_le
+      - LTLAcc.domsep
+      - LTLAcc.eq_dropLast_append_of_getLast?
+      - LTLAcc.exists_singleton_of_length_one
+      - LTLAcc.extractCons
+      - LTLAcc.extractConsNode
+      - LTLAcc.extractCons_correct
+      - LTLAcc.extractCons_correct_paper
+      - LTLAcc.extractCons_nonvacuous
+      - LTLAcc.extractIncl
+      - LTLAcc.extractIncl_correct
+      - LTLAcc.extractIncl_nonvacuous
+      - LTLAcc.extractMTH
+      - LTLAcc.extractMTH_correct
+      - LTLAcc.extractMTH_nonvacuous
+      - LTLAcc.fork_distinct
+      - LTLAcc.getD_drop
+      - LTLAcc.getD_take
+      - LTLAcc.hleaf
+      - LTLAcc.hnode
+      - LTLAcc.hnode_preimage_inj
+      - LTLAcc.incl_complete
+      - LTLAcc.instDecidableEqHash
+      - LTLAcc.instInhabitedHash
+      - LTLAcc.kbelow
+      - LTLAcc.kbelow_eq_of_pow2_between
+      - LTLAcc.kbelow_lt
+      - LTLAcc.kbelow_pos
+      - LTLAcc.kbelow_pow2
+      - LTLAcc.kbelow_prefix_eq
+      - LTLAcc.le_two_kbelow
+      - LTLAcc.pinAccept
+      - LTLAcc.pinAccept_monotone
+      - LTLAcc.pinExtract
+      - LTLAcc.pin_prefix_correct
+      - LTLAcc.pin_prefix_nonvacuous
+      - LTLAcc.pow2_exp_unique
+      - LTLAcc.take_all
+      - LTLAcc.take_append_drop
+      - LTLAcc.take_drop_prefix
+      - LTLAcc.take_take_le
+    certificate_axioms:
+      LTLAcc.ConsRec: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Hash: []
+      LTLAcc.IsCollision: ["LTLAcc.sha256"]
+      LTLAcc.MTH: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.MTH_single: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.MTH_split: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Path: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Root: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Root_left: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Root_one: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Root_one_cons: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.Root_right: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.acceptCons: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.acceptCons_sound: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.acceptIncl: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.acceptIncl_complete: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.acceptIncl_sound: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.consRecBinding: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.consRec_base_false_eq: ["propext", "Classical.choice", "Quot.sound"]
+      LTLAcc.consRec_base_true_eq: ["propext"]
+      LTLAcc.consRec_some_le: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.domsep: []
+      LTLAcc.eq_dropLast_append_of_getLast?: ["propext"]
+      LTLAcc.exists_singleton_of_length_one: ["propext", "Classical.choice", "Quot.sound"]
+      LTLAcc.extractCons: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractConsNode: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractCons_correct: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractCons_correct_paper: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractCons_nonvacuous: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractIncl: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractIncl_correct: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractIncl_nonvacuous: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractMTH: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractMTH_correct: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.extractMTH_nonvacuous: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.fork_distinct: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.getD_drop: ["propext", "Quot.sound"]
+      LTLAcc.getD_take: ["propext", "Quot.sound"]
+      LTLAcc.hleaf: ["LTLAcc.sha256"]
+      LTLAcc.hnode: ["LTLAcc.sha256"]
+      LTLAcc.hnode_preimage_inj: ["propext"]
+      LTLAcc.incl_complete: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.instDecidableEqHash: []
+      LTLAcc.instInhabitedHash: ["propext"]
+      LTLAcc.kbelow: ["propext", "Quot.sound"]
+      LTLAcc.kbelow_eq_of_pow2_between: ["propext", "Quot.sound"]
+      LTLAcc.kbelow_lt: ["propext", "Quot.sound"]
+      LTLAcc.kbelow_pos: ["propext", "Quot.sound"]
+      LTLAcc.kbelow_pow2: ["propext", "Quot.sound"]
+      LTLAcc.kbelow_prefix_eq: ["propext", "Quot.sound"]
+      LTLAcc.le_two_kbelow: ["propext", "Quot.sound"]
+      LTLAcc.pinAccept: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.pinAccept_monotone: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.pinExtract: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.pin_prefix_correct: ["propext", "Classical.choice", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.pin_prefix_nonvacuous: ["propext", "LTLAcc.sha256", "Quot.sound"]
+      LTLAcc.pow2_exp_unique: ["propext", "Quot.sound"]
+      LTLAcc.take_all: ["propext"]
+      LTLAcc.take_append_drop: []
+      LTLAcc.take_drop_prefix: ["propext", "Classical.choice", "Quot.sound"]
+      LTLAcc.take_take_le: ["propext", "Quot.sound"]

paper/reinvention-outline.md

@@ -0,0 +1,122 @@
+# Paper reinvention — working outline (post second ePrint rejection)
+
+Status: approved direction (operator order 2026-07-16: "entry 13 and
+paper reinvention"); this outline is the committed starting point for
+the full rewrite. Diagnosis it responds to: both external analyses
+(GPT-5.6 rejection post-mortem; round-6 reviewer aside) converge on
+POSITIONING, not correctness — five papers compressed into one, the
+novelty (trust decomposition) occupying less space than its supporting
+machinery, and the honest "components unchanged" refrain reading as
+"nothing new" in a thirty-second editorial skim.
+
+## 0. The one sentence (everything else exists to support it)
+
+> We define and instantiate a cryptographic distribution model for
+> machine-checked correctness evidence, enabling lightweight consumers
+> to obtain accountable assurance without executing the original
+> verifier — and demonstrate it end to end with a deployed log that
+> carries kernel-checked proofs of its own accountability machinery as
+> an entry in itself.
+
+The second clause is the only-this-paper claim; it becomes literally
+true at entry 13 and the paper should be finalized AFTER that append so
+the abstract can cite the live leaf.
+
+## 1. Title candidates (working)
+
+- "Accountable Distribution of Machine-Checked Correctness Evidence"
+- "Transparency for Theorem Provers: Distributing Formal Verification
+  to Consumers Who Cannot Replay It"
+- (subtitle either way): "…with a deployed log that notarizes the
+  proofs of its own machinery"
+
+"The Lean Transparency Log" becomes the *system's* name, not the
+paper's identity.
+
+## 2. Inverted structure
+
+1. **Problem.** Theorem provers solve the PRODUCTION of correctness
+   evidence; nothing standard solves scalable DISTRIBUTION and
+   CONSUMPTION by clients that cannot run the prover (no toolchain, no
+   hours of replay, no trust in the operator's word). State it as the
+   gap between "verified" and "verifiable by you."
+2. **Model.** The trust decomposition, presented abstractly:
+   (a) producer performs expensive deterministic verification once;
+   (b) the result becomes a precise attestation object (subject commit,
+   toolchain, certificates with exact assumption cones, scope);
+   (c) a transparency structure supplies persistence, consistency, and
+   equivocation-evidence; (d) consumers apply policy locally without
+   executing the verifier; (e) the residual trust is enumerated, not
+   waved at. Define the accountability property: misbehavior
+   manufactures transferable evidence.
+3. **Design space** (the section the old paper lacked). Position
+   against: reproducible replay services; succinct proofs of proof
+   checking (SNARKed kernels); checkpoint/cosigning committees;
+   witness cosigning; downloadable proof artifacts; proof-carrying
+   code; cached prover environments/containers. Axis of comparison:
+   consumer cost, operator trust, accountability (evidence on
+   misbehavior), incrementality, and what happens when the operator
+   disappears. The log wins on accountability-per-consumer-cost; be
+   honest where SNARKed checking would win (validity vs
+   accountability) and why it is not yet practical for a full kernel.
+4. **Instantiation: the LTL.** Lean 4 + Aeneas corpora as producers;
+   Ed25519 heads signed by the dogfooded verified signer
+   (self_inclusion); RFC 9162 accumulator; pin-store consumers.
+   Compressed from old §4–5; the four ed25519 subject corpora become a
+   TABLE + pointer to project documentation, not sections.
+5. **Security of the instantiation.** The mechanized model (61
+   certificates, single opaque-SHA-256 axiom, environment-derived audit
+   surface); Theorems 1–3 + Prop 1 in one page each of STATEMENT (the
+   proofs live in the repo; the paper sells the statements). Present
+   gap 14/15 as a RESULT, not a confession: the model/deployment seam
+   located, measured (3,867 one-sided divergences), fenced by pinned
+   tests, and bridged by an explicitly stated operational invariant —
+   this is what honest mechanization boundaries look like.
+6. **Exhibit A: the log attests itself.** Entry 13 as the paper's
+   demonstration: the accountability machinery's own proofs, carried by
+   the machinery, verifiable end to end by one command from a stock
+   toolchain. Include the leaf hash + head root; a reader can check
+   inclusion in seconds.
+7. **Deployment & consumers.** Live service; warden (quorum custody
+   wallet) as the internal consumer; Swiss Post e-voting PoC as the
+   prospective external consumer (dalek-family transport). Replay
+   economics (measured ~1,800 s/fork) as the cost the model amortizes.
+8. **Related work.** CT lineage (RFC 6962/9162, CONIKS, sigstore);
+   optimistic-rollup analogy (accountability-over-validity; the
+   fraud-proof reading of Theorem 3 — from
+   ltl-accumulator-verified/docs/optimistic-accountability.md);
+   proof-carrying code; reproducible builds/SLSA; in-toto.
+9. **Limitations** = the 15-gap ledger, grouped (assumption base /
+   scope lines / unmechanized bridge), each one sentence, pointer to
+   the repo ledger.
+
+## 3. What moves OUT of the paper
+
+- Ed25519 corpus construction details → project docs / possible
+  separate implementation report ("Paper C" in the GPT taxonomy).
+- Curriculum, wallet internals, agent-native surfaces → out entirely.
+- Appendix A/B verbatim-leaf material → shrink to one leaf excerpt
+  (entry 13 itself, naturally).
+- The §8 operational-history narrative → compress to the
+  retrievability-decay paragraph + one table.
+
+## 4. Sequencing & venues
+
+1. Entry 13 lands (prerequisite for the abstract's second clause).
+2. Rewrite per this outline (fresh tex, new title; old ltl.tex remains
+   hosted as the system report at /paper — versioned, not erased).
+3. arXiv (cs.CR) immediately for timestamp + citability.
+4. Venue: CPP/ITP (mechanization framing) or SCORED/SecDev
+   (supply-chain framing) or RWC talk (deployment framing) — decide
+   after the rewrite settles which face leads.
+5. All queued wording fixes (Lemma-2 specializations, fidelity =
+   pinned families, §10(i)/(v), Remark 1, pinned-pair side condition)
+   are ABSORBED by the rewrite rather than patched into the old text.
+
+## 5. Success criterion
+
+A hurried editor can answer "what is the contribution?" from the title
++ first paragraph alone, and the thought-experiment inversion holds:
+remove any single supporting component (Lean, Ed25519, RFC 9162) and
+the CLAIM survives; remove the trust-decomposition model and nothing is
+left. That is the opposite polarity of the rejected manuscript.

provider/src/pacta_provider/service.py

@@ -109,6 +109,18 @@ def build_attestation(
             "axiom_log_path": axiom.log_path if axiom else None,
             "axiom_diagnostics": axiom.diagnostics if axiom else [],
         },
+        # Scope block: the human-readable honesty carried BY THE LEAF
+        # itself (review round 6). Previously the profile's
+        # guarantees/exclusions/deployment_constraints reached only the
+        # claim card, never the published leaf — so a leaf could not
+        # carry its own scoped-claim wording (the required entry-13
+        # attestation-scope text lives in known_status →
+        # deployment_constraints). Pure text; safe to publish.
+        "scope": {
+            "guarantees": list(profile.guarantees),
+            "exclusions": list(profile.exclusions),
+            "deployment_constraints": list(profile.deployment_constraints),
+        },
         "certificates": certs,
     }
     signed = sign_attestation(unsigned, private_key, public_key)

src/pacta/lean.py

@@ -296,16 +296,7 @@ def run_axiom_audit(
             return_code = 124
     logs.write_text(output, encoding="utf-8")
     parsed = parse_axiom_output(output, certificates)
-    cert_results: list[CertificateAxiomResult] = []
+    cert_results = classify_certificates(parsed, certificates, return_code, expected_for)
-    for cert in certificates:
-        observed = parsed.get(cert, [])
-        if return_code != 0 and not observed:
-            status = "failed"
-            axiom_status = "not_checked"
-        else:
-            status = "proven" if observed or _mentions_no_axioms(output) else "unknown"
-            axiom_status = "clean" if sorted(observed) == sorted(expected_for(cert)) else "dirty"
-        cert_results.append(CertificateAxiomResult(cert, status, axiom_status, observed, expected_for(cert)))
     return AxiomAuditResult(
         attempted=True,
         ok=return_code == 0 and all(cert.axiom_status == "clean" for cert in cert_results),
@@ -316,34 +307,77 @@ def run_axiom_audit(
     )
 
 
+# Anchor lines as Lean prints them: 'Name' depends on axioms: …  /
+# 'Name' does not depend on any axioms. The name is captured between the
+# first pair of quotes (an identifier that itself CONTAINS a quote, e.g.
+# Foo', would mis-capture — no such name exists on this estate; the old
+# substring matching was strictly worse).
+_AXIOM_ANCHOR = re.compile(r"'([^']+)'\s+(depends on axioms|does not depend on any axioms)")
+
+
 def parse_axiom_output(output: str, certificates: list[str]) -> dict[str, list[str]]:
-    results: dict[str, list[str]] = {}
+    """Record-scoped parsing (review round 6, GPT §6 / Claude R6-B).
+
+    The output is split into RECORDS: each anchor line starts one, the
+    next anchor line ends it. A cone bracket is accepted only inside its
+    own record; a record whose bracket is missing or truncated yields a
+    MISSING certificate (fail closed at the caller), never a bracket
+    borrowed from the next record. Cones may wrap arbitrarily many lines
+    (the ed25519 apex tiers carry 11 axioms — the old fixed 16-line
+    window was a latent overflow for them). Duplicate anchors: first one
+    wins, deterministically.
+    """
     lines = output.splitlines()
-    for cert in certificates:
+    anchors: list[tuple[int, str, bool]] = []  # (line index, name, axiom-free?)
-        cert_results: list[str] | None = None
+    for i, line in enumerate(lines):
-        for i, line in enumerate(lines):
+        m = _AXIOM_ANCHOR.search(line)
-            if cert not in line:
+        if m:
-                continue
+            anchors.append((i, m.group(1), "does not depend" in m.group(2)))
-            # Lean wraps long axiom lists (the apex tiers carry 11 axioms)
+    wanted = set(certificates)
-            # across many lines; take a window wide enough for the largest
+    results: dict[str, list[str]] = {}
-            # documented boundary and flatten it before matching, the same
+    for k, (i, name, axiom_free) in enumerate(anchors):
-            # move the corpus' check scripts make (tr '\n' ' ').
+        if name not in wanted or name in results:
-            window = "\n".join(lines[i : i + 16])
+            continue
-            bracket = re.search(r"\[([^\]]*)\]", window, re.DOTALL)
+        if axiom_free:
-            if bracket:
+            results[name] = []
-                cert_results = [item.strip() for item in bracket.group(1).split(",") if item.strip()]
+            continue
-                break
+        end = anchors[k + 1][0] if k + 1 < len(anchors) else len(lines)
-            if _mentions_no_axioms(window):
+        record = "\n".join(lines[i:end])
-                cert_results = []
+        bracket = re.search(r"\[([^\]]*)\]", record, re.DOTALL)
-                break
+        if bracket:
-        if cert_results is not None:
+            results[name] = [item.strip() for item in bracket.group(1).split(",") if item.strip()]
-            results[cert] = cert_results
+        # else: no complete bracket before the next record — leave MISSING.
     return results
 
 
-def _mentions_no_axioms(text: str) -> bool:
+def classify_certificates(
-    lowered = text.lower()
+    parsed: dict[str, list[str]],
-    return "no axioms" in lowered or "does not depend on any axioms" in lowered
+    certificates: list[str],
+    return_code: int,
+    expected_for,
+) -> list[CertificateAxiomResult]:
+    """Fail-closed per-certificate classification (review round 6, R6-B1).
+
+    Provenness is decided by the certificate's OWN anchor having been
+    found (membership in `parsed` — which includes axiom-free certs as
+    []), never by a whole-output "no axioms" sentence: an ABSENT
+    axiom-free certificate previously scored proven+clean because some
+    OTHER certificate's bracketless sentence satisfied the global check
+    and [] == [] satisfied the cone comparison. Absent certificates are
+    never clean.
+    """
+    out: list[CertificateAxiomResult] = []
+    for cert in certificates:
+        if cert in parsed:
+            observed = parsed[cert]
+            status = "proven"
+            axiom_status = "clean" if sorted(observed) == sorted(expected_for(cert)) else "dirty"
+        else:
+            observed = []
+            status = "failed" if return_code != 0 else "unknown"
+            axiom_status = "not_checked"
+        out.append(CertificateAxiomResult(cert, status, axiom_status, observed, expected_for(cert)))
+    return out
 
 
 def _version(cmd: list[str | None], env: dict[str, str] | None = None) -> str | None:

tests/test_lean.py

@@ -24,6 +24,107 @@ def test_parse_axiom_output_no_axioms_wording():
     assert parsed["CurveFieldProofs.fieldImplementation"] == []
 
 
+def test_parse_axiom_output_axiom_free_cert_does_not_steal_next_cone():
+    # Regression (found by the entry-13 rehearsal, 2026-07-16): an
+    # axiom-free certificate is followed by a cone-carrying one. The old
+    # windowed search reached past the bracketless "does not depend"
+    # sentence and attributed the NEXT certificate's cone. The
+    # accumulator corpus is the first subject with axiom-free
+    # certificates (domsep, Hash, instDecidableEqHash, take_append_drop),
+    # so no fork attestation ever exercised this path.
+    output = (
+        "'LTLAcc.domsep' does not depend on any axioms\n"
+        "'LTLAcc.eq_dropLast_append_of_getLast?' depends on axioms: [propext]\n"
+    )
+    parsed = parse_axiom_output(output, ["LTLAcc.domsep", "LTLAcc.eq_dropLast_append_of_getLast?"])
+    assert parsed["LTLAcc.domsep"] == []
+    assert parsed["LTLAcc.eq_dropLast_append_of_getLast?"] == ["propext"]
+
+
+def test_classify_absent_axiom_free_cert_is_not_clean():
+    # Regression (round-6 Claude R6-B1, executed end-to-end by the
+    # reviewer): domsep's line deleted from otherwise-pristine output
+    # still yielded 61/61 because a whole-output "no axioms" sentence +
+    # ([] == []) scored the ABSENT cert proven+clean. Provenness must be
+    # the cert's own anchor, i.e. membership in the parsed dict.
+    from pacta.lean import classify_certificates
+
+    output = (
+        "'LTLAcc.Hash' does not depend on any axioms\n"
+        "'LTLAcc.MTH' depends on axioms: [propext, LTLAcc.sha256, Quot.sound]\n"
+    )
+    certs = ["LTLAcc.Hash", "LTLAcc.domsep", "LTLAcc.MTH"]
+    parsed = parse_axiom_output(output, certs)
+    results = classify_certificates(parsed, certs, 0, lambda c: [])
+    by_name = {r.name: r for r in results}
+    assert by_name["LTLAcc.Hash"].status == "proven"
+    assert by_name["LTLAcc.domsep"].status == "unknown"
+    assert by_name["LTLAcc.domsep"].axiom_status == "not_checked"
+    assert not all(r.axiom_status == "clean" for r in results)
+
+
+def test_parse_missing_bracket_does_not_steal_next_record():
+    # GPT round-6 §6: a cone-bearing anchor with a MISSING bracket must
+    # not consume the next certificate's bracket.
+    output = (
+        "'A.a' depends on axioms:\n"
+        "'B.b' depends on axioms: [propext]\n"
+    )
+    parsed = parse_axiom_output(output, ["A.a", "B.b"])
+    assert "A.a" not in parsed
+    assert parsed["B.b"] == ["propext"]
+
+
+def test_parse_truncated_cone_is_missing():
+    output = "'A.a' depends on axioms: [propext, Classical.choice\n"
+    parsed = parse_axiom_output(output, ["A.a"])
+    assert "A.a" not in parsed
+
+
+def test_parse_long_wrapped_cone_beyond_old_window():
+    # The ed25519 apex tiers carry 11 axioms; the old fixed 16-line
+    # window was a latent overflow. Records now extend to the next
+    # anchor regardless of length.
+    items = [f"Ax{i}" for i in range(11)]
+    wrapped = "[\n" + ",\n".join(items) + "\n" * 10 + "]"
+    output = f"'A.a' depends on axioms: {wrapped}\n'B.b' does not depend on any axioms\n"
+    parsed = parse_axiom_output(output, ["A.a", "B.b"])
+    assert parsed["A.a"] == items
+    assert parsed["B.b"] == []
+
+
+def test_parse_duplicate_anchor_first_wins():
+    output = (
+        "'A.a' depends on axioms: [propext]\n"
+        "'A.a' depends on axioms: [Quot.sound]\n"
+    )
+    parsed = parse_axiom_output(output, ["A.a"])
+    assert parsed["A.a"] == ["propext"]
+
+
+def test_parse_interleaved_diagnostics_inside_record():
+    output = (
+        "'A.a' depends on axioms:\n"
+        "warning: something unrelated\n"
+        "[propext, Quot.sound]\n"
+        "'B.b' does not depend on any axioms\n"
+    )
+    parsed = parse_axiom_output(output, ["A.a", "B.b"])
+    assert parsed["A.a"] == ["propext", "Quot.sound"]
+    assert parsed["B.b"] == []
+
+
+def test_parse_axiom_output_exact_name_not_prefix():
+    # 'LTLAcc.MTH' must not match the line for 'LTLAcc.MTH_single' even
+    # when the latter comes first in the output.
+    output = (
+        "'LTLAcc.MTH_single' depends on axioms: [propext, LTLAcc.sha256, Quot.sound]\n"
+        "'LTLAcc.MTH' depends on axioms: [propext, LTLAcc.sha256, Quot.sound]\n"
+    )
+    parsed = parse_axiom_output(output, ["LTLAcc.MTH"])
+    assert parsed["LTLAcc.MTH"] == ["propext", "LTLAcc.sha256", "Quot.sound"]
+
+
 def test_mac_safe_lean_command_is_argument_list():
     tools = LeanTools(lean="/usr/local/bin/lean", lake=None)
     cmd = build_lean_invocation(Path("Proofs/A.lean"), tools, output_path=Path("Proofs/A.olean"), root_path=Path("."))

tests/test_provider.py

@@ -49,3 +49,42 @@ def test_provider_builds_signed_attestation_for_fixture(tmp_path):
     )
     assert attestation["signature"]["status"] == "signed"
     assert attestation["certificates"][0]["status"] == "proven"
+    # The leaf carries its own scope block (review round 6): the
+    # profile's guarantees/exclusions/deployment_constraints must reach
+    # the published leaf, not only the claim card.
+    assert "scope" in attestation
+    for key in ("guarantees", "exclusions", "deployment_constraints"):
+        assert key in attestation["scope"]
+
+
+def test_attestation_scope_carries_repo_known_status_and_exclusions(tmp_path):
+    # A repo's known_status (scoped-claim wording) and known_exclusions
+    # must land in the leaf's scope block. Regression for the entry-13
+    # requirement that the leaf itself carry its scoped attestation text.
+    private_key = tmp_path / "provider.key"
+    public_key = tmp_path / "provider.pub"
+    generate_ed25519_keypair(private_key, public_key)
+    repo = RepoConfig(
+        name="dalek-ed25519-verified",
+        url="https://github.com/saymrwulf/dalek-ed25519-verified.git",
+        kind="ed25519",
+        verification_dir="verification",
+        verified_backend="serial/u64",
+        certificates=["CurveFieldProofs.fieldImplementation"],
+        axiom_imports=["Proofs.FieldMain"],
+        expected_axioms=[],
+        known_status="SCOPE MARKER: mechanized model only, not the deployed verifier.",
+        known_exclusions=["EXCLUSION MARKER: side-channel resistance"],
+    )
+    attestation = build_attestation(
+        repo,
+        Path("tests/fixtures/mini-ed25519-verified"),
+        provider="local-test-provider",
+        private_key=private_key,
+        public_key=public_key,
+        timeout=30,
+        log_dir=tmp_path / "logs",
+    )
+    scope = attestation["scope"]
+    assert any("SCOPE MARKER" in c for c in scope["deployment_constraints"])
+    assert any("EXCLUSION MARKER" in e for e in scope["exclusions"])