diff --git a/Main.lean b/Main.lean
index 13448dc..e603f4c 100644
--- a/Main.lean
+++ b/Main.lean
@@ -43,14 +43,12 @@ def runManifest (file dest : String) : IO UInt32 := do
   | some entries =>
     let destCs := if dest = "" then [] else dest.splitOn "/"
     for e in entries do
-      if isRegular e then
-        match gate e.name with
-        | none => IO.println s!"REJECT\t{e.name}"
-        | some rel =>
-          let path := String.intercalate "/" (destCs ++ rel)
-          IO.println s!"OK\t{path}\t{e.data.size}\t{byteSum e.data}"
-      else
-        IO.println s!"SKIP\t{e.name}\t{e.typeflag.toNat}"
+      match extractEntry destCs e with
+      | some (path, bytes) =>
+        IO.println s!"OK\t{joinPath path}\t{bytes.size}\t{byteSum bytes}"
+      | none =>
+        if isRegular e then IO.println s!"REJECT\t{e.name}"
+        else IO.println s!"SKIP\t{e.name}\t{e.typeflag.toNat}"
     return 0
 
 def runCreate (out : String) (files : List String) : IO UInt32 := do
diff --git a/README.md b/README.md
index 8a4f55f..1644d22 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # tar: a tar extractor that cannot escape its destination
 
-This repo reads a tar archive (ustar format) and extracts regular files into an in-memory list of paths and file contents. Every path it emits is built by joining the destination with a cleaned relative path. A machine-checked proof shows the cleaned path can never climb out of the destination.
+This repo reads a tar archive (ustar format) and extracts regular files into an in-memory list of paths and file contents. Every path it emits is built by joining the destination with a cleaned relative path. A machine-checked proof covers the joined string: resolving a relative POSIX path lexically, without symlinks, leaves it inside the resolved destination. This tool writes no extracted files to disk.
 
 It is the first Proven Commons project. The org's home repo, [mission](https://github.com/Proven-Commons/mission), publishes the verified bar it is measured against. Status: built, not yet verified. The [bar audit of 2026-10-24](https://github.com/Proven-Commons/mission/blob/main/reviews/tar/2026-10-24-bar-audit.md) found that the bar is not yet met, and lists the fixes.
 
@@ -21,12 +21,15 @@ lake build
 
 The path gate and the extraction rule, in `TarPilot/Path.lean` and `TarPilot/Archive.lean`:
 
-- `gate_sound`: a name that passes the gate gives relative components with no `..`, no empty component, no `.`, and the list is not empty.
-- `cleanComponents_sound`: the component cleaner behind the gate has the same properties.
-- `extractAll_safe`: every path the extractor emits is the destination components followed by a gated relative path, so no emitted path escapes the destination.
-- `extractArchive_safe`: the same guarantee for an archive read from bytes.
+- `cleanComponents_plain` and `gate_plain`: accepted components are plain names, with no empty name, `.`, `..`, embedded `/`, or NUL. The gate also requires a nonempty result. The original `cleanComponents_sound` and `gate_sound` guarantees remain available.
+- `extractEntry_contained` and `extractAll_contained`: every accepted path is the destination components followed by a nonempty list of plain names.
+- `extractAll_joined`: rendering those components with `joinPath` and splitting the string on `/` recovers the destination followed by the plain names. This assumes the destination components themselves contain no `/`, as when the CLI splits its destination argument.
+- `extractAll_resolves_inside` and `extractEntry_resolves_inside`: resolving that rendered string with the relative POSIX lexical resolver in `Path.lean` gives the resolved destination followed by the plain names, under the same destination assumption. Archive names cannot add a parent traversal above the destination. The resolver preserves leading `..`; it does not model absolute-root handling, Windows paths, or symlinks.
+- `extractAll_safe` and `extractArchive_safe`: the original component-list guarantee, including extraction from archive bytes.
 
-The gate rules: absolute names are rejected. Any `..` component is rejected. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files (typeflag `0` or NUL) are extracted. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination.
+The CLI's `OK` lines call `extractEntry` and `joinPath`, the same functions used by these statements. `extractAll` filters the results of `extractEntry`. The CLI adds only `REJECT` and `SKIP` diagnostics for entries with no extracted result, preserving archive order. Parsing, diagnostics, and formatting sizes and byte sums remain outside the proof.
+
+The gate rules: absolute names are rejected. Any `..` component is rejected, as is a component containing `/` or NUL. Empty and `.` components are dropped. A name with nothing left is rejected. Only regular files (typeflag `0` or NUL) are extracted. Directory, link, and other entries are skipped, so a link entry cannot place a later entry outside the destination.
 
 Axiom check: each proof depends only on the standard Lean axioms (`propext`, `Classical.choice`, `Quot.sound`, or a subset). Full output is recorded in `tests/TEST-RESULTS.md`.
 
@@ -34,10 +37,10 @@ Axiom check: each proof depends only on the standard Lean axioms (`propext`, `Cl
 
 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`: 16 checks, 0 failures, on 14 archive entries covering normal files, hostile names, a long name split over the ustar prefix field, 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`: the original 14 archive entries and create/readback checks, plus 524 path cases (512 random, seed `20261024`) under eight destinations. Manifest comparisons preserve duplicate names and entry order; `posixpath` independently checks containment of emitted paths. Lean regressions cover embedded separators, NUL, the old theorem's traversal counterexample, and lexical resolution. Broken inputs cover truncated archives, garbage, and bad checksums.
 - 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, symlinked destination folders) is outside this project for now.
-- Names that are not valid UTF-8 read as empty and are rejected by the gate. GNU tar extensions (longname entries, pax headers), base-256 size fields, and sparse files are not supported. An archive using them fails to parse instead of being read in a wrong way.
-- The Lean compiler, runtime, and kernel are trusted, as in every Lean project. A bug in them is outside the proof.
+- Invalid UTF-8 becomes an empty header field. With a split ustar name, a valid prefix or name can survive while the invalid field is lost. GNU longname and pax path overrides are ignored rather than reliably rejected, so extension-bearing archives can produce incorrect names. Base-256 sizes and sparse files are not supported. Typeflag `7` (contiguous file) is skipped even though Python treats it as regular. These parser and compatibility findings from the audit remain open; use the pilot only for its supported ustar subset.
+- The Lean compiler, runtime, kernel, and hardware are trusted. The tests also rely on Python's `tarfile` and `posixpath` as oracles. Bugs in these are outside the proof.
 
 ## Re-check it
 
@@ -47,7 +50,7 @@ lake env lean TarPilot/Verify.lean
 python3 tests/run_tests.py
 ```
 
-The build fails if a proof breaks. The second command prints the axiom list. The test script rebuilds if needed, reruns every comparison, and rewrites `tests/TEST-RESULTS.md`.
+The build checks the proofs, but accepts `sorry` with a warning. The second command prints the axiom list. The test script always rebuilds, runs the Lean regressions and every comparison, and rewrites `tests/TEST-RESULTS.md`. It requires each named theorem's axiom list to contain only `propext`, `Classical.choice`, and `Quot.sound`, so `sorryAx` and custom axioms fail the tests.
 
 ## Layout
 
@@ -58,3 +61,4 @@ The build fails if a proof breaks. The second command prints the axiom list. The
 - `TarPilot/Verify.lean`: the axiom check.
 - `Main.lean`: the command line front end.
 - `tests/run_tests.py`: differential tests against Python's `tarfile`.
+- `tests/PathSafety.lean`: path safety regressions, including the old statement's counterexample.
diff --git a/TarPilot/Archive.lean b/TarPilot/Archive.lean
index b3af75d..d1806e1 100644
--- a/TarPilot/Archive.lean
+++ b/TarPilot/Archive.lean
@@ -2,10 +2,10 @@
   Whole-archive parsing, extraction, and writing.
 
   The extraction rule is the proved part, together with the path gate
-  in `Path.lean`: `extractAll` only emits a path built as
-  `dest ++ rel`, where `rel` passed the gate, and the theorem
-  `extractAll_safe` states that every emitted relative path has no
-  `..`, no empty component, no `.`, and is not empty.
+  in `Path.lean`: the CLI and `extractAll` both call `extractEntry`.
+  Each emitted path is `dest ++ rel`, where `rel` is a nonempty list
+  of plain names. The containment theorems also cover joining the
+  components into a string and resolving that relative path lexically.
 
   Parsing and writing are covered by differential tests against
   Python's `tarfile` module (see `tests/`), not by a proof.
@@ -57,43 +57,96 @@ def parseArchive (data : ByteArray) : Option (List RawEntry) :=
 def isRegular (e : RawEntry) : Bool :=
   e.typeflag == '0' || e.typeflag == Char.ofNat 0
 
+/-- The extraction decision shared by the CLI and the in-memory model. -/
+def extractEntry (dest : List String) (e : RawEntry) : Option (List String × ByteArray) :=
+  if isRegular e then
+    (gate e.name).map fun rel => (dest ++ rel, e.data)
+  else none
+
+/-- An accepted entry extends the destination by nonempty plain names. -/
+theorem extractEntry_contained (dest : List String) (e : RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (h : extractEntry dest e = some (path, bytes)) :
+    ∃ rel, rel ≠ [] ∧ path = dest ++ rel ∧ ∀ c ∈ rel, PlainName c := by
+  unfold extractEntry at h
+  split at h
+  · cases hg : gate e.name with
+    | none => simp [hg] at h
+    | some rel =>
+      simp only [hg, Option.map_some, Option.some.injEq, Prod.mk.injEq] at h
+      obtain ⟨hp, hne⟩ := gate_plain e.name rel hg
+      exact ⟨rel, hne, h.1.symm, hp⟩
+  · simp at h
+
 /-- Extract entries into a list of `(path, data)` pairs, in memory.
     The path of each pair is the destination components followed by the
     gated relative components of the entry name. -/
 def extractAll (dest : List String) (entries : List RawEntry) :
     List (List String × ByteArray) :=
-  entries.filterMap fun e =>
-    if isRegular e then
-      (gate e.name).map fun rel => (dest ++ rel, e.data)
-    else none
+  entries.filterMap (extractEntry dest)
+
+/-- Every emitted relative path is nonempty and contains only plain names,
+    including the absence of embedded separators and NUL. -/
+theorem extractAll_contained (dest : List String) (entries : List RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (h : (path, bytes) ∈ extractAll dest entries) :
+    ∃ rel, rel ≠ [] ∧ path = dest ++ rel ∧ ∀ c ∈ rel, PlainName c := by
+  obtain ⟨e, _, he⟩ := List.mem_filterMap.mp h
+  exact extractEntry_contained dest e path bytes he
 
 /-- Every path `extractAll` emits is the destination followed by a
     gated relative path: no `..`, no empty component, no `.`, and the
-    relative path is not empty. So no emitted path escapes the
-    destination. -/
+    relative path is not empty. This is the original component-list
+    guarantee; see `extractAll_resolves_inside` for the joined string. -/
 theorem extractAll_safe : ∀ (dest : List String) (entries : List RawEntry)
     (path : List String) (bytes : ByteArray),
     (path, bytes) ∈ extractAll dest entries →
     ∃ rel, path = dest ++ rel ∧
       ".." ∉ rel ∧ "" ∉ rel ∧ "." ∉ rel ∧ rel ≠ [] := by
   intro dest entries path bytes h
-  unfold extractAll at h
-  rw [List.mem_filterMap] at h
-  obtain ⟨e, _, hfe⟩ := h
-  by_cases hreg : isRegular e
-  · rw [if_pos hreg] at hfe
-    cases hg : gate e.name with
-    | none =>
-      rw [hg] at hfe
-      simp at hfe
-    | some rel =>
-      rw [hg] at hfe
-      simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at hfe
-      obtain ⟨hpath, _⟩ := hfe
-      obtain ⟨h1, h2, h3, h4⟩ := gate_sound e.name rel hg
-      exact ⟨rel, hpath.symm, h1, h2, h3, h4⟩
-  · rw [if_neg hreg] at hfe
-    exact absurd hfe (by simp)
+  obtain ⟨rel, hne, heq, hp⟩ := extractAll_contained dest entries path bytes h
+  exact ⟨rel, heq, fun hm => (hp _ hm).2.2.1 rfl,
+    fun hm => (hp _ hm).1 rfl, fun hm => (hp _ hm).2.1 rfl, hne⟩
+
+/-- Rendering a path and splitting it again preserves the destination
+    and plain relative names. Destination components must be slash-free. -/
+theorem extractAll_joined (dest : List String) (entries : List RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (hdest : ∀ d ∈ dest, '/' ∉ d.toList)
+    (h : (path, bytes) ∈ extractAll dest entries) :
+    ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧
+      pathComponents (joinPath path) = dest ++ rel := by
+  obtain ⟨rel, hne, hpath, hplain⟩ := extractAll_contained dest entries path bytes h
+  refine ⟨rel, hne, hplain, ?_⟩
+  subst hpath
+  apply pathComponents_join
+  · intro s hs
+    rcases List.mem_append.mp hs with hs | hs
+    · exact hdest s hs
+    · exact (hplain s hs).2.2.2.1
+  · simp [hne]
+
+/-- The rendered path resolves to the resolved destination followed by
+    plain names. This is lexical containment of a relative POSIX path,
+    without symlinks; it is not a theorem about filesystem writes. -/
+theorem extractAll_resolves_inside (dest : List String) (entries : List RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (hdest : ∀ d ∈ dest, '/' ∉ d.toList)
+    (h : (path, bytes) ∈ extractAll dest entries) :
+    ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧
+      resolve [] (pathComponents (joinPath path)) = resolve [] dest ++ rel := by
+  obtain ⟨rel, hne, hplain, hjoin⟩ := extractAll_joined dest entries path bytes hdest h
+  exact ⟨rel, hne, hplain, by rw [hjoin, resolve_append, resolve_plain rel _ hplain]⟩
+
+/-- The same joined-string guarantee for the decision the CLI calls. -/
+theorem extractEntry_resolves_inside (dest : List String) (e : RawEntry)
+    (path : List String) (bytes : ByteArray)
+    (hdest : ∀ d ∈ dest, '/' ∉ d.toList)
+    (h : extractEntry dest e = some (path, bytes)) :
+    ∃ rel, rel ≠ [] ∧ (∀ c ∈ rel, PlainName c) ∧
+      resolve [] (pathComponents (joinPath path)) = resolve [] dest ++ rel := by
+  apply extractAll_resolves_inside dest [e] path bytes hdest
+  exact List.mem_filterMap.mpr ⟨e, by simp, h⟩
 
 /-- Parse, then extract. -/
 def extractArchive (dest : List String) (data : ByteArray) :
diff --git a/TarPilot/Path.lean b/TarPilot/Path.lean
index 300ee2b..4ecc395 100644
--- a/TarPilot/Path.lean
+++ b/TarPilot/Path.lean
@@ -1,31 +1,32 @@
 /-
-  Path safety for tar entry names.
-
-  A tar entry name is untrusted input. Before an entry may be extracted,
-  its name goes through `gate`, which produces a list of path components
-  that is proved to contain no `..`, no empty component, and no `.`,
-  and to be non-empty. Extraction joins those components under a
-  destination, so every extracted path stays under the destination by
-  construction (see `Archive.extractAll_safe`).
+  Path safety for tar entry names. Plain names exclude empty, dot,
+  dot-dot, slash and NUL. The lexical resolver models relative POSIX
+  paths without symlinks; filesystem writes remain outside the model.
+
+  Containment lemmas adapted from the F1 evidence in Proven-Commons/mission,
+  reviews/tar/evidence/Contained.lean (98521c0).
 -/
 
 namespace TarPilot
 
-/-- Split a tar entry name into path components. -/
+/-- Split an untrusted archive name into path components. -/
 def components (name : String) : List String :=
   name.splitOn "/"
 
-/-- Drop empty and `.` components. Fail if any component is `..`. -/
+/-- A component that names one entry inside its directory. -/
+def PlainName (c : String) : Prop :=
+  c ≠ "" ∧ c ≠ "." ∧ c ≠ ".." ∧ '/' ∉ c.toList ∧ Char.ofNat 0 ∉ c.toList
+
+/-- Drop empty and dot components; reject dot-dot, embedded `/`, or NUL. -/
 def cleanComponents : List String → Option (List String)
   | [] => some []
   | c :: cs =>
-    if c = ".." then none
+    if c = ".." ∨ '/' ∈ c.toList ∨ Char.ofNat 0 ∈ c.toList then none
     else (cleanComponents cs).map (fun rest =>
       if c = "" ∨ c = "." then rest else c :: rest)
 
-theorem cleanComponents_sound : ∀ (cs : List String) (out : List String),
-    cleanComponents cs = some out →
-    ".." ∉ out ∧ "" ∉ out ∧ "." ∉ out := by
+theorem cleanComponents_plain : ∀ (cs out : List String),
+    cleanComponents cs = some out → ∀ c ∈ out, PlainName c := by
   intro cs
   induction cs with
   | nil =>
@@ -35,69 +36,117 @@ theorem cleanComponents_sound : ∀ (cs : List String) (out : List String),
     simp
   | cons c cs ih =>
     intro out h
-    rw [cleanComponents] at h
-    by_cases hpar : c = ".."
-    · rw [if_pos hpar] at h
-      exact absurd h (by simp)
-    · rw [if_neg hpar] at h
+    unfold cleanComponents at h
+    split at h
+    · simp at h
+    · rename_i hbad
       cases hrec : cleanComponents cs with
       | none =>
         rw [hrec] at h
         simp at h
       | some rest =>
         rw [hrec] at h
-        obtain ⟨h1, h2, h3⟩ := ih rest hrec
-        by_cases hskip : c = "" ∨ c = "."
-        · rw [Option.map_some] at h
-          rw [if_pos hskip] at h
-          injection h with h'
-          subst h'
-          exact ⟨h1, h2, h3⟩
-        · rw [Option.map_some] at h
-          rw [if_neg hskip] at h
-          injection h with h'
-          subst h'
-          have hn1 : c ≠ "" := fun hc => hskip (Or.inl hc)
-          have hn2 : c ≠ "." := fun hc => hskip (Or.inr hc)
-          refine ⟨?_, ?_, ?_⟩
-          · simp only [List.mem_cons, not_or]
-            exact ⟨fun hh => hpar hh.symm, h1⟩
-          · simp only [List.mem_cons, not_or]
-            exact ⟨fun hh => hn1 hh.symm, h2⟩
-          · simp only [List.mem_cons, not_or]
-            exact ⟨fun hh => hn2 hh.symm, h3⟩
-
-/-- The gate every entry name must pass before extraction.
-    Absolute names are rejected. `..` is rejected. Empty and `.`
-    components are dropped. A name with nothing left is rejected. -/
+        simp only [Option.map_some, Option.some.injEq] at h
+        have ih' := ih rest hrec
+        split at h
+        · subst h
+          exact ih'
+        · rename_i hskip
+          subst h
+          intro x hx
+          simp only [List.mem_cons] at hx
+          rcases hx with rfl | hx
+          · simp only [not_or] at hbad hskip
+            exact ⟨hskip.1, hskip.2, hbad.1, hbad.2.1, hbad.2.2⟩
+          · exact ih' x hx
+
+/-- Reject absolute names and require a nonempty cleaned relative path. -/
 def gate (name : String) : Option (List String) :=
   if name.startsWith "/" then none
   else match cleanComponents (components name) with
     | some (r :: rs) => some (r :: rs)
     | _ => none
 
-theorem gate_sound : ∀ (name : String) (rel : List String),
-    gate name = some rel →
-    ".." ∉ rel ∧ "" ∉ rel ∧ "." ∉ rel ∧ rel ≠ [] := by
-  intro name rel h
+/-- Accepted relative paths are nonempty lists of plain names. -/
+theorem gate_plain (name : String) (rel : List String) (h : gate name = some rel) :
+    (∀ c ∈ rel, PlainName c) ∧ rel ≠ [] := by
   unfold gate at h
-  by_cases habs : name.startsWith "/" = true
-  · rw [if_pos habs] at h
-    exact absurd h (by simp)
-  · rw [if_neg habs] at h
-    cases hclean : cleanComponents (components name) with
-    | none =>
-      rw [hclean] at h
-      exact absurd h (by simp)
-    | some out =>
-      rw [hclean] at h
-      obtain ⟨h1, h2, h3⟩ := cleanComponents_sound _ _ hclean
-      cases out with
-      | nil =>
-        exact absurd h (by simp)
-      | cons r rs =>
-        injection h with h'
-        subst h'
-        exact ⟨h1, h2, h3, by simp⟩
+  split at h
+  · simp at h
+  · split at h
+    · rename_i r rs hc
+      injection h with h
+      subst h
+      exact ⟨cleanComponents_plain _ _ hc, by simp⟩
+    · simp at h
+
+/-- The original cleaner guarantee, retained for callers. -/
+theorem cleanComponents_sound (cs out : List String) (h : cleanComponents cs = some out) :
+    ".." ∉ out ∧ "" ∉ out ∧ "." ∉ out := by
+  have hp := cleanComponents_plain cs out h
+  exact ⟨fun hm => (hp _ hm).2.2.1 rfl,
+    fun hm => (hp _ hm).1 rfl, fun hm => (hp _ hm).2.1 rfl⟩
+
+/-- The original gate guarantee, retained for callers. -/
+theorem gate_sound (name : String) (rel : List String) (h : gate name = some rel) :
+    ".." ∉ rel ∧ "" ∉ rel ∧ "." ∉ rel ∧ rel ≠ [] := by
+  obtain ⟨hp, hne⟩ := gate_plain name rel h
+  exact ⟨fun hm => (hp _ hm).2.2.1 rfl,
+    fun hm => (hp _ hm).1 rfl, fun hm => (hp _ hm).2.1 rfl, hne⟩
+
+/-- The components a system sees in a path string: the parts between `/`. -/
+def pathComponents (s : String) : List String :=
+  (s.split '/').toList.map (·.copy)
+
+/-- Render components with the POSIX separator. Used by the CLI and the theorems. -/
+def joinPath (path : List String) : String :=
+  String.intercalate "/" path
+
+theorem pathComponents_join (l : List String) (hl : ∀ s ∈ l, '/' ∉ s.toList)
+    (hne : l ≠ []) : pathComponents (joinPath l) = l := by
+  have h := String.toList_split_intercalate (c := '/') hl
+  simp only [hne, ite_false] at h
+  exact h
+
+/-- Resolve the components of a relative path as POSIX does, without
+    symlinks: `..` drops the last component, or is kept when nothing is
+    left to drop or the last is itself `..`; empty and `.` change nothing. -/
+def resolve : List String → List String → List String
+  | acc, [] => acc
+  | acc, c :: cs =>
+    if c = "" ∨ c = "." then resolve acc cs
+    else if c = ".." then
+      if acc = [] ∨ acc.getLast? = some ".." then resolve (acc ++ [".."]) cs
+      else resolve acc.dropLast cs
+    else resolve (acc ++ [c]) cs
+
+theorem resolve_append : ∀ (xs ys acc : List String),
+    resolve acc (xs ++ ys) = resolve (resolve acc xs) ys := by
+  intro xs
+  induction xs with
+  | nil => intro ys acc; simp [resolve]
+  | cons c cs ih =>
+    intro ys acc
+    simp only [List.cons_append, resolve]
+    split
+    · exact ih ys _
+    · split
+      · split
+        · exact ih ys _
+        · exact ih ys _
+      · exact ih ys _
+
+theorem resolve_plain : ∀ (rel acc : List String), (∀ c ∈ rel, PlainName c) →
+    resolve acc rel = acc ++ rel := by
+  intro rel
+  induction rel with
+  | nil => intro acc _; simp [resolve]
+  | cons c cs ih =>
+    intro acc h
+    have ⟨h1, h2, h3, _, _⟩ := h c (by simp)
+    have hcs : ∀ x ∈ cs, PlainName x := fun x hx => h x (by simp [hx])
+    simp only [resolve, h1, h2, h3, or_self, ite_false]
+    rw [ih _ hcs]
+    simp
 
 end TarPilot
diff --git a/TarPilot/Verify.lean b/TarPilot/Verify.lean
index 483c242..eaa83ba 100644
--- a/TarPilot/Verify.lean
+++ b/TarPilot/Verify.lean
@@ -11,3 +11,10 @@ import TarPilot.Archive
 #print axioms TarPilot.cleanComponents_sound
 #print axioms TarPilot.extractAll_safe
 #print axioms TarPilot.extractArchive_safe
+#print axioms TarPilot.cleanComponents_plain
+#print axioms TarPilot.gate_plain
+#print axioms TarPilot.extractEntry_contained
+#print axioms TarPilot.extractAll_contained
+#print axioms TarPilot.extractAll_joined
+#print axioms TarPilot.extractAll_resolves_inside
+#print axioms TarPilot.extractEntry_resolves_inside
diff --git a/tests/PathSafety.lean b/tests/PathSafety.lean
new file mode 100644
index 0000000..b564b14
--- /dev/null
+++ b/tests/PathSafety.lean
@@ -0,0 +1,33 @@
+import TarPilot
+
+open TarPilot
+
+-- The old cleaner accepted a whole traversal path as one component.
+#guard cleanComponents ["a/../../etc/passwd"] == none
+#guard cleanComponents ["ok", "bad" ++ String.singleton (Char.ofNat 0)] == none
+#guard gate "a/../../etc/passwd" == none
+#guard gate "./a//b/./" == some ["a", "b"]
+#guard gate "././" == none
+
+-- The old statement holds of this component, yet its rendered path escapes.
+example : ".." ∉ ["a/../../etc/passwd"] ∧ "" ∉ ["a/../../etc/passwd"] ∧
+    "." ∉ ["a/../../etc/passwd"] := by decide
+example : ¬ PlainName "a/../../etc/passwd" := by
+  unfold PlainName
+  decide
+#guard resolve [] (pathComponents (joinPath ["out", "a/../../etc/passwd"])) ==
+    ["etc", "passwd"]
+
+-- The resolver must preserve leading parents and reduce internal parents.
+#guard resolve [] ["..", "..", "out", ".", "", "nested", "..", "file"] ==
+    ["..", "..", "out", "file"]
+#guard pathComponents (joinPath ["out", "", "nested", "file"]) ==
+    ["out", "", "nested", "file"]
+
+-- Mixed outcomes must preserve the order and data of the accepted entries.
+private def entry (name : String) (typeflag : Char := '0') : RawEntry :=
+  { name, typeflag, data := ByteArray.mk #[65] }
+
+#guard (extractAll ["out"] [entry "./a//b", entry "../evil", entry "link" '2',
+    entry "./", entry "last" (Char.ofNat 0)]).map (fun p => (joinPath p.1, p.2.toList)) ==
+    [("out/a/b", [65]), ("out/last", [65])]
diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md
index df8d2eb..e0751f7 100644
--- a/tests/TEST-RESULTS.md
+++ b/tests/TEST-RESULTS.md
@@ -1,20 +1,29 @@
 # 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.12.3.
+Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release). Python: 3.12.14.
 
-- Checks run: 16
+- Checks run: 40
 - Failures: 0
 - Archive A entries compared (list and manifest): 14
 - Manifest outcome on archive A: 9 extracted, 3 rejected by the path gate, 2 skipped as non-regular
 - Files written by the Lean `create` command and read back by Python: 3
+- Path regression entries: 524 (512 random, seed 20261024), compared with the spec under 8 destinations and checked with `posixpath`
+- `tests/PathSafety.lean`: cleaner, gate, joined-path and relative-resolution regressions
 - Broken inputs rejected with exit code 1: truncated archive, random garbage, corrupted checksum
 
 Axiom check (`TarPilot/Verify.lean`):
 
 ```
 'TarPilot.gate_sound' depends on axioms: [propext, Classical.choice, Quot.sound]
-'TarPilot.cleanComponents_sound' depends on axioms: [propext]
+'TarPilot.cleanComponents_sound' depends on axioms: [propext, Classical.choice, Quot.sound]
 'TarPilot.extractAll_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
 'TarPilot.extractArchive_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.cleanComponents_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.gate_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.extractEntry_contained' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.extractAll_contained' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.extractAll_joined' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.extractAll_resolves_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
+'TarPilot.extractEntry_resolves_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
 ```
diff --git a/tests/run_tests.py b/tests/run_tests.py
index 10fbf25..5bafdd8 100644
--- a/tests/run_tests.py
+++ b/tests/run_tests.py
@@ -7,14 +7,16 @@
 
     python3 tests/run_tests.py
 
-It builds the Lean project if the executable is missing, runs all
+It builds the Lean project, runs all
 cases in a temporary directory, writes `tests/TEST-RESULTS.md`, and
 exits non-zero if any case fails.
 """
 
 import io
 import os
+import posixpath
 import random
+import re
 import subprocess
 import sys
 import tarfile
@@ -24,6 +26,9 @@
 PILOT_DIR = Path(__file__).resolve().parent.parent
 EXE = PILOT_DIR / ".lake" / "build" / "bin" / "tar-pilot"
 RESULTS = PILOT_DIR / "tests" / "TEST-RESULTS.md"
+PATH_SEED = 20261024
+PATH_RANDOM_CASES = 512
+DESTINATIONS = ("", ".", "out", "out/", "./out//nested/..", "../dest", "/tmp/out", "/")
 
 checks = 0
 failures = []
@@ -52,7 +57,7 @@ def spec_gate(name):
         return None
     out = []
     for comp in name.split("/"):
-        if comp == "..":
+        if comp == ".." or "\0" in comp:
             return None
         if comp in ("", "."):
             continue
@@ -102,7 +107,7 @@ def build_archive_a(path):
     return entries
 
 
-def expected_manifest(entries_data):
+def expected_manifest(entries_data, dest="out"):
     """Expected manifest lines from the spec, in archive order.
     entries_data: list of (name, data, typeflag_byte)."""
     lines = []
@@ -114,14 +119,18 @@ def expected_manifest(entries_data):
         if rel is None:
             lines.append(f"REJECT\t{name}")
         else:
-            joined = "/".join(["out"] + rel)
+            joined = "/".join((dest.split("/") if dest else []) + rel)
             lines.append(f"OK\t{joined}\t{len(data)}\t{sum(data)}")
     return lines
 
 
 def main():
-    if not EXE.exists():
-        subprocess.run(["lake", "build"], cwd=PILOT_DIR, check=True)
+    # Rebuild even if the binary exists: source edits must reach the tests.
+    subprocess.run(["lake", "build"], cwd=PILOT_DIR, check=True)
+    regression = subprocess.run(["lake", "env", "lean", "tests/PathSafety.lean"],
+                                cwd=PILOT_DIR, capture_output=True, text=True)
+    check("path-regressions", regression.returncode == 0,
+          regression.stdout + regression.stderr)
 
     with tempfile.TemporaryDirectory() as td:
         td = Path(td)
@@ -213,16 +222,61 @@ def main():
         r = run_lean("list", str(badsum))
         check("bad-checksum-fails", r.returncode == 1, f"rc={r.returncode}")
 
-    # 6. Axiom check: only the three standard axioms.
+        # 6. Exercise the actual CLI extraction decision with repeated names,
+        # hostile components and mixed outcomes, under varied destinations.
+        rng = random.Random(PATH_SEED)
+        names = ["../evil", "a/../../etc/passwd", "/abs", "", ".", "././", "a//b",
+                 "./a/./b/", "same", "same", "trailing/", "..."]
+        alphabet = ("a", "b", "..", ".", "", "...", "file.txt")
+        names += ["/".join(rng.choices(alphabet, k=rng.randrange(1, 9)))
+                  for _ in range(PATH_RANDOM_CASES)]
+        path_archive = td / "paths.tar"
+        with tarfile.open(path_archive, "w", format=tarfile.USTAR_FORMAT) as tf:
+            for i, name in enumerate(names):
+                ti = tarfile.TarInfo(name)
+                ti.type = (tarfile.REGTYPE, tarfile.AREGTYPE,
+                           tarfile.SYMTYPE, tarfile.DIRTYPE)[i % 4]
+                # tarfile treats legacy NUL-type names ending in '/' as
+                # directories; keep their headers free of regular-file data.
+                if ti.type == tarfile.AREGTYPE and name.endswith("/"):
+                    ti.type = tarfile.REGTYPE
+                data = bytes([i % 256]) * (i % 17)
+                ti.size = len(data) if ti.type in (tarfile.REGTYPE, tarfile.AREGTYPE) else 0
+                tf.addfile(ti, io.BytesIO(data) if ti.size else None)
+        with tarfile.open(path_archive) as tf:
+            path_entries = [(m.name, tf.extractfile(m).read() if m.isreg() else b"", m.type[0])
+                            for m in tf.getmembers()]
+        check("path-reference-count", len(path_entries) == len(names),
+              f"read {len(path_entries)} of {len(names)} generated entries")
+        for dest in DESTINATIONS:
+            r = run_lean("manifest", str(path_archive), dest)
+            actual = norm_skip(r.stdout.splitlines())
+            expected = norm_skip(expected_manifest(path_entries, dest))
+            differences = [(i, a, b) for i, (a, b) in enumerate(zip(actual, expected)) if a != b]
+            check(f"path-manifest-{dest!r}", r.returncode == 0 and actual == expected,
+                  f"rc={r.returncode}, stderr={r.stderr}, lengths={len(actual)}/{len(expected)}, "
+                  f"differences={differences[:3]}")
+            root = posixpath.normpath(posixpath.join("/sandbox", dest))
+            emitted = [line.split("\t")[1] for line in actual if line.startswith("OK\t")]
+            resolved = [posixpath.normpath(posixpath.join("/sandbox", path)) for path in emitted]
+            check(f"path-containment-{dest!r}", bool(resolved) and all(
+                posixpath.commonpath([root, path]) == root and path != root for path in resolved),
+                f"root={root}, paths={resolved[:5]}")
+
+    # 7. Axiom check: every named theorem must print only standard axioms.
     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])
-    for thm in ["gate_sound", "cleanComponents_sound", "extractAll_safe",
-                "extractArchive_safe"]:
-        check(f"axioms-{thm}", thm in ax_out, ax_out[:400])
-    bad_axioms = [w for w in ["sorryAx"] if w in ax_out]
-    check("axioms-no-sorry", not bad_axioms, ax_out[:400])
+    allowed_axioms = {"propext", "Classical.choice", "Quot.sound"}
+    for thm in ["gate_sound", "cleanComponents_sound", "extractAll_safe", "extractArchive_safe",
+                "cleanComponents_plain", "gate_plain", "extractEntry_contained", "extractAll_contained",
+                "extractAll_joined", "extractAll_resolves_inside", "extractEntry_resolves_inside"]:
+        match = re.search(rf"^'TarPilot\.{thm}' depends on axioms: \[([^\]]*)\]$", ax_out, re.M)
+        no_axioms = f"'TarPilot.{thm}' does not depend on any axioms" in ax_out.splitlines()
+        axioms = {a.strip() for a in match[1].split(",") if a.strip()} if match else set()
+        check(f"axioms-{thm}", (match is not None or no_axioms) and axioms <= allowed_axioms,
+              f"missing theorem or unexpected axioms: {sorted(axioms - allowed_axioms)}; {ax_out[:400]}")
 
     lean_ver = subprocess.run(["lean", "--version"], capture_output=True,
                               text=True).stdout.strip()
@@ -239,6 +293,9 @@ def main():
         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)}",
+        f"- Path regression entries: {len(path_entries)} ({PATH_RANDOM_CASES} random, seed {PATH_SEED}), "
+        f"compared with the spec under {len(DESTINATIONS)} destinations and checked with `posixpath`",
+        "- `tests/PathSafety.lean`: cleaner, gate, joined-path and relative-resolution regressions",
         "- Broken inputs rejected with exit code 1: truncated archive, "
         "random garbage, corrupted checksum",
         "",