diff --git a/CHANGELOG.md b/CHANGELOG.md
index 110a22277..2ab02a704 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -74,6 +74,14 @@ date when the release is tagged.
 - **Check and render.** One reused converter reads every page, and each linked
   path is resolved once per run, so `check` uses about a fifth less CPU on an
   1,806-article vault; neither command's output changes (#415).
+- **Large skeletons.** Packets, the report, and the check that guards their
+  publication are hashed and written in pieces, so writing a large report no
+  longer holds every packet in memory, and shared closure material is no longer
+  parsed and escaped again for every root; output bytes and hashes are unchanged.
+  `skeleton` names each phase on stderr as it starts (`skeleton: probing <n>
+  modules...`, then `assembling` once no probe runs, then `writing`). Agent
+  Review and Formalize say what a user's pause of skeleton evidence during proof
+  development still requires (#497).
 - **Builds.** `project new` turns on Lake's artifact cache with
   `enableArtifactCache` and `restoreAllArtifacts`, so checkouts and worktrees
   on one toolchain reuse each other's builds; Setup offers the same two lines
diff --git a/autoform_cli/README.md b/autoform_cli/README.md
index da5d7ff85..6d165d79c 100644
--- a/autoform_cli/README.md
+++ b/autoform_cli/README.md
@@ -587,6 +587,10 @@ check, the helper's build, and each probe have their own 600-second budget;
 run at a time. These limits are resource controls, not a security or
 authenticity boundary.
 
+Each phase is named on stderr as it starts: `skeleton: probing <n> modules...`
+when Lean probes start, `skeleton: assembling...` once none runs (the build must
+still not change), and `skeleton: writing...` before `--output` or `--packets`.
+
 `--packets DIR` writes one comment-stripped packet per skeleton, named after
 its article and declaration, with a manifest of articles and hashes; a blind
 auditor gets the hash-named packets of `review prepare` instead. The
diff --git a/autoform_cli/__main__.py b/autoform_cli/__main__.py
index d3b3e6e1d..e71e59642 100644
--- a/autoform_cli/__main__.py
+++ b/autoform_cli/__main__.py
@@ -3,6 +3,7 @@
 from __future__ import annotations
 
 import argparse
+import contextlib
 import hashlib
 import json
 import os
@@ -1754,22 +1755,37 @@ def _skeleton(args: argparse.Namespace) -> int:
             print("error: --output must be disjoint from packet and passage directories", file=sys.stderr)
             return 2
     stream = sys.stderr if args.json else sys.stdout
+
+    def progress(phase: str) -> None:
+        # Information only. Without fd 2, print(file=None) would write to stdout,
+        # and a line left in a broken stderr's buffer would fail the exit-time flush.
+        if sys.stderr is None:
+            return
+        try:
+            print(f"skeleton: {phase}...", file=sys.stderr, flush=True)
+        except OSError:
+            with contextlib.suppress(OSError, ValueError):
+                os.dup2(os.open(os.devnull, os.O_WRONLY), sys.stderr.fileno())
+
     try:
         report = extract_skeletons(
             args.blueprint_dir,
             lean_root=args.lean_root,
             timeout=args.timeout,
             node_ids=tuple(args.nodes) if args.nodes else None,
+            progress=progress,
         )
         if args.packets is not None and not report.clean:
             print("error: refusing to publish review packets from an incomplete skeleton report", file=sys.stderr)
         elif args.packets is not None:
+            progress("writing")
             written = write_packets(report, args.packets, passages=args.passages, report_path=args.output)
             print(f"{args.packets}: {len(written)} blind packet(s) written", file=stream)
             if args.passages is not None:
                 cited = sum(1 for node in report.nodes if node.passage is not None)
                 print(f"{args.passages}: {cited} source passage(s) written", file=stream)
         if args.output is not None and (args.packets is None or not report.clean):
+            progress("writing")
             write_skeleton_report(report, args.output)
     except SkeletonError as exc:
         for issue in exc.issues:
@@ -1784,7 +1800,9 @@ def _skeleton(args: argparse.Namespace) -> int:
         for issue in report.unresolved:
             print(f"error: {issue.message}", file=stream)
     elif args.json:
-        print(report.to_json())
+        # In pieces, as `--output` writes it: a large report need not be held twice.
+        sys.stdout.writelines(report._json_pieces())
+        sys.stdout.write("\n")
     else:
         print(format_report(report, lean_root=args.lean_root), end="")
     return 0 if report.clean else 1
diff --git a/autoform_cli/_managed_output.py b/autoform_cli/_managed_output.py
index 75984d9c2..77d2784f7 100644
--- a/autoform_cli/_managed_output.py
+++ b/autoform_cli/_managed_output.py
@@ -27,6 +27,7 @@
 import sys
 import tempfile
 import warnings
+from collections.abc import Iterable
 from pathlib import Path
 
 from ._tree_snapshot import _normalized_name
@@ -60,7 +61,12 @@ def output_identity(path: Path) -> tuple[int, int, str] | None:
             if child.is_dir():
                 digest.update(b"directory\0")
             elif child.is_file():
-                digest.update(b"file\0" + child.read_bytes() + b"\0")
+                # In blocks: one packet of a large closure can be gigabytes.
+                digest.update(b"file\0")
+                with child.open("rb") as stream:
+                    while block := stream.read(1 << 20):
+                        digest.update(block)
+                digest.update(b"\0")
             else:
                 raise SkeletonError([f"refusing special file in packet output: {child}"])
     except OSError as exc:
@@ -101,9 +107,13 @@ def validate_managed_output(path: Path, *, kind: str, schema: str | None = None)
     return identity
 
 
-def stage_output(destination: Path, content: str | None = None, *, stages: list[Path] | None = None) -> Path:
+def stage_output(
+    destination: Path, content: str | Iterable[str] | None = None, *, stages: list[Path] | None = None
+) -> Path:
     """Create a same-directory stage, a directory or a file of ``content``, with the old mode.
 
+    ``content`` may come in pieces, which are written as they come.
+
     With ``stages``, the stage is registered there before it is created, so
     whoever owns ``stages`` removes it however this call or a later step ends.
     Without, a stage this call cannot finish is removed before the error leaves.
@@ -130,7 +140,7 @@ def stage_output(destination: Path, content: str | None = None, *, stages: list[
     try:
         if stream is not None:
             with stream:
-                stream.write(content)
+                stream.writelines((content,) if isinstance(content, str) else content)
                 stream.flush()
                 os.fsync(stream.fileno())
         if mode is not None:
diff --git a/autoform_cli/skeleton.py b/autoform_cli/skeleton.py
index 7af65a54a..2a7a406dc 100644
--- a/autoform_cli/skeleton.py
+++ b/autoform_cli/skeleton.py
@@ -97,7 +97,9 @@
 detected before commit aborts publication instead of being overwritten.
 Combined, they are staged together and a failed commit restores the previous
 set: failure atomicity, not simultaneous visibility, since each rename is
-atomic on its own.
+atomic on its own. Packets, the report, and the trees' identities are hashed
+and written in pieces: a joint packet repeats every closure in its article, and
+can be gigabytes.
 
 Passages. A ``## Sources`` link with a ``#L<start>-L<end>`` fragment that names
 a regular Markdown file in the blueprint, in any letter case, is a note; any
@@ -130,12 +132,13 @@
 import contextlib
 import errno
 import hashlib
+import itertools
 import json
 import os
 import re
 import stat
 import time
-from collections.abc import Callable
+from collections.abc import Callable, Iterable, Iterator
 from dataclasses import asdict, dataclass, fields
 from dataclasses import field as dataclass_field
 from pathlib import Path
@@ -258,8 +261,9 @@ class DeclarationSkeleton(TrustedDeclaration):
     statement: str | None = None
     #: UTF-8 byte ranges of the comments in ``statement``.
     statement_comments: tuple[tuple[int, int], ...] = ()
-    #: Hashes and packet text, each computed once: a report states them
-    #: several times, and each fingerprint encodes the whole trusted closure.
+    #: Hashes, each computed once: a report states them several times, and
+    #: each fingerprint encodes the whole trusted closure. The packet text is
+    #: streamed instead, since a large closure makes it gigabytes.
     _cache: dict[str, str] = dataclass_field(default_factory=dict, init=False, repr=False, compare=False)
 
     @property
@@ -304,8 +308,7 @@ def hash(self) -> str:
         """Fingerprint the probe's canonical elaborated meaning and trust boundary."""
 
         if "hash" not in self._cache:
-            modules = {module for module, _, _ in self.boundary_modules}
-            self._cache["hash"] = self._fingerprint(self.trusted, self.assumed, modules, axioms=True)
+            self._fingerprints({})
         return self._cache["hash"]
 
     @property
@@ -314,14 +317,34 @@ def statement_hash(self) -> str:
         and what only they reach. Unlike :attr:`hash`, editing only a theorem's
         proof, ``sorry`` to a proof included, leaves it unchanged."""
 
+        if "statement_hash" not in self._cache:
+            self._fingerprints({})
+        return self._cache["statement_hash"]
+
+    def _fingerprints(self, escaped: dict[str, bytes]) -> None:
+        """Compute :attr:`hash` and :attr:`statement_hash`, escaping each string
+        once per ``escaped``, which roots that share a closure can share."""
+
+        if "hash" not in self._cache:
+            modules = {module for module, _, _ in self.boundary_modules}
+            self._cache["hash"] = self._fingerprint(self.trusted, self.assumed, modules, axioms=True, escaped=escaped)
         if "statement_hash" not in self._cache:
             self._cache["statement_hash"] = self._fingerprint(
-                self.statement_trusted, self.statement_assumed, set(self.statement_boundary_modules), axioms=False
+                self.statement_trusted,
+                self.statement_assumed,
+                set(self.statement_boundary_modules),
+                axioms=False,
+                escaped=escaped,
             )
-        return self._cache["statement_hash"]
 
     def _fingerprint(
-        self, trusted: tuple[TrustedDeclaration, ...], assumed: tuple[str, ...], modules: set[str], *, axioms: bool
+        self,
+        trusted: tuple[TrustedDeclaration, ...],
+        assumed: tuple[str, ...],
+        modules: set[str],
+        *,
+        axioms: bool,
+        escaped: dict[str, bytes],
     ) -> str:
         names = set(assumed)
         material = {
@@ -338,14 +361,17 @@ def _fingerprint(
         }
         if axioms:
             material |= {"axioms": list(self.axioms), "axiom_semantics": [list(item) for item in self.axiom_semantics]}
-        return _sha256_id(json.dumps(material, sort_keys=True, ensure_ascii=False).encode())
+        digest = hashlib.sha256()
+        for piece in _json_utf8(material, escaped):
+            digest.update(piece)
+        return f"sha256:{digest.hexdigest()}"
 
     @property
     def evidence_hash(self) -> str:
         """Fingerprint the exact proof-free text presented to a reviewer."""
 
         if "evidence_hash" not in self._cache:
-            self._cache["evidence_hash"] = _sha256_id(self.blind_text().encode("utf-8"))
+            self._cache["evidence_hash"] = _sha256_pieces(self._packet())
         return self._cache["evidence_hash"]
 
     def blind_text(self) -> str:
@@ -361,45 +387,36 @@ def blind_text(self) -> str:
         unless it decides whether an equation-style statement can be cut at all.
         """
 
-        if "packet" not in self._cache:
-            self._cache["packet"] = self._packet()
-        return self._cache["packet"]
-
-    def _packet(self) -> str:
-        lines = [
-            f"-- {self.kind} {self.name}",
-            f"-- assumed from libraries: {', '.join(self.statement_assumed) or 'none'}",
-            "",
-            self.signature,
-            "-- raw signature:",
-            self.raw_signature,
-            f"-- canonical kernel material: {self.semantic}",
-        ]
+        return "".join(self._packet())
+
+    def _packet(self) -> Iterator[str]:
+        """The packet in pieces, each line followed by its newline, so the
+        kernel material is never copied into one string."""
+
+        yield f"-- {self.kind} {self.name}\n"
+        yield f"-- assumed from libraries: {', '.join(self.statement_assumed) or 'none'}\n\n"
+        yield from (self.signature, "\n-- raw signature:\n", self.raw_signature, "\n")
+        yield from ("-- canonical kernel material: ", self.semantic, "\n")
         own = _without_comments(self.source or "", self.source_comments).strip("\n")
         if own:
-            lines.append(own)
+            yield own + "\n"
         elif self.statement:
             written = _without_comments(self.statement, self.statement_comments).strip("\n")
             if written:
-                lines += ["-- as written:", written]
+                yield f"-- as written:\n{written}\n"
         if self.source_withheld or not (own or self.statement):
-            lines.append(_NOT_SHOWN)
+            yield _NOT_SHOWN + "\n"
         for item in self.statement_trusted:
             body = _without_comments(item.source or "", item.source_comments).strip("\n")
             # The elaborated signature restores what `variable` binders and
             # `open` leave implicit in the source, such as the type of `S`.
-            lines += [
-                "",
-                f"-- {item.kind} {item.name}",
-                f"-- signature: {item.signature}",
-                f"-- raw signature: {item.raw_signature}",
-                f"-- canonical kernel material: {item.semantic}",
-            ]
+            yield f"\n-- {item.kind} {item.name}\n"
+            yield from ("-- signature: ", item.signature, "\n-- raw signature: ", item.raw_signature, "\n")
+            yield from ("-- canonical kernel material: ", item.semantic, "\n")
             if body:
-                lines.append(body)
+                yield body + "\n"
             elif item.source_withheld:
-                lines.append(_NOT_SHOWN)
-        return "\n".join(lines) + "\n"
+                yield _NOT_SHOWN + "\n"
 
     def as_dict(self) -> dict[str, object]:
         """The report record, naming what the report's shared tables state once."""
@@ -458,9 +475,13 @@ def blind_text(self) -> str:
         alone.
         """
 
-        parts = [f"-- article with {len(self.declarations)} declaration(s)"]
-        parts += [declaration.blind_text() for declaration in self.declarations]
-        return "\n".join(parts)
+        return "".join(self._packet())
+
+    def _packet(self) -> Iterator[str]:
+        yield f"-- article with {len(self.declarations)} declaration(s)"
+        for declaration in self.declarations:
+            yield "\n"
+            yield from declaration._packet()
 
     @property
     def hash(self) -> str | None:
@@ -478,7 +499,7 @@ def evidence_hash(self) -> str:
         """Fingerprint the exact joint packet presented to a reviewer."""
 
         if "evidence_hash" not in self._cache:
-            self._cache["evidence_hash"] = _sha256_id(self.blind_text().encode("utf-8"))
+            self._cache["evidence_hash"] = _sha256_pieces(self._packet())
         return self._cache["evidence_hash"]
 
     @property
@@ -670,7 +691,12 @@ def _record(self, tables: _Tables) -> dict[str, object]:
         }
 
     def to_json(self) -> str:
-        return json.dumps(self._record(self._tables), sort_keys=True, separators=(",", ":"), ensure_ascii=False)
+        return _REPORT_JSON.encode(self._record(self._tables))
+
+    def _json_pieces(self) -> Iterator[str]:
+        """:meth:`to_json` in pieces, for a report too large to hold twice."""
+
+        return _REPORT_JSON.iterencode(self._record(self._tables))
 
 
 def _share(table: dict[str, object], name: str, value: object, *, table_name: str) -> None:
@@ -682,6 +708,45 @@ def _sha256_id(content: bytes) -> str:
     return f"sha256:{hashlib.sha256(content).hexdigest()}"
 
 
+def _sha256_pieces(pieces: Iterable[str]) -> str:
+    """The :func:`_sha256_id` of the UTF-8 text ``pieces`` join to, without joining them."""
+
+    digest = hashlib.sha256()
+    for piece in pieces:
+        digest.update(piece.encode("utf-8"))
+    return f"sha256:{digest.hexdigest()}"
+
+
+#: The report's spelling; its ``iterencode`` writes what ``encode`` returns, in pieces.
+_REPORT_JSON = json.JSONEncoder(sort_keys=True, separators=(",", ":"), ensure_ascii=False)
+
+
+def _json_utf8(value: object, escaped: dict[str, bytes]) -> Iterator[bytes]:
+    """``json.dumps(value, sort_keys=True, ensure_ascii=False)`` in UTF-8 pieces,
+    for a value of strings, lists, and dicts, escaping each string once per ``escaped``."""
+
+    if isinstance(value, str):
+        piece = escaped.get(value)
+        if piece is None:
+            piece = escaped[value] = json.encoder.encode_basestring(value).encode("utf-8")
+        yield piece
+    elif isinstance(value, list):
+        yield b"["
+        for index, item in enumerate(value):
+            if index:
+                yield b", "
+            yield from _json_utf8(item, escaped)
+        yield b"]"
+    elif isinstance(value, dict):
+        yield b"{"
+        for index, (key, item) in enumerate(sorted(value.items())):
+            yield from (b", " if index else b"", *_json_utf8(key, escaped), b": ")
+            yield from _json_utf8(item, escaped)
+        yield b"}"
+    else:
+        raise TypeError(f"cannot fingerprint {type(value).__name__}")
+
+
 def _without_comments(text: str, comments: tuple[tuple[int, int], ...]) -> str:
     """Blank the comment ranges Lean found without joining surrounding tokens."""
 
@@ -1059,7 +1124,7 @@ def _require_probe_source(value: object, *, kind: str, context: str) -> None:
         raise SkeletonError([f"the skeleton probe emitted proof-bearing source for {context}"])
 
 
-def _probe_record_issue(record: dict[str, object]) -> str | None:
+def _probe_record_issue(record: dict[str, object], *, safe: set[int] | None = None) -> str | None:
     """Why a validated probe record cannot yield a skeleton, confined to its node.
 
     A declaration whose source cannot be located leaves nothing faithful to
@@ -1068,17 +1133,22 @@ def _probe_record_issue(record: dict[str, object]) -> str | None:
     (for example, a statement that uses `local notation`) is only withheld: the
     signatures and canonical kernel material still state its meaning. A
     partial root or trusted dependency has no kernel meaning to bind, so its
-    node is refused as well.
+    node is refused as well. ``safe`` holds the ids of shared records already
+    found safe, so each is parsed once however many roots trust it.
     """
 
     root = str(record["root"])
     trusted = record["trusted"]
     assert isinstance(trusted, list)
+    safe = set() if safe is None else safe
     safety = [(root, record)] + [(str(item.get("source_name") or ""), item) for item in trusted]
     for source_name, item in safety:
+        if id(item) in safe:
+            continue
         issue = _local_safety_issue(source_name, str(item["semantic"]))
         if issue is not None:
             return issue
+        safe.add(id(item))
     entries = [(root, root, record)]
     entries += [(str(item["name"]), f"{root} trusted declaration {item['name']}", item) for item in trusted]
     for name, context, item in entries:
@@ -1299,6 +1369,7 @@ def extract_skeletons(
     runner: ProbeRunner | None = None,
     node_ids: tuple[str, ...] | None = None,
     timeout: float | None = None,
+    progress: Callable[[str], None] | None = None,
 ) -> SkeletonReport:
     """Extract the skeleton of every ``lean:`` declaration the blueprint names.
 
@@ -1311,7 +1382,8 @@ def extract_skeletons(
     so it cannot be combined with ``timeout``, and may be called from several
     threads at once. A declaration the lexical index cannot place is reported
     as unresolved without running Lean, exactly as
-    ``autoform check --lean-root`` reports it.
+    ``autoform check --lean-root`` reports it. ``progress`` hears each phase as
+    it starts, as :func:`extract_graph_skeletons` says.
     """
 
     if runner is not None and timeout is not None:
@@ -1337,7 +1409,14 @@ def extract_skeletons(
         probing, runner = lean_probe.default_runner(root, timeout=DEFAULT_PROBE_TIMEOUT if timeout is None else timeout)
 
     report = extract_graph_skeletons(
-        graph, lean_root=root, libraries=libraries, index=index, runner=runner, node_ids=node_ids, probing=probing
+        graph,
+        lean_root=root,
+        libraries=libraries,
+        index=index,
+        runner=runner,
+        node_ids=node_ids,
+        probing=probing,
+        progress=progress,
     )
     current = check_inputs_unchanged(graph, root, index, inputs, activity=activity)
     if _blueprint_hash(current, _source_passages(current)) != report.blueprint_hash:
@@ -1460,12 +1539,15 @@ def extract_graph_skeletons(
     runner: ProbeRunner,
     node_ids: tuple[str, ...] | None = None,
     probing: Callable[[tuple[str, ...]], contextlib.AbstractContextManager[object]] | None = None,
+    progress: Callable[[str], None] | None = None,
 ) -> SkeletonReport:
     """Extract skeletons for an already loaded graph.
 
     ``probing``, when given, is entered with every module about to be probed and
     held while the probes run, and only then; the default runner's freshness
     check, helper build, scratch directory and signal guard live there.
+    ``progress``, when given, hears ``probing <n> modules`` before any module
+    is probed, ``probing`` included, and ``assembling`` once no probe runs.
     """
 
     targets, selected, selection = select_lean_targets(graph, node_ids)
@@ -1511,6 +1593,8 @@ def extract_graph_skeletons(
             for module in sorted(groups)
         }
         snapshot_started_ns = time.time_ns()
+        if progress is not None:
+            progress(f"probing {_plural(len(programs), 'module')}")
 
         def probe(module: str) -> dict[str, dict[str, object]]:
             # Parsed in the worker, as soon as the probe ends.
@@ -1528,8 +1612,13 @@ def probe(module: str) -> dict[str, dict[str, object]]:
             else:
                 records.update(result)
 
+    if progress is not None:
+        progress("assembling")
     nodes: list[NodeSkeleton] = []
     module_hashes: dict[tuple[str, str], str] = {}
+    # A probe states each shared record once; these keep it read once, by id.
+    safe: set[int] = set()
+    shared: dict[int, TrustedDeclaration] = {}
     for node, names in selected:
         declarations: list[DeclarationSkeleton] = []
         for name in names:
@@ -1563,7 +1652,7 @@ def probe(module: str) -> dict[str, dict[str, object]]:
                 reason = f"Lean declares it in module {record.get('module')}, not in {module} where its source was found"
                 unresolved.append(UnresolvedTarget(node.id, name, reason))
                 continue
-            issue = _probe_record_issue(record)
+            issue = _probe_record_issue(record, safe=safe)
             if issue is not None:
                 unresolved.append(UnresolvedTarget(node.id, name, issue))
                 continue
@@ -1575,6 +1664,7 @@ def probe(module: str) -> dict[str, dict[str, object]]:
                     index=index,
                     module_hashes=module_hashes,
                     snapshot_started_ns=snapshot_started_ns,
+                    shared=shared,
                 )
             )
         passage, locator, _ = passages[node.id]
@@ -1588,6 +1678,11 @@ def probe(module: str) -> dict[str, dict[str, object]]:
                 complete={item.name for item in declarations} == set(names),
             )
         )
+    # Roots share most of their closures, so each string is escaped once for all their fingerprints.
+    escaped: dict[str, bytes] = {}
+    for item in nodes:
+        for declaration in item.declarations:
+            declaration._fingerprints(escaped)
     return SkeletonReport(
         blueprint_hash=_blueprint_hash(graph, passages),
         targets=tuple((node.id, names) for node, names in targets),
@@ -1747,8 +1842,13 @@ def _declaration(
     index: SourceIndex,
     module_hashes: dict[tuple[str, str], str],
     snapshot_started_ns: int | None,
+    shared: dict[int, TrustedDeclaration],
 ) -> DeclarationSkeleton:
-    trusted = [_trusted(item, libraries=libraries, lean_root=lean_root, index=index) for item in record["trusted"]]
+    trusted: list[TrustedDeclaration] = []
+    for item in record["trusted"]:  # type: ignore[attr-defined]
+        if id(item) not in shared:
+            shared[id(item)] = _trusted(item, libraries=libraries, lean_root=lean_root, index=index)
+        trusted.append(shared[id(item)])
     name = str(record["root"])
     module = str(record["module"])
     start, end = record["range"] or (None, None)
@@ -1968,7 +2068,7 @@ def _stage_report_output(report: SkeletonReport, destination: Path) -> tuple[Pat
     identity = output_identity(destination)
     if identity is not None and not destination.is_file():
         raise SkeletonError([f"report output exists and is not a regular file: {destination}"])
-    return stage_output(destination, report.to_json() + "\n"), identity
+    return stage_output(destination, itertools.chain(report._json_pieces(), "\n")), identity
 
 
 def _paths_overlap(first: Path, second: Path) -> bool:
@@ -2054,8 +2154,9 @@ def write_packets(
     manifest: list[dict[str, str]] = []
     passage_manifest: list[dict[str, str]] = []
     # Written after the manifests: a capture that lists a stage before its
-    # marker is complete then finds no folder to descend into.
-    files: list[tuple[Path, str | bytes]] = []
+    # marker is complete then finds no folder to descend into. Packets are
+    # streamed, so no packet is held whole.
+    files: list[tuple[Path, bytes | Iterable[str]]] = []
     try:
         packet_stage = stage_output(root)
         passages_stage = stage_output(passages_root) if passages_root is not None else None
@@ -2078,11 +2179,11 @@ def write_packets(
                 )
             article_relative = node_path / ARTICLE_PACKET
             if node.declarations:
-                files.append((packet_stage / article_relative, node.blind_text()))
+                files.append((packet_stage / article_relative, node._packet()))
                 written.append(root / article_relative)
             for declaration in node.declarations:
                 relative = node_path / declaration_filename(declaration.name)
-                files.append((packet_stage / relative, declaration.blind_text()))
+                files.append((packet_stage / relative, declaration._packet()))
                 written.append(root / relative)
                 entry = {
                     "article_packet": article_relative.as_posix(),
@@ -2111,8 +2212,9 @@ def write_packets(
             path.parent.mkdir(parents=True, exist_ok=True)
             if isinstance(content, bytes):
                 path.write_bytes(content)
-            else:
-                path.write_text(content, encoding="utf-8")
+                continue
+            with path.open("w", encoding="utf-8") as stream:
+                stream.writelines(content)
         outputs = [(root, packet_stage, root_identity)]
         if passages_root is not None and passages_stage is not None:
             outputs.append((passages_root, passages_stage, passages_identity))
diff --git a/skills/agent-review/SKILL.md b/skills/agent-review/SKILL.md
index 1fe725e0b..594e9e260 100644
--- a/skills/agent-review/SKILL.md
+++ b/skills/agent-review/SKILL.md
@@ -49,7 +49,11 @@ of the packet that was read, and, for a source-faithfulness verdict, the
 article review hash; the
 [CLI reference](../../autoform_cli/README.md#skeleton-hashes) says what each
 binds. These hashes are provenance evidence, not reviewer authentication or an
-approval key.
+approval key. If the user has paused skeleton evidence during proof development,
+skip it and Formalize's import-edit baselines, say so, and record none of these
+hashes; still build the target, run `#print axioms` on each recorded declaration
+and `autoform check` and `audit` with `--lean-root`, and compare the compiled
+statement with its source.
 
 Report findings first, ordered by severity and tied to files or nodes. Then give
 the rubric scores, weighted verdict, commands run, unresolved questions, and a
diff --git a/skills/formalize/SKILL.md b/skills/formalize/SKILL.md
index 3151a1eb0..179d443ba 100644
--- a/skills/formalize/SKILL.md
+++ b/skills/formalize/SKILL.md
@@ -84,14 +84,14 @@ rerunning it with `--module-scope import-closure` when the default scope cannot
 build or load every root library. When the run uses claims, follow the [import
 claims](references/claims.md#import-edits) from then on; otherwise send the lead
 the report's `claim_targets` and `affected_claim_targets` and wait for its
-answer. Capture baseline skeleton evidence for the report's currently
-built, named affected articles and, when the edit removes an import, for the
-articles of modules only that import kept in the build. The affected articles
-are not a lock: do not acquire or edit them merely because they are listed, and
-treat reported unresolved declarations as unknown validation scope, not proof
-they are unaffected. After rebuilding, repeat the skeleton evidence and use
-Agent Review to judge semantic changes; repair each article that actually needs
-changes under the review gates of the [revision
+answer. Unless the user has paused skeleton evidence, capture baseline skeleton
+evidence for the report's currently built, named affected articles and, when the
+edit removes an import, for the articles of modules only that import kept in the
+build. The affected articles are not a lock: do not acquire or edit them merely
+because they are listed, and treat reported unresolved declarations as unknown
+validation scope, not proof they are unaffected. After rebuilding, repeat any
+baseline skeleton evidence and use Agent Review to judge semantic changes; repair
+each article that actually needs changes under the review gates of the [revision
 contract](../../autoform_cli/reference/claims-and-revisions.md#revision-contract).
 Stop for an active conflict (an affected target another worker holds, or another
 owner's live claim on one) or failed validation, not for a blanket import rule;
diff --git a/tests/test_skeleton.py b/tests/test_skeleton.py
index 1318b0006..b4bc06649 100644
--- a/tests/test_skeleton.py
+++ b/tests/test_skeleton.py
@@ -11,6 +11,7 @@
 import sys
 import threading
 import time
+import tracemalloc
 from collections.abc import Callable
 from dataclasses import replace
 from pathlib import Path
@@ -60,6 +61,7 @@
     UnresolvedTarget,
     _declaration,
     _hash_module_files,
+    _json_utf8,
     _local_safety_issue,
     _without_comments,
     _probe_record_issue,
@@ -301,6 +303,82 @@ def _fake_report(tmp_path: Path, output: str | None = None) -> SkeletonReport:
     return extract_skeletons(blueprint, lean_root=project, runner=lambda probe, root: output)
 
 
+def _shared_closure(root: Path, articles: dict[str, int], *, closure: int, size: int) -> tuple[Path, Path, str]:
+    """A project whose roots all trust one chain of definitions, its blueprint, and
+    what the probe says about them, written without Lean.
+
+    ``articles`` maps each article to how many roots it names. Each of the
+    ``closure`` definitions carries about ``size`` characters of kernel material,
+    with quotes, escapes, and characters beyond the Basic Multilingual Plane.
+    """
+
+    project = root / "project"
+    (project / "Synth").mkdir(parents=True)
+    (project / "lean-toolchain").write_text("leanprover/lean4:v4.32.2\n", encoding="utf-8")
+    (project / "lakefile.toml").write_text(
+        'name = "Synth"\ndefaultTargets = ["Synth"]\n\n[[lean_lib]]\nname = "Synth"\n', encoding="utf-8"
+    )
+    (project / "Synth.lean").write_text("import Synth.Main\n", encoding="utf-8")
+    roots = {stem: [f"{stem}_{index}" for index in range(count)] for stem, count in articles.items()}
+    names = [name for group in roots.values() for name in group]
+    lean = {stem: ", ".join(f"Synth.{name}" for name in group) for stem, group in roots.items()}
+    (project / "Synth" / "Main.lean").write_text(
+        "\n".join(["namespace Synth", "", *(f"theorem {name} : True := trivial" for name in names), "", "end Synth"])
+        + "\n",
+        encoding="utf-8",
+    )
+    blueprint = _blueprint(root, lean=lean)
+    source = blueprint / "sources" / "book.tex"
+    source.parent.mkdir()
+    source.write_text("Every root is \\emph{true}.\n", encoding="utf-8")
+    first = blueprint / "roadmap" / "basics" / f"{next(iter(articles))}.md"
+    _replace_source(first, "## Depends on", "## Sources\n\n- [book](../../sources/book.tex#L1-L1)\n\n## Depends on")
+
+    def table(kind: str, name: str, value: object) -> str:
+        return PROBE_MARKER + json.dumps({"table": kind, "name": name, "value": value})
+
+    pad = ('"q\\b" ℝ → 𝔽\t' * (size // 12 + 1))[:size]
+    lines: list[str] = []
+    for index in range(closure):
+        name = f"Synth.d{index}"
+        doc, code, comment = f"/-- Step {index} in ℝ. -/\n", f"def d{index} : ℝ → Type := ", "-- a step ⟨x⟩"
+        source_text = f"{doc}{code}{comment}\n  fun _ => Unit"
+        start = len(f"{doc}{code}".encode())
+        material = {"safety": "safe", "type": {"const": [name, pad]}, "value": {"bvar": index}}
+        entry = _trusted(
+            name, "def", [2 * index + 1, 2 * index + 2], f"{name} : ℝ →\n  Type",
+            depends=[f"Synth.d{index - 1}"] if index else [],
+            source=source_text,
+            source_comments=[[0, len(doc.encode()) - 1], [start, start + len(comment.encode())]],
+            module="Synth.Main",
+            semantic=json.dumps({"generated": [], "root": material}, separators=(",", ":"), ensure_ascii=False),
+        )
+        lines.append(table("trusted", name, dict(entry, semantic=[entry["semantic"]])))
+    semantic = _semantic({"type": {"sort": {"zero": None}}})
+    lines += [table("semantic", name, [semantic]) for name in ("Mathlib.Fake", "propext")]
+    lines.append(table("module", "Mathlib.Fake", [["olean", "Synth/Main.lean"]]))
+    for line, name in enumerate(names, start=3):
+        # Every other root's written statement holds a comment Lean could not place, so it is withheld.
+        statement = f"theorem {name} :\n    True" if line % 2 else f"theorem {name} : -- why\n    True"
+        lines.append(
+            PROBE_MARKER
+            + json.dumps(
+                {
+                    "root": f"Synth.{name}", "found": True, "kind": "theorem", "module": "Synth.Main",
+                    "range": [line, line], "signature": f"Synth.{name} : True", "raw_signature": f"Synth.{name} : True",
+                    "semantic_schema": SEMANTIC_SCHEMA, "semantic": [semantic], "lean_version": "4.32.2",
+                    "source": None, "source_comments": None, "statement_source": statement,
+                    "statement_comments": [] if line % 2 else None,
+                    "depends": [f"Synth.d{closure - 1}"], "trusted": [f"Synth.d{index}" for index in range(closure)],
+                    "assumed": ["Mathlib.Fake"], "boundary_modules": ["Mathlib.Fake"],
+                    "statement_assumed": ["Mathlib.Fake"], "statement_boundary_modules": ["Mathlib.Fake"],
+                    "axioms": ["propext"],
+                }
+            )
+        )
+    return project, blueprint, "\n".join(lines)
+
+
 # --------------------------------------------------------------------------- #
 # The probe program
 # --------------------------------------------------------------------------- #
@@ -1791,10 +1869,32 @@ def test_report_bytes_are_pinned(tmp_path: Path) -> None:
     assert digest == "a28525d38295df4e9848c3d1334528a29478678f269272e487d8de98ec41b8e3"
 
 
+def _tree_digest(root: Path) -> str:
+    digest = hashlib.sha256()
+    for path in sorted(root.rglob("*")):
+        if path.is_file():
+            digest.update(path.relative_to(root).as_posix().encode() + b"\0" + path.read_bytes() + b"\0")
+    return digest.hexdigest()
+
+
+def test_shared_closure_outputs_are_pinned(tmp_path: Path) -> None:
+    # Streaming the report and packets must keep every byte, and so every hash, a reader recorded.
+    project, blueprint, output = _shared_closure(tmp_path, {"joint": 3, "single": 1}, closure=4, size=300)
+    report = extract_skeletons(blueprint, lean_root=project, runner=lambda probe, root: output)
+    out = tmp_path / "out"
+
+    write_packets(report, out / "packets", passages=out / "passages", report_path=out / "skeleton.json")
+    write_skeleton_report(report, tmp_path / "alone.json")
+
+    assert report.clean
+    assert _tree_digest(out) == "89ca807ef1aaf2dce369bc5a56699dd831aaa7e0cace3b1a4c2300f0b4b6a92d"
+    assert (tmp_path / "alone.json").read_text(encoding="utf-8") == report.to_json() + "\n"
+    assert (out / "skeleton.json").read_bytes() == (tmp_path / "alone.json").read_bytes()
+
+
 def test_report_serialization_fingerprints_each_declaration_once(
     tmp_path: Path, monkeypatch: pytest.MonkeyPatch
 ) -> None:
-    report = _fake_report(tmp_path)
     calls: dict[str, int] = {"_fingerprint": 0, "_packet": 0, "_shared_tables": 0}
     for owner, name in (
         (DeclarationSkeleton, "_fingerprint"),
@@ -1808,12 +1908,52 @@ def counted(*args: object, _original: Callable[..., object] = original, _name: s
             return _original(*args, **kwargs)
 
         monkeypatch.setattr(owner, name, counted)
+    report = _fake_report(tmp_path)
 
     report.to_json()
     report.to_json()
 
-    # One meaning hash and one statement hash, one packet, and the tables built at construction.
-    assert calls == {"_fingerprint": 2, "_packet": 1, "_shared_tables": 0}
+    # Extraction makes one meaning hash and one statement hash; the packet is
+    # streamed once for its own hash and once in its article's; the tables are
+    # built at construction.
+    assert calls == {"_fingerprint": 2, "_packet": 2, "_shared_tables": 1}
+
+
+def test_writing_holds_no_whole_packet(tmp_path: Path) -> None:
+    # A large shared closure makes a packet gigabytes, so writing holds pieces of it, not all of it.
+    project, blueprint, output = _shared_closure(tmp_path, {"joint": 3}, closure=80, size=20000)
+    report = extract_skeletons(blueprint, lean_root=project, runner=lambda probe, root: output)
+    first, second, _ = report.nodes[0].declarations
+    assert all(item is other for item, other in zip(first.trusted, second.trusted, strict=True))
+
+    tracemalloc.start()
+    try:
+        write_packets(report, tmp_path / "packets", report_path=tmp_path / "skeleton.json")
+        _, peak = tracemalloc.get_traced_memory()
+    finally:
+        tracemalloc.stop()
+
+    article = (tmp_path / "packets" / "basics" / "joint" / "article.lean").stat().st_size
+    assert peak < article / 3, (peak, article)
+
+
+@pytest.mark.parametrize(
+    "value",
+    [
+        {},
+        [],
+        "",
+        {"b": [], "a": {}, "é": "\u2028", "A": ["\x00\x1f\x7f", "\"\\/", "𝔽 ℝ\t\n"]},
+        [["x", [], {"z": "1", "y": ["2", "3"]}], "\ud7ff\ue000\uffff"],
+    ],
+)
+def test_fingerprint_encoding_matches_json_dumps(value: object) -> None:
+    escaped: dict[str, bytes] = {}
+    expected = json.dumps(value, sort_keys=True, ensure_ascii=False).encode("utf-8")
+
+    # Twice, so a string escaped once encodes the same from the memo.
+    assert b"".join(_json_utf8(value, escaped)) == expected
+    assert b"".join(_json_utf8(value, escaped)) == expected
 
 
 def test_report_record_edits_do_not_reach_the_report(tmp_path: Path) -> None:
@@ -2154,7 +2294,62 @@ def test_cli_publishes_report_and_packet_trees_together(
     assert (passages / PACKET_MANIFEST).is_file()
     assert json.loads(output.read_text(encoding="utf-8"))["unresolved"] == []
     assert list(tmp_path.glob(".*.autoform-*")) == []
-    assert capsys.readouterr().err == ""
+    assert capsys.readouterr().err == "skeleton: probing 1 module...\nskeleton: assembling...\nskeleton: writing...\n"
+
+
+def test_cli_names_each_phase_on_stderr_as_it_starts(tmp_path: Path, capsys, monkeypatch) -> None:
+    project = _project(tmp_path)
+    blueprint = _blueprint(tmp_path, lean={"determined": "Skel.observation_determined"})
+    during_probe: list[str] = []
+
+    def probe(program: str, lean_root: Path) -> str:
+        during_probe.append(capsys.readouterr().err)
+        return _fake_probe_output()
+
+    _fake_default_probe(monkeypatch, probe)
+    output = tmp_path / "skeleton.json"
+
+    assert main(["skeleton", str(blueprint), "--lean-root", str(project), "--output", str(output)]) == 0
+
+    captured = capsys.readouterr()
+    # No probe runs once `assembling` appears, though the build must stay as it is until the command ends.
+    assert during_probe == ["skeleton: probing 1 module...\n"]
+    assert captured.err == "skeleton: assembling...\nskeleton: writing...\n"
+    assert captured.out == f"{output}: 1 skeleton(s) for 1 article(s)\n"
+
+
+def test_cli_json_prints_the_report_bytes(tmp_path: Path, capsys, monkeypatch) -> None:
+    assert _cli(tmp_path, monkeypatch, "--json") == 0
+
+    captured = capsys.readouterr()
+    assert captured.out == _fake_report(tmp_path / "other").to_json() + "\n"
+    assert captured.err == "skeleton: probing 1 module...\nskeleton: assembling...\n"
+
+
+def test_cli_json_stdout_stays_the_report_without_stderr(tmp_path: Path, capsys, monkeypatch) -> None:
+    # Started with fd 2 closed, Python sets sys.stderr to None, and print(file=None) writes to stdout.
+    monkeypatch.setattr(sys, "stderr", None)
+
+    assert _cli(tmp_path, monkeypatch, "--json") == 0
+
+    assert capsys.readouterr().out == _fake_report(tmp_path / "other").to_json() + "\n"
+
+
+@pytest.mark.skipif(os.name != "posix", reason="needs a POSIX pipe")
+def test_cli_progress_on_a_broken_stderr_leaves_nothing_to_fail_at_exit(tmp_path: Path, capsys, monkeypatch) -> None:
+    # A reader that stopped tailing stderr: the write end of a pipe whose read end is closed.
+    read_end, write_end = os.pipe()
+    os.close(read_end)
+    broken = open(write_end, "w", encoding="utf-8")
+    monkeypatch.setattr(sys, "stderr", broken)
+    try:
+        assert _cli(tmp_path, monkeypatch, "--json") == 0
+        # The interpreter flushes stderr at exit; a failure there would turn exit 0 into 120.
+        broken.flush()
+    finally:
+        broken.close()
+
+    assert capsys.readouterr().out == _fake_report(tmp_path / "other").to_json() + "\n"
 
 
 def test_cli_does_not_publish_packets_when_report_staging_fails(
@@ -3379,6 +3574,7 @@ def _declaration_of(project: Path, record: dict[str, object]):
         index=index_project(project),
         module_hashes={},
         snapshot_started_ns=None,
+        shared={},
     )