diff --git a/Proofs/Contain.lean b/Proofs/Contain.lean
index 9da005a..ab355e0 100644
--- a/Proofs/Contain.lean
+++ b/Proofs/Contain.lean
@@ -318,7 +318,7 @@ theorem gate_plain (name : String) (rel : List String) :
     is rejected; anything else is skipped. -/
 theorem manifest_eq (dest : List String) (entries : List RawEntry) :
     manifest dest entries = entries.map fun e =>
-      if regularType e.typeflag then
+      if regularType e.typeflag e.name then
         match cleanName e.name with
         | some rel => .extract (dest ++ rel) e.data
         | none => .reject e.name
@@ -514,7 +514,7 @@ theorem manifest_lines_eq (dest : String) (entries : List RawEntry) :
   funext e
   simp only [Function.comp_apply]
   unfold outcome Spec.line
-  have hreg : isRegular e = regularType e.typeflag := rfl
+  have hreg : isRegular e = regularType e.typeflag e.name := rfl
   rw [hreg, gate_eq]
   split
   · split
diff --git a/README.md b/README.md
index 570aa98..8458d62 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,7 @@ lake build
 
 The theorems are in `Proofs/Contain.lean`, about the code in `TarPilot/Path.lean` and `TarPilot/Archive.lean`. Their statements use the definitions in `Spec/Defs.lean`: a special character (a control character, C0, DEL, or C1, or the Unicode line or paragraph separator), a plain name (not empty, `.` or `..`, and free of `/` and special characters), the components of a path string (the parts between `/`), the gate's rules, the regular typeflags, a path under a destination, how a name is printed, the exact line printed for an entry, and lexical resolution of a relative path. They are about the code definitions `Spec/Defs.lean` lists, which a reviewer reads with them.
 
-The gate rules, which `gate_eq` proves the gate follows exactly: a name that starts with `/` is rejected. A name with a `..` component, or with a special character, is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files (typeflag `0` or NUL) are extracted, which `manifest_eq` proves. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination.
+The gate rules, which `gate_eq` proves the gate follows exactly: a name that starts with `/` is rejected. A name with a `..` component, or with a special character, is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files are extracted, which `manifest_eq` proves: typeflag `0`, NUL from older archives, or `7`, a contiguous file, which POSIX lets a reader treat as regular; and a name that does not end in `/`, which older archives use for a directory and GNU tar reads as one. So an entry with a regular typeflag and a name ending in `/` gets a `SKIP` line when its size is zero. When its size is not zero, the whole archive fails to parse, since readers disagree on whether data follows (see the list under What is not proved). Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination.
 
 - `gate_eq`: the gate is exactly its rules.
 - `gate_plain`: a name that passes the gate gives a non-empty list of plain names.
@@ -43,11 +43,17 @@ Axiom check: each theorem depends only on the standard Lean axioms (`propext`, `
 
 Read this before trusting the pilot with real archives:
 
-- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. Results are in `tests/TEST-RESULTS.md`: 37 checks, 14 of them on the axioms, 0 failures. They cover 23 archive entries with normal files, hostile names (control characters and line separators among them), and a long name split over the ustar prefix field; eight destinations, and six refused: five for a special character or U+FFFD, and one given as bytes that are not UTF-8; and broken inputs (truncated, garbage, bad checksum).
+- Header parsing, octal fields, checksums, and archive writing are tested, not proved. The tests compare the Lean code against Python's `tarfile` module and against an independent copy of the extraction spec. Results are in `tests/TEST-RESULTS.md`: 121 checks, 14 of them on the axioms, 0 failures. They cover 23 archive entries with normal files, hostile names (control characters and line separators among them), and a long name split over the ustar prefix field; eight destinations, and six refused: five for a special character or U+FFFD, and one given as bytes that are not UTF-8; broken inputs (truncated, garbage, bad checksum); 29 archives in formats the pilot does not read; and 13 more archives it does read, among them GNU format, GNU tar's own output in its default, `gnu` and `oldgnu` formats, names ending in `/`, and links, devices, directories and FIFOs whose size fields are not zero. Both commands are compared with `tarfile` on each of them. `tarfile` reads typeflag NUL with a name ending in `/` as a directory, typeflag 5, so the tool's typeflag 0 on such an entry is compared as 5. Every other typeflag is compared as printed.
 - The `list` output is tested, not proved. So is `Main.lean`: that it prints `o.line` for each outcome of the manifest, and refuses a destination with a special character or U+FFFD. Read it with the statements; it is a few lines.
 - Extraction works on an in-memory model. Nothing here writes files to disk, so the step from a proved in-memory path to a safe write on a real filesystem (races, symlinks already on disk, symlinked destination folders) is outside this project for now. The proof resolves paths lexically, as POSIX does when no component is a symlink.
 - The destination itself. The proof says where a path lands relative to the destination, not whether the destination is a safe place to write. The destination is the command-line argument as the Lean runtime decodes it from UTF-8.
-- Formats beyond POSIX ustar. GNU tar extensions (long name entries, pax headers), base-256 size fields, and sparse files are not supported. A base-256 size field fails to parse, but an archive with a GNU long name or a pax header is not refused, as the bar audit's probes show (findings F2 and F3). Such a header is skipped as a non-regular entry, so the file after it is read under the name in its own ustar header: a long name is cut to 100 bytes, and a pax path is ignored. A name or prefix field that is not valid UTF-8 reads as empty. So a short name like that is rejected, but a name split over both fields, with one field invalid, is extracted under another name. In every probe the path stays inside the destination, since the gate still runs.
+- Formats beyond POSIX ustar. The pilot reads ustar headers, and GNU headers that carry nothing ustar does not. As POSIX says, and as GNU tar and Python's `tarfile` read them, links, devices, directories and FIFOs store no data, whatever their size field says. An archive that uses anything else fails to parse as a whole, instead of being read in a wrong way:
+  - typeflags outside the POSIX set (NUL and `0` to `7`), among them GNU long names and long links (`L`, `K`), pax headers (`x`, `g`), and GNU sparse, incremental and volume entries. GNU tar writes long names this way by default, and Python's `tarfile` writes pax headers for long or non-ASCII names;
+  - a GNU header with anything where ustar keeps its name prefix (bytes 345 to 499), such as the access and change times of an incremental dump. GNU tar 1.35 puts nothing there for short names, in its default, `gnu` and `oldgnu` formats, unless it is asked for an incremental dump, a sparse file or a multi-volume archive;
+  - a name or prefix field that is not valid UTF-8;
+  - a base-256 size field, or a size field of spaces, which GNU tar refuses;
+  - a regular typeflag with a name ending in `/`, which reads as a directory, and a size that is not zero, where readers disagree on whether data follows;
+  - any other magic, such as an old Unix V7 header.
 - The Lean compiler, runtime, and kernel are trusted, as in every Lean project. A bug in them is outside the proof.
 
 ## Re-check it
@@ -60,7 +66,9 @@ python3 tests/run_tests.py
 
 The build fails if a proof breaks, though it accepts a `sorry` with only a warning. The second command prints the axioms each theorem depends on. The test script builds the project first, fails if any theorem depends on an axiom other than the three standard ones, reruns every comparison, and rewrites `tests/TEST-RESULTS.md`.
 
-`python3 tests/compare_old.py` builds the tool as it was before the containment change (commit 7517a86) and compares the two on 3,000 random archives under five destinations, from a recorded seed. Once the new escapes in names are undone, the output must be the same. It writes `tests/COMPARE-OLD.md`.
+`python3 tests/compare_old.py --new 1273382` builds the tool as it was before the containment change (commit 7517a86) and the tool of that change (commit 1273382), and compares the two on 3,000 random archives under five destinations, from a recorded seed. Once the new escapes in names are undone, the output must be the same. It writes `tests/COMPARE-OLD.md`. Without `--new`, it compares this checkout's tool, and runs differ on purpose: some random names end in `/` with a regular typeflag, and this tool skips such an entry, or refuses the archive when the entry has data.
+
+`python3 tests/run_tests.py --tool 1273382` runs the same checks against the tool of the containment change (commit 1273382), from before the parser changes. It leaves out the axiom check, which reads this checkout's proofs, not the tool, and writes `tests/TEST-RESULTS-1273382.md`: 68 of the 107 checks fail there.
 
 `python3 tests/planted_bugs.py` plants, one at a time in a copy, a `sorry`, an axiom, an extra theorem that is not on the list, and a listed theorem left out of `TarPilot/Verify.lean`. It records that `lake build` passes on each and that the test script fails. It writes `tests/PLANTED-BUGS.md`.
 
diff --git a/Spec/Defs.lean b/Spec/Defs.lean
index e707289..338d34d 100644
--- a/Spec/Defs.lean
+++ b/Spec/Defs.lean
@@ -47,9 +47,12 @@ def cleanName (name : String) : Option (List String) :=
       let kept := parts.filter (fun c => !(c == "" || c == "."))
       if kept = [] then none else some kept
 
-/-- The typeflags of regular files: `0`, and NUL from older archives. -/
-def regularType (t : Char) : Bool :=
-  t == '0' || t == Char.ofNat 0
+/-- Whether an entry with typeflag `t` and name `name` is a regular file:
+    typeflag `0`, NUL from older archives, or `7`, a contiguous file,
+    which POSIX lets a reader treat as regular; and a name that does not
+    end in `/`, which older archives use for a directory. -/
+def regularType (t : Char) (name : String) : Bool :=
+  (t == '0' || t == Char.ofNat 0 || t == '7') && name.toList.getLast? != some '/'
 
 /-- A relative path `rel` under the destination `dest`, as a string: `rel`
     alone when `dest` is empty, `dest` then `rel` when `dest` ends in `/`,
@@ -135,7 +138,7 @@ def byteSum (b : ByteArray) : Nat :=
     whose name fails; `SKIP`, the name, and the typeflag as a decimal
     code, for anything else. -/
 def line (dest : String) (name : String) (t : Char) (data : ByteArray) : String :=
-  if regularType t then
+  if regularType t name then
     match cleanName name with
     | some rel =>
       "OK\t" ++ under dest (String.intercalate "/" rel) ++ "\t" ++ toString data.size ++
diff --git a/TarPilot/Archive.lean b/TarPilot/Archive.lean
index b6d8268..1131d41 100644
--- a/TarPilot/Archive.lean
+++ b/TarPilot/Archive.lean
@@ -51,11 +51,16 @@ def parseBlocks (data : ByteArray) (off : Nat) : Nat → Option (List RawEntry)
 def parseArchive (data : ByteArray) : Option (List RawEntry) :=
   parseBlocks data 0 (data.size / 512 + 1)
 
-/-- Regular files only: typeflag `0` or NUL. Directories, links, and
-    everything else are never extracted, so a link entry cannot be used
-    to place a later entry outside the destination. -/
+/-- Regular files only: typeflag `0`, NUL, or `7` (a contiguous file,
+    which POSIX lets a reader treat as regular, as Python's `tarfile`
+    does), and a name that does not end in `/`. Older archives mark a
+    directory with that `/`, and GNU tar reads any entry named so as a
+    directory. Directories, links, and everything else are never
+    extracted, so a link entry cannot be used to place a later entry
+    outside the destination. -/
 def isRegular (e : RawEntry) : Bool :=
-  e.typeflag == '0' || e.typeflag == Char.ofNat 0
+  (e.typeflag == '0' || e.typeflag == Char.ofNat 0 || e.typeflag == '7') &&
+    e.name.toList.getLast? != some '/'
 
 /-- Extract entries into a list of `(path, data)` pairs, in memory.
     The path of each pair is the destination components followed by the
diff --git a/TarPilot/Header.lean b/TarPilot/Header.lean
index 68885a7..d948491 100644
--- a/TarPilot/Header.lean
+++ b/TarPilot/Header.lean
@@ -16,7 +16,8 @@ import TarPilot.Octal
 
 namespace TarPilot
 
-/-- A parsed header. Only the fields the pilot uses. -/
+/-- A parsed header. Only the fields the pilot uses. `size` is the size
+    of the data that follows the header. -/
 structure Header where
   name : String
   size : Nat
@@ -31,11 +32,26 @@ def byteAt (b : ByteArray) (i : Nat) : UInt8 :=
 def sliceList (b : ByteArray) (off len : Nat) : List UInt8 :=
   (b.extract off (off + len)).toList
 
-/-- A name field: bytes up to the first NUL, read as UTF-8.
-    Invalid UTF-8 reads as the empty string. -/
-def bytesToName (bs : List UInt8) : String :=
+/-- A name field: bytes up to the first NUL, read as UTF-8, or `none`
+    when they are not valid UTF-8. -/
+def bytesToName (bs : List UInt8) : Option String :=
   let raw := bs.takeWhile (fun b => b ≠ 0)
-  (String.fromUTF8? (ByteArray.mk raw.toArray)).getD ""
+  String.fromUTF8? (ByteArray.mk raw.toArray)
+
+/-- The magic and version of a POSIX ustar header: `ustar`, NUL, `00`. -/
+def ustarMagic : List UInt8 := [117, 115, 116, 97, 114, 0, 48, 48]
+
+/-- The magic and version of a GNU header: `ustar`, two spaces, NUL. -/
+def gnuMagic : List UInt8 := [117, 115, 116, 97, 114, 32, 32, 0]
+
+/-- The typeflags the pilot reads: NUL and `0` to `7`, the types POSIX
+    ustar defines. Any other typeflag, among them the GNU long name and
+    long link entries `L` and `K`, the pax headers `x` and `g`, and GNU
+    sparse and incremental entries, makes the archive fail to parse:
+    such entries change how other entries read, or carry data the pilot
+    does not read. -/
+def knownTypeflag (t : Char) : Bool :=
+  t == Char.ofNat 0 || ('0' ≤ t && t ≤ '7')
 
 /-- The header checksum: sum of all 512 bytes, with the checksum field
     itself (bytes 148 to 155) counted as spaces. -/
@@ -43,20 +59,38 @@ def blockChecksum (bs : List UInt8) : Nat :=
   (bs.zipIdx).foldl
     (fun acc p => acc + (if 148 ≤ p.2 ∧ p.2 < 156 then 32 else p.1.toNat)) 0
 
-/-- Parse one 512-byte header block. Fails on a short block, a bad
-    magic, a checksum mismatch, or a bad size field. -/
+/-- Parse one 512-byte header block. Fails on a short block; a magic
+    that is neither POSIX ustar nor GNU; a GNU header with anything in
+    the area where ustar keeps its prefix (GNU keeps access and change
+    times, sparse maps and volume offsets there); a checksum mismatch; a
+    bad size field; a typeflag outside `knownTypeflag`; a name or prefix
+    field that is not valid UTF-8; or a regular typeflag with a name
+    ending in `/`, which reads as a directory, and a size that is not
+    zero, where readers disagree on whether data follows.
+
+    Only regular typeflags (NUL, `0`, `7`) are followed by data. POSIX
+    stores no data for links, devices, directories and FIFOs (types 1 to
+    6), whatever their size field says, and GNU tar and Python's tarfile
+    read the next header straight after them, so the size given for
+    those is 0. -/
 def parseBlock (block : ByteArray) : Option Header :=
   if block.size < 512 then none
   else do
-    if sliceList block 257 5 ≠ [117, 115, 116, 97, 114] then none else
+    let magic := sliceList block 257 8
+    let gnuPlain := magic = gnuMagic ∧ (sliceList block 345 155).all (· = 0)
+    if ¬(magic = ustarMagic ∨ gnuPlain) then none else
     let stored ← parseOctal (sliceList block 148 8)
     if stored ≠ blockChecksum (sliceList block 0 512) then none else
     let size ← parseOctal (sliceList block 124 12)
-    let name := bytesToName (sliceList block 0 100)
-    let pfx := bytesToName (sliceList block 345 155)
+    let typeflag := Char.ofNat (byteAt block 156).toNat
+    if !knownTypeflag typeflag then none else
+    let name ← bytesToName (sliceList block 0 100)
+    let pfx ← bytesToName (sliceList block 345 155)
     let fullName := if pfx = "" then name else pfx ++ "/" ++ name
-    some { name := fullName, size := size,
-           typeflag := Char.ofNat (byteAt block 156).toNat }
+    let regular := typeflag == '0' || typeflag == Char.ofNat 0 || typeflag == '7'
+    let dirName := fullName.toList.getLast? == some '/'
+    if regular && dirName && size != 0 then none else
+    some { name := fullName, size := if regular then size else 0, typeflag := typeflag }
 
 /-- Content padded on the right with NUL bytes to width `w`,
     or cut to `w` when longer. -/
@@ -65,7 +99,8 @@ def fieldBytes (content : List UInt8) (w : Nat) : List UInt8 :=
 
 /-- Split a long name at a `/` so the part before it fits the 155-byte
     prefix field and the part after it fits the 100-byte name field.
-    Short names get an empty prefix. Fails when no split works. -/
+    Short names get an empty prefix. Neither part of a split may be
+    empty, so an absolute name keeps its `/`. Fails when no split works. -/
 def splitUstarName (name : String) : Option (String × String) :=
   if name.toUTF8.size ≤ 100 then some ("", name)
   else
@@ -73,7 +108,7 @@ def splitUstarName (name : String) : Option (String × String) :=
     let tries := (List.range cs.length).map fun k =>
       (String.intercalate "/" (cs.take (k + 1)), String.intercalate "/" (cs.drop (k + 1)))
     tries.find? (fun p =>
-      p.1.toUTF8.size ≤ 155 ∧ p.2.toUTF8.size ≤ 100 ∧ p.2 ≠ "")
+      p.1 ≠ "" ∧ p.1.toUTF8.size ≤ 155 ∧ p.2.toUTF8.size ≤ 100 ∧ p.2 ≠ "")
 
 /-- Build a 512-byte header block for a regular file or directory.
     Mode is fixed at 0644, uid, gid, and mtime at 0.
diff --git a/TarPilot/Octal.lean b/TarPilot/Octal.lean
index 8973946..df9c4d0 100644
--- a/TarPilot/Octal.lean
+++ b/TarPilot/Octal.lean
@@ -14,9 +14,11 @@ def trimField (bs : List UInt8) : List UInt8 :=
   (noLead.reverse.dropWhile (fun b => b = 0 ∨ b = 32)).reverse
 
 /-- Parse an octal field. Fails on any byte that is not an octal digit
-    after trimming. An empty field parses as 0. -/
+    after trimming. A field with no digits parses as 0 when it is all
+    NUL, and fails when it holds a space, as GNU tar refuses it. -/
 def parseOctal (bs : List UInt8) : Option Nat :=
   let digits := trimField bs
+  if digits.isEmpty && bs.any (· == 32) then none else
   digits.foldl (fun acc b =>
     match acc with
     | none => none
diff --git a/tests/COMPARE-OLD.md b/tests/COMPARE-OLD.md
index b0e8d65..11e2cc6 100644
--- a/tests/COMPARE-OLD.md
+++ b/tests/COMPARE-OLD.md
@@ -2,7 +2,7 @@
 
 Written by `tests/compare_old.py`. Rerun it to check these numbers.
 
-- Old tool: commit 7517a86. New tool: this checkout.
+- Old tool: commit 7517a86. New tool: commit 1273382.
 - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17.
 - Seed: 20261025
 - Random archives: 3000, written by Python's `tarfile` in ustar format
diff --git a/tests/TEST-RESULTS-1273382.md b/tests/TEST-RESULTS-1273382.md
new file mode 100644
index 0000000..f8ac273
--- /dev/null
+++ b/tests/TEST-RESULTS-1273382.md
@@ -0,0 +1,93 @@
+# Test results
+
+Run by `tests/run_tests.py --tool 1273382` against Python's `tarfile` module.
+The tool was built from commit 1273382, not from this checkout. The axiom
+check reads this checkout's proofs, not the tool, so it is left out.
+Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17. System tar: tar (GNU tar) 1.35.
+
+- Checks run: 107, all on the tool
+- Failures: 68
+- Archive A entries compared (list and manifest): 23
+- Manifest outcome on archive A: 10 extracted, 9 rejected by the path gate, 4 skipped as non-regular
+- Files written by the Lean `create` command and read back by Python: 3
+- Broken inputs that must fail with exit code 1: truncated archive, random garbage, corrupted checksum
+- Archives in formats the pilot does not read, which must fail with exit code 1 under `list` and `manifest`: 29
+- Archives in other formats it reads, compared with tarfile under `list` and `manifest`: 13
+
+How the output is compared with tarfile. tarfile drops the `/` at the end of a
+directory name, so directory names in `list` and names in `SKIP` lines are
+compared without it. tarfile also reads an entry with typeflag NUL and a name
+ending in `/` as a directory, typeflag 5, so for the readable archives the
+tool's typeflag 0 on such an entry is read as 5. Every other typeflag is
+compared as printed.
+
+## Failures
+
+- unsupported-fails: GNU long name entry (typeflag L) (list): rc=0 out='././@LongLink\t127\t76\nd/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t48\n'
+- unsupported-fails: GNU long name entry (typeflag L) (manifest): rc=0 out='SKIP\t././@LongLink\t76\nOK\tout/d/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t120\n'
+- unsupported-fails: GNU long link entry (typeflag K) (list): rc=0 out='l.txt\t1\t75\n'
+- unsupported-fails: GNU long link entry (typeflag K) (manifest): rc=0 out='SKIP\tl.txt\t75\n'
+- unsupported-fails: pax long path (typeflag x) (list): rc=0 out='././@PaxHeader\t136\t120\nd/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t48\n'
+- unsupported-fails: pax long path (typeflag x) (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/d/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t120\n'
+- unsupported-fails: pax path override (list): rc=0 out='././@PaxHeader\t27\t120\nsafe.txt\t1\t48\n'
+- unsupported-fails: pax path override (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/safe.txt\t1\t120\n'
+- unsupported-fails: pax path override that climbs out (list): rc=0 out='././@PaxHeader\t27\t120\nsafe.txt\t1\t48\n'
+- unsupported-fails: pax path override that climbs out (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/safe.txt\t1\t120\n'
+- unsupported-fails: pax non-ASCII name (list): rc=0 out='././@PaxHeader\t24\t120\ncaf?/notes.txt\t1\t48\n'
+- unsupported-fails: pax non-ASCII name (manifest): rc=0 out='SKIP\t././@PaxHeader\t120\nOK\tout/caf?/notes.txt\t1\t120\n'
+- unsupported-fails: pax global header (typeflag g) (list): rc=0 out='././@PaxHeader\t18\t103\ng.txt\t1\t48\n'
+- unsupported-fails: pax global header (typeflag g) (manifest): rc=0 out='SKIP\t././@PaxHeader\t103\nOK\tout/g.txt\t1\t103\n'
+- unsupported-fails: split name, invalid UTF-8 in the prefix field only (list): rc=0 out='qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq/file.txt\t1\t48\n'
+- unsupported-fails: split name, invalid UTF-8 in the prefix field only (manifest): rc=0 out='OK\tout/qqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqqq/file.txt\t1\t120\n'
+- unsupported-fails: split name, invalid UTF-8 in the name field only (list): rc=0 out='pppppppppppppppppppppppppppppp/\t1\t48\n'
+- unsupported-fails: split name, invalid UTF-8 in the name field only (manifest): rc=0 out='OK\tout/pppppppppppppppppppppppppppppp\t1\t120\n'
+- unsupported-fails: split name, invalid UTF-8 in both fields (list): rc=0 out='\t1\t48\n'
+- unsupported-fails: split name, invalid UTF-8 in both fields (manifest): rc=0 out='REJECT\t\n'
+- unsupported-fails: short name, invalid UTF-8 (list): rc=0 out='\t1\t48\n'
+- unsupported-fails: short name, invalid UTF-8 (manifest): rc=0 out='REJECT\t\n'
+- unsupported-fails: GNU header with access and change times (incremental dump) (list): rc=0 out='15267276047/a.txt\t1\t48\n'
+- unsupported-fails: GNU header with access and change times (incremental dump) (manifest): rc=0 out='OK\tout/15267276047/a.txt\t1\t120\n'
+- unsupported-fails: GNU header with a sparse map (list): rc=0 out='a.txt\t1\t48\n'
+- unsupported-fails: GNU header with a sparse map (manifest): rc=0 out='OK\tout/a.txt\t1\t120\n'
+- unsupported-fails: unknown typeflag D (list): rc=0 out='u.txt\t1\t68\n'
+- unsupported-fails: unknown typeflag D (manifest): rc=0 out='SKIP\tu.txt\t68\n'
+- unsupported-fails: unknown typeflag M (list): rc=0 out='u.txt\t1\t77\n'
+- unsupported-fails: unknown typeflag M (manifest): rc=0 out='SKIP\tu.txt\t77\n'
+- unsupported-fails: unknown typeflag N (list): rc=0 out='u.txt\t1\t78\n'
+- unsupported-fails: unknown typeflag N (manifest): rc=0 out='SKIP\tu.txt\t78\n'
+- unsupported-fails: unknown typeflag S (list): rc=0 out='u.txt\t1\t83\n'
+- unsupported-fails: unknown typeflag S (manifest): rc=0 out='SKIP\tu.txt\t83\n'
+- unsupported-fails: unknown typeflag V (list): rc=0 out='u.txt\t1\t86\n'
+- unsupported-fails: unknown typeflag V (manifest): rc=0 out='SKIP\tu.txt\t86\n'
+- unsupported-fails: unknown typeflag A (list): rc=0 out='u.txt\t1\t65\n'
+- unsupported-fails: unknown typeflag A (manifest): rc=0 out='SKIP\tu.txt\t65\n'
+- unsupported-fails: unknown typeflag Z (list): rc=0 out='u.txt\t1\t90\n'
+- unsupported-fails: unknown typeflag Z (manifest): rc=0 out='SKIP\tu.txt\t90\n'
+- unsupported-fails: ustar magic with a GNU version (list): rc=0 out='m.txt\t1\t48\n'
+- unsupported-fails: ustar magic with a GNU version (manifest): rc=0 out='OK\tout/m.txt\t1\t120\n'
+- unsupported-fails: name ending in / with typeflag b'\x00' and data (list): rc=0 out='d/\t1\t0\n'
+- unsupported-fails: name ending in / with typeflag b'\x00' and data (manifest): rc=0 out='OK\tout/d\t1\t120\n'
+- unsupported-fails: name ending in / with typeflag b'0' and data (list): rc=0 out='e/\t1\t48\n'
+- unsupported-fails: name ending in / with typeflag b'0' and data (manifest): rc=0 out='OK\tout/e\t1\t120\n'
+- unsupported-fails: size field of spaces (list): rc=0 out='f\t0\t48\n'
+- unsupported-fails: size field of spaces (manifest): rc=0 out='OK\tout/f\t0\t0\n'
+- unsupported-fails: system tar, default format, long name (list): rc=0 out='d/\t0\t53\n././@LongLink\t127\t76\nd/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t48\n'
+- unsupported-fails: system tar, default format, long name (manifest): rc=0 out='SKIP\td/\t53\nSKIP\t././@LongLink\t76\nOK\tout/d/nnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnnn\t1\t120\n'
+- unsupported-fails: system tar, incremental dump (times in bytes 345 to 368) (list): rc=0 out='15267725440/a.txt\t3\t48\n'
+- unsupported-fails: system tar, incremental dump (times in bytes 345 to 368) (manifest): rc=0 out='OK\tout/15267725440/a.txt\t3\t219\n'
+- unsupported-fails: system tar, sparse file (typeflag S, map in bytes 386 to 494) (list): rc=0 out='sparse\t3\t83\n'
+- unsupported-fails: system tar, sparse file (typeflag S, map in bytes 386 to 494) (manifest): rc=0 out='SKIP\tsparse\t83\n'
+- readable-manifest: contiguous file (typeflag 7): rc=0 lean=['SKIP\tcontig.bin\t55'] expected=['OK\tout/contig.bin\t10\t1104']
+- readable-manifest: names ending in / with typeflags NUL and 0, read as directories: rc=0 lean=['OK\tout/olddir\t0\t0', 'OK\tout/olddir/f.txt\t3\t319', 'OK\tout/slashdir\t0\t0'] expected=['SKIP\tolddir\t53', 'OK\tout/olddir/f.txt\t3\t319', 'SKIP\tslashdir\t48']
+- readable-list: typeflag 1 with a size field, then two files: rc=0 lean=[('node', 1024, 49), ('b.txt', 1, 48)] expected=[('node', 0, 49), ('hidden.txt', 6, 48), ('b.txt', 1, 48)]
+- readable-manifest: typeflag 1 with a size field, then two files: rc=0 lean=['SKIP\tnode\t49', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t49', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98']
+- readable-list: typeflag 2 with a size field, then two files: rc=0 lean=[('node', 1024, 50), ('b.txt', 1, 48)] expected=[('node', 0, 50), ('hidden.txt', 6, 48), ('b.txt', 1, 48)]
+- readable-manifest: typeflag 2 with a size field, then two files: rc=0 lean=['SKIP\tnode\t50', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t50', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98']
+- readable-list: typeflag 3 with a size field, then two files: rc=0 lean=[('node', 1024, 51), ('b.txt', 1, 48)] expected=[('node', 0, 51), ('hidden.txt', 6, 48), ('b.txt', 1, 48)]
+- readable-manifest: typeflag 3 with a size field, then two files: rc=0 lean=['SKIP\tnode\t51', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t51', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98']
+- readable-list: typeflag 4 with a size field, then two files: rc=0 lean=[('node', 1024, 52), ('b.txt', 1, 48)] expected=[('node', 0, 52), ('hidden.txt', 6, 48), ('b.txt', 1, 48)]
+- readable-manifest: typeflag 4 with a size field, then two files: rc=0 lean=['SKIP\tnode\t52', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t52', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98']
+- readable-list: typeflag 5 with a size field, then two files: rc=0 lean=[('node', 1024, 53), ('b.txt', 1, 48)] expected=[('node', 0, 53), ('hidden.txt', 6, 48), ('b.txt', 1, 48)]
+- readable-manifest: typeflag 5 with a size field, then two files: rc=0 lean=['SKIP\tnode\t53', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t53', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98']
+- readable-list: typeflag 6 with a size field, then two files: rc=0 lean=[('node', 1024, 54), ('b.txt', 1, 48)] expected=[('node', 0, 54), ('hidden.txt', 6, 48), ('b.txt', 1, 48)]
+- readable-manifest: typeflag 6 with a size field, then two files: rc=0 lean=['SKIP\tnode\t54', 'OK\tout/b.txt\t1\t98'] expected=['SKIP\tnode\t54', 'OK\tout/hidden.txt\t6\t620', 'OK\tout/b.txt\t1\t98']
diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md
index 0a22413..7070a4f 100644
--- a/tests/TEST-RESULTS.md
+++ b/tests/TEST-RESULTS.md
@@ -1,14 +1,23 @@
 # Test results
 
 Run by `tests/run_tests.py` against Python's `tarfile` module.
-Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17.
+Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.13.17. System tar: tar (GNU tar) 1.35.
 
-- Checks run: 37 (14 of them on the axioms of the theorems)
+- Checks run: 121 (14 of them on the axioms of the theorems)
 - Failures: 0
 - Archive A entries compared (list and manifest): 23
 - Manifest outcome on archive A: 10 extracted, 9 rejected by the path gate, 4 skipped as non-regular
 - Files written by the Lean `create` command and read back by Python: 3
-- Broken inputs rejected with exit code 1: truncated archive, random garbage, corrupted checksum
+- Broken inputs that must fail with exit code 1: truncated archive, random garbage, corrupted checksum
+- Archives in formats the pilot does not read, which must fail with exit code 1 under `list` and `manifest`: 29
+- Archives in other formats it reads, compared with tarfile under `list` and `manifest`: 13
+
+How the output is compared with tarfile. tarfile drops the `/` at the end of a
+directory name, so directory names in `list` and names in `SKIP` lines are
+compared without it. tarfile also reads an entry with typeflag NUL and a name
+ending in `/` as a directory, typeflag 5, so for the readable archives the
+tool's typeflag 0 on such an entry is read as 5. Every other typeflag is
+compared as printed.
 
 Axiom check (`TarPilot/Verify.lean`):
 
diff --git a/tests/run_tests.py b/tests/run_tests.py
index 8a0b164..1638769 100644
--- a/tests/run_tests.py
+++ b/tests/run_tests.py
@@ -10,12 +10,24 @@
 It builds the Lean project first, so it never checks stale code, runs
 all cases in a temporary directory, writes `tests/TEST-RESULTS.md`, and
 exits non-zero if any case fails.
+
+With `--tool REV`, the checks on the tool run against the tool built
+from commit REV, in a temporary directory, instead of this checkout's.
+The checkout is not changed or built. The axiom check reads this
+checkout's proofs, not the tool, so it is left out. The record goes to
+`tests/TEST-RESULTS-REV.md`, with REV as a short hash, and
+`tests/TEST-RESULTS.md` is left as it is. This shows which of these
+checks an earlier tool fails:
+
+    python3 tests/run_tests.py --tool 1273382
 """
 
+import argparse
 import io
 import os
 import random
 import re
+import shutil
 import subprocess
 import sys
 import tarfile
@@ -98,6 +110,209 @@ def is_regular(ti):
     return ti.isreg()
 
 
+# Typeflags of regular files: `0`, NUL, and `7` (contiguous file).
+REGULAR_CODES = (ord("0"), 0, ord("7"))
+
+
+def is_regular_entry(name, tcode):
+    """A regular file: typeflag `0`, NUL or `7`, and a name that does not
+    end in `/`, which older archives use for a directory."""
+    return tcode in REGULAR_CODES and not name.endswith("/")
+
+
+def one_file(fmt, name, data=b"x", typ=tarfile.REGTYPE, pax=None):
+    """An archive of one entry, written by Python's tarfile."""
+    buf = io.BytesIO()
+    with tarfile.open(fileobj=buf, mode="w", format=fmt) as t:
+        ti = tarfile.TarInfo(name)
+        ti.size = len(data)
+        ti.type = typ
+        ti.mtime = 0
+        if pax:
+            ti.pax_headers = pax
+        t.addfile(ti, io.BytesIO(data))
+    return buf.getvalue()
+
+
+def patch_header(raw, offset, new_bytes):
+    """Overwrite bytes in the first header and fix its checksum."""
+    hdr = bytearray(raw[:512])
+    hdr[offset:offset + len(new_bytes)] = new_bytes
+    hdr[148:156] = b" " * 8
+    hdr[148:156] = ("%06o\0 " % sum(hdr)).encode()
+    return bytes(hdr) + raw[512:]
+
+
+LONG = "d/" + "n" * 120 + ".txt"
+SPLIT = "p" * 30 + "/" + "q" * 90 + "/file.txt"
+
+
+def unsupported_archives(work):
+    """Archives that use what the pilot does not read. Each must fail to
+    parse: these are the probes of findings F2, F3 and F7 of the bar
+    audit, and more of the same kinds."""
+    yield "GNU long name entry (typeflag L)", one_file(tarfile.GNU_FORMAT, LONG)
+    yield "GNU long link entry (typeflag K)", patch_header(
+        one_file(tarfile.GNU_FORMAT, "l.txt"), 156, b"K")
+    yield "pax long path (typeflag x)", one_file(tarfile.PAX_FORMAT, LONG)
+    yield "pax path override", one_file(tarfile.PAX_FORMAT, "safe.txt",
+                                        pax={"path": "other/dir/real.txt"})
+    yield "pax path override that climbs out", one_file(
+        tarfile.PAX_FORMAT, "safe.txt", pax={"path": "../../etc/cron.d/x"})
+    yield "pax non-ASCII name", one_file(tarfile.PAX_FORMAT, "café/notes.txt")
+    buf = io.BytesIO()
+    with tarfile.open(fileobj=buf, mode="w", format=tarfile.PAX_FORMAT,
+                      pax_headers={"comment": "global"}) as t:
+        ti = tarfile.TarInfo("g.txt")
+        ti.size = 1
+        t.addfile(ti, io.BytesIO(b"g"))
+    yield "pax global header (typeflag g)", buf.getvalue()
+    split = one_file(tarfile.USTAR_FORMAT, SPLIT)
+    yield "split name, invalid UTF-8 in the prefix field only", patch_header(split, 345, b"\xff")
+    yield "split name, invalid UTF-8 in the name field only", patch_header(split, 0, b"\xff")
+    yield "split name, invalid UTF-8 in both fields", patch_header(
+        patch_header(split, 0, b"\xff"), 345, b"\xff")
+    yield "short name, invalid UTF-8", patch_header(
+        one_file(tarfile.USTAR_FORMAT, "short.txt"), 0, b"\xff")
+    gnu = one_file(tarfile.GNU_FORMAT, "a.txt")
+    yield "GNU header with access and change times (incremental dump)", patch_header(
+        gnu, 345, b"15267276047\x0015267276047\x00")
+    yield "GNU header with a sparse map", patch_header(gnu, 386, b"00000000001")
+    for code in b"DMNSVAZ":
+        yield f"unknown typeflag {chr(code)}", patch_header(
+            one_file(tarfile.USTAR_FORMAT, "u.txt"), 156, bytes([code]))
+    yield "base-256 size field", patch_header(
+        one_file(tarfile.USTAR_FORMAT, "b.txt"), 124, b"\x80" + b"\x00" * 10 + b"\x01")
+    yield "ustar magic with a GNU version", patch_header(
+        one_file(tarfile.USTAR_FORMAT, "m.txt"), 263, b" \x00")
+    yield "no magic (old Unix V7 header)", patch_header(
+        one_file(tarfile.USTAR_FORMAT, "v.txt"), 257, b"\x00" * 8)
+    for name, typ in [("d/", tarfile.AREGTYPE), ("e/", tarfile.REGTYPE)]:
+        yield f"name ending in / with typeflag {typ!r} and data", one_file(
+            tarfile.USTAR_FORMAT, name, data=b"x", typ=typ)
+    yield "size field of spaces", patch_header(
+        one_file(tarfile.USTAR_FORMAT, "f", data=b""), 124, b" " * 12)
+    gnu_tar = shutil.which("tar")
+    if gnu_tar:
+        src = work / "systar-long" / "d"
+        src.mkdir(parents=True)
+        (src / ("n" * 120 + ".txt")).write_bytes(b"x")
+        out = work / "systar-long.tar"
+        subprocess.run([gnu_tar, "cf", str(out), "d"], cwd=work / "systar-long", check=True)
+        yield "system tar, default format, long name", out.read_bytes()
+    if gnu_tar and is_gnu_tar(gnu_tar):
+        # GNU tar's own output for the GNU fields in bytes 345 to 499.
+        src = work / "systar-gnu-fields"
+        src.mkdir()
+        (src / "a.txt").write_bytes(b"hi\n")
+        with open(src / "sparse", "wb") as f:
+            f.seek(1 << 20)
+            f.write(b"end")
+        out = work / "systar-incremental.tar"
+        subprocess.run([gnu_tar, "cf", str(out), "--format=gnu",
+                        f"--listed-incremental={work / 'systar.snar'}", "a.txt"],
+                       cwd=src, check=True)
+        yield "system tar, incremental dump (times in bytes 345 to 368)", out.read_bytes()
+        out = work / "systar-sparse.tar"
+        subprocess.run([gnu_tar, "cf", str(out), "--format=gnu", "--sparse", "sparse"],
+                       cwd=src, check=True)
+        yield "system tar, sparse file (typeflag S, map in bytes 386 to 494)", out.read_bytes()
+
+
+def readable_archives(work):
+    """Archives in formats the pilot reads. Each must read as Python's
+    tarfile reads it."""
+    yield "contiguous file (typeflag 7)", one_file(
+        tarfile.USTAR_FORMAT, "contig.bin", data=b"contiguous", typ=tarfile.CONTTYPE)
+    buf = io.BytesIO()
+    with tarfile.open(fileobj=buf, mode="w", format=tarfile.GNU_FORMAT) as t:
+        for name, data in [("gnu.txt", b"gnu"), ("dir/inner.bin", bytes(range(40)))]:
+            ti = tarfile.TarInfo(name)
+            ti.size = len(data)
+            ti.mtime = 0
+            t.addfile(ti, io.BytesIO(data))
+    yield "GNU format, short names", buf.getvalue()
+    yield "pax format, short ASCII name (no pax header)", one_file(
+        tarfile.PAX_FORMAT, "plain.txt", data=b"plain")
+    buf = io.BytesIO()
+    with tarfile.open(fileobj=buf, mode="w", format=tarfile.USTAR_FORMAT) as t:
+        for name, typ, data in [("olddir/", tarfile.AREGTYPE, b""),
+                                ("olddir/f.txt", tarfile.AREGTYPE, b"old"),
+                                ("slashdir/", tarfile.REGTYPE, b"")]:
+            ti = tarfile.TarInfo(name)
+            ti.type = typ
+            ti.size = len(data)
+            ti.mtime = 0
+            t.addfile(ti, io.BytesIO(data))
+    yield "names ending in / with typeflags NUL and 0, read as directories", buf.getvalue()
+    for typ in [tarfile.LNKTYPE, tarfile.SYMTYPE, tarfile.CHRTYPE, tarfile.BLKTYPE,
+                tarfile.DIRTYPE, tarfile.FIFOTYPE]:
+        yield f"typeflag {typ.decode()} with a size field, then two files", hidden_after(typ)
+    gnu_tar = shutil.which("tar")
+    if gnu_tar:
+        # Every kind of entry GNU tar writes for short names in its own
+        # formats: GNU keeps nothing in bytes 345 to 499 for these unless
+        # it is asked for an incremental dump, a sparse file or a
+        # multi-volume archive.
+        src = work / "systar-short"
+        (src / "d").mkdir(parents=True)
+        (src / "a.txt").write_bytes(b"hi\n")
+        (src / "empty").write_bytes(b"")
+        (src / "d" / "b.txt").write_bytes(b"x\n")
+        os.link(src / "a.txt", src / "hard.txt")
+        os.symlink("a.txt", src / "sym")
+        os.mkfifo(src / "fifo")
+        names = ["a.txt", "empty", "d", "hard.txt", "sym", "fifo"]
+        for fmt in ["default"] + (["gnu", "oldgnu"] if is_gnu_tar(gnu_tar) else []):
+            out = work / f"systar-short-{fmt}.tar"
+            opts = [] if fmt == "default" else [f"--format={fmt}"]
+            subprocess.run([gnu_tar, "cf", str(out), *opts, *names], cwd=src, check=True)
+            yield (f"system tar, {fmt} format, short names: files, a directory, "
+                   "a hard link, a symlink, a FIFO"), out.read_bytes()
+
+
+def is_gnu_tar(tar):
+    r = subprocess.run([tar, "--version"], capture_output=True, text=True)
+    return r.stdout.startswith("tar (GNU tar)")
+
+
+def tar_version():
+    tar = shutil.which("tar")
+    if not tar:
+        return "none"
+    r = subprocess.run([tar, "--version"], capture_output=True, text=True)
+    return (r.stdout.splitlines() or ["unknown"])[0]
+
+
+def hidden_after(typ):
+    """An entry of type `typ` whose size field says 1024, then a header and
+    data that fill those 1024 bytes, then one more file. Types 1 to 6
+    store no data, so a reader must see all three entries."""
+    buf = io.BytesIO()
+    with tarfile.open(fileobj=buf, mode="w", format=tarfile.USTAR_FORMAT) as t:
+        for name, kind, data in [("node", typ, b""), ("hidden.txt", tarfile.REGTYPE, b"hidden"),
+                                 ("b.txt", tarfile.REGTYPE, b"b")]:
+            ti = tarfile.TarInfo(name)
+            ti.type = kind
+            ti.size = len(data)
+            ti.mtime = 0
+            if kind in (tarfile.SYMTYPE, tarfile.LNKTYPE):
+                ti.linkname = "target"
+            t.addfile(ti, io.BytesIO(data))
+    return patch_header(buf.getvalue(), 124, b"00000002000\0")
+
+
+def tarfile_view(path):
+    """(name, data, typeflag code) for each entry, as tarfile reads it."""
+    out = []
+    with tarfile.open(path) as tf:
+        for m in tf.getmembers():
+            data = tf.extractfile(m).read() if m.isreg() else b""
+            tcode = m.type[0] if isinstance(m.type, bytes) else ord(m.type)
+            out.append((m.name, data, tcode))
+    return out
+
+
 def build_archive_a(path):
     """Archive with normal, hostile, and edge-case entries, built with
     Python's tarfile as the reference implementation."""
@@ -157,7 +372,7 @@ def expected_manifest(entries_data, dest="out"):
     entries_data: list of (name, data, typeflag_byte)."""
     lines = []
     for name, data, tcode in entries_data:
-        if tcode not in (ord("0"), 0):
+        if not is_regular_entry(name, tcode):
             lines.append(f"SKIP\t{escape_name(name)}\t{tcode}")
             continue
         rel = spec_gate(name)
@@ -189,16 +404,75 @@ def list_rows(stdout):
     return rows
 
 
-def main():
-    # A run that stops early must not leave an earlier passing record.
-    RESULTS.unlink(missing_ok=True)
-    build = subprocess.run(["lake", "build"], cwd=PILOT_DIR, capture_output=True, text=True)
+def as_tarfile_reads(row):
+    """A `list` row as tarfile reads the entry. tarfile reads typeflag
+    NUL with a name ending in `/` as a directory, typeflag 5 ("Old V7
+    tar format represents a directory as a regular file with a trailing
+    slash", in tarfile.py). Every other row is left as it is."""
+    if len(row) == 3 and row[2] == 0 and row[0].endswith("/"):
+        return (row[0], row[1], 53)
+    return row
+
+
+def skip_as_tarfile_reads(line):
+    """A `manifest` line as tarfile reads the entry: the same rule, for
+    SKIP lines."""
+    p = line.split("\t")
+    if len(p) == 3 and p[0] == "SKIP" and p[2] == "0" and p[1].endswith("/"):
+        return "\t".join([p[0], p[1], "53"])
+    return line
+
+
+def commit_of(rev):
+    """The short hash of commit `rev`."""
+    r = subprocess.run(["git", "rev-parse", "--short=7", "--verify", rev + "^{commit}"],
+                       cwd=PILOT_DIR, capture_output=True, text=True)
+    if r.returncode != 0:
+        sys.exit(f"not a commit: {rev}")
+    return r.stdout.strip()
+
+
+def tool_at(rev, td):
+    """Build the tool at commit `rev` in `td`. The checkout is not
+    changed."""
+    src = td / "tool-src"
+    src.mkdir()
+    r = subprocess.run(["git", "archive", "--format=tar", rev], cwd=PILOT_DIR,
+                       capture_output=True)
+    if r.returncode != 0:
+        sys.exit(f"git archive {rev} failed: {r.stderr.decode()}")
+    with tarfile.open(fileobj=io.BytesIO(r.stdout)) as tf:
+        tf.extractall(src, filter="data")
+    build = subprocess.run(["lake", "build", "tar-pilot"], cwd=src, capture_output=True,
+                           text=True)
     if build.returncode != 0:
         print(build.stdout + build.stderr)
-        sys.exit("lake build failed")
+        sys.exit(f"lake build failed at {rev}")
+    return src / ".lake" / "build" / "bin" / "tar-pilot"
+
+
+def main():
+    global EXE
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("--tool", metavar="REV",
+                    help="check the tool built from commit REV instead of this checkout's, "
+                         "and leave out the axiom check")
+    args = ap.parse_args()
+    rev = commit_of(args.tool) if args.tool else None
+    results = RESULTS if rev is None else PILOT_DIR / "tests" / f"TEST-RESULTS-{rev}.md"
+    # A run that stops early must not leave an earlier passing record.
+    results.unlink(missing_ok=True)
+    if rev is None:
+        build = subprocess.run(["lake", "build"], cwd=PILOT_DIR, capture_output=True,
+                               text=True)
+        if build.returncode != 0:
+            print(build.stdout + build.stderr)
+            sys.exit("lake build failed")
 
     with tempfile.TemporaryDirectory() as td:
         td = Path(td)
+        if rev is not None:
+            EXE = tool_at(rev, td)
         archive_a = td / "a.tar"
         entries = build_archive_a(archive_a)
 
@@ -272,6 +546,13 @@ def main():
                     if m.isreg():
                         got[m.name] = tf.extractfile(m).read()
         check("create-readback", got == files, f"got={list(got)} want={list(files)}")
+        # A name too long for the name field, with no `/` to split it at,
+        # fails with exit code 1 and writes nothing.
+        target = td / "bad.tar"
+        (src / ("n" * 101)).write_bytes(b"x")
+        r = run_lean("create", str(target), "n" * 101, cwd=src)
+        check("create-refuses-long-name", r.returncode == 1 and not target.exists(),
+              f"rc={r.returncode} exists={target.exists()}")
 
         # 4. Lean reads its own archive back with the same manifest.
         if r.returncode == 0:
@@ -300,55 +581,108 @@ def main():
         r = run_lean("list", str(badsum))
         check("bad-checksum-fails", r.returncode == 1, f"rc={r.returncode}")
 
-    # 6. Axiom check: Verify.lean prints the axioms of exactly the
+        # 6. Formats the pilot does not read fail to parse, with exit
+        # code 1 and nothing on standard output, for both commands.
+        unsupported = 0
+        for i, (label, raw) in enumerate(unsupported_archives(td)):
+            unsupported += 1
+            path = td / f"unsupported{i}.tar"
+            path.write_bytes(raw)
+            for cmd in (["list", str(path)], ["manifest", str(path), "out"]):
+                r = run_lean(*cmd)
+                check(f"unsupported-fails: {label} ({cmd[0]})",
+                      r.returncode == 1 and r.stdout == "",
+                      f"rc={r.returncode} out={r.stdout[:200]!r}")
+
+        # 7. Formats the pilot reads give what tarfile reads.
+        readable = 0
+        for i, (label, raw) in enumerate(readable_archives(td)):
+            readable += 1
+            path = td / f"readable{i}.tar"
+            path.write_bytes(raw)
+            ref = tarfile_view(path)
+            # tarfile reports an old-style directory (typeflag NUL, name
+            # ending in `/`) as typeflag 5. The tool's output is read the
+            # same way (`as_tarfile_reads`); no other typeflag changes.
+            r = run_lean("list", str(path))
+            got = norm([as_tarfile_reads(row) for row in list_rows(r.stdout)])
+            want = norm([(escape_name(n), len(d), t) for (n, d, t) in ref])
+            check(f"readable-list: {label}", r.returncode == 0 and got == want,
+                  f"rc={r.returncode} lean={got} expected={want}")
+            r = run_lean("manifest", str(path), "out")
+            got = norm_skip([skip_as_tarfile_reads(l) for l in output_lines(r.stdout)])
+            want = norm_skip(expected_manifest(ref))
+            check(f"readable-manifest: {label}", r.returncode == 0 and got == want,
+                  f"rc={r.returncode} lean={got} expected={want}")
+
+    # 8. Axiom check: Verify.lean prints the axioms of exactly the
     # theorems in THEOREMS, and each depends on the three standard axioms
-    # at most. Any other axiom, `sorryAx` included, fails the check.
-    ax = subprocess.run(["lake", "env", "lean", "TarPilot/Verify.lean"],
-                        cwd=PILOT_DIR, capture_output=True, text=True)
-    ax_out = ax.stdout + ax.stderr
-    check("axioms-run", ax.returncode == 0, ax_out[:400])
-    allowed = {"propext", "Classical.choice", "Quot.sound"}
-    records = {}
-    for m in re.finditer(r"'([\w.]+)' depends on axioms: \[(.*?)\]", ax_out, re.DOTALL):
-        records[m.group(1)] = {a.strip() for a in m.group(2).split(",") if a.strip()}
-    for m in re.finditer(r"'([\w.]+)' does not depend on any axioms", ax_out):
-        records[m.group(1)] = set()
-    expected = set(THEOREMS)
-    check("axioms-names", set(records) == expected,
-          f"printed {sorted(records)}, expected {sorted(expected)}")
-    for name, used in sorted(records.items()):
-        check(f"axioms-{name}", used <= allowed, f"axioms: {sorted(used)}")
-
-    axiom_checks = len(records) + 2
+    # at most. Any other axiom, `sorryAx` included, fails the check. It
+    # reads this checkout's proofs, so it is left out with `--tool`.
+    if rev is None:
+        ax = subprocess.run(["lake", "env", "lean", "TarPilot/Verify.lean"],
+                            cwd=PILOT_DIR, capture_output=True, text=True)
+        ax_out = ax.stdout + ax.stderr
+        check("axioms-run", ax.returncode == 0, ax_out[:400])
+        allowed = {"propext", "Classical.choice", "Quot.sound"}
+        records = {}
+        for m in re.finditer(r"'([\w.]+)' depends on axioms: \[(.*?)\]", ax_out, re.DOTALL):
+            records[m.group(1)] = {a.strip() for a in m.group(2).split(",") if a.strip()}
+        for m in re.finditer(r"'([\w.]+)' does not depend on any axioms", ax_out):
+            records[m.group(1)] = set()
+        expected = set(THEOREMS)
+        check("axioms-names", set(records) == expected,
+              f"printed {sorted(records)}, expected {sorted(expected)}")
+        for name, used in sorted(records.items()):
+            check(f"axioms-{name}", used <= allowed, f"axioms: {sorted(used)}")
+        axiom_checks = len(records) + 2
+
     lean_ver = subprocess.run(["lean", "--version"], capture_output=True,
                               text=True).stdout.strip()
 
+    if rev is None:
+        header = [f"Run by `tests/run_tests.py` against Python's `tarfile` module."]
+        count = f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)"
+    else:
+        header = [
+            f"Run by `tests/run_tests.py --tool {rev}` against Python's `tarfile` module.",
+            f"The tool was built from commit {rev}, not from this checkout. The axiom",
+            "check reads this checkout's proofs, not the tool, so it is left out.",
+        ]
+        count = f"- Checks run: {checks}, all on the tool"
     lines = [
         "# Test results",
         "",
-        f"Run by `tests/run_tests.py` against Python's `tarfile` module.",
-        f"Lean: {lean_ver}. Python: {sys.version.split()[0]}.",
+        *header,
+        f"Lean: {lean_ver}. Python: {sys.version.split()[0]}. System tar: {tar_version()}.",
         "",
-        f"- Checks run: {checks} ({axiom_checks} of them on the axioms of the theorems)",
+        count,
         f"- Failures: {len(failures)}",
         f"- Archive A entries compared (list and manifest): {len(ref_entries)}",
         f"- Manifest outcome on archive A: {ok_count} extracted, "
         f"{rej_count} rejected by the path gate, {skip_count} skipped as non-regular",
         f"- Files written by the Lean `create` command and read back by Python: {len(files)}",
-        "- Broken inputs rejected with exit code 1: truncated archive, "
+        "- Broken inputs that must fail with exit code 1: truncated archive, "
         "random garbage, corrupted checksum",
+        f"- Archives in formats the pilot does not read, which must fail with exit code 1 "
+        f"under `list` and `manifest`: {unsupported}",
+        f"- Archives in other formats it reads, compared with tarfile under `list` and "
+        f"`manifest`: {readable}",
         "",
-        "Axiom check (`TarPilot/Verify.lean`):",
-        "",
-        "```",
-        ax_out.strip(),
-        "```",
+        "How the output is compared with tarfile. tarfile drops the `/` at the end of a",
+        "directory name, so directory names in `list` and names in `SKIP` lines are",
+        "compared without it. tarfile also reads an entry with typeflag NUL and a name",
+        "ending in `/` as a directory, typeflag 5, so for the readable archives the",
+        "tool's typeflag 0 on such an entry is read as 5. Every other typeflag is",
+        "compared as printed.",
         "",
     ]
+    if rev is None:
+        lines += ["Axiom check (`TarPilot/Verify.lean`):", "", "```", ax_out.strip(), "```", ""]
     if failures:
         lines += ["## Failures", ""] + [f"- {f}" for f in failures] + [""]
-    RESULTS.write_text("\n".join(lines))
-    print(f"{checks - len(failures)}/{checks} checks passed; results in {RESULTS}")
+    results.write_text("\n".join(lines))
+    print(f"{checks - len(failures)}/{checks} checks passed; results in {results}")
     return 1 if failures else 0