diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 06a3cea..961ffad 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -71,28 +71,33 @@ tasks-completed = [
 ]
 
 [coq-proof-status]
-admitted = 3
+admitted = 0
 axioms-justified = 1
 admitted-detail = """
-3 Admitted markers as of 2026-06-02 post-PR #55 design-gap surfacing:
-
-  1. mkdir_two_dirs_reversible (filesystem_composition.v:697) — non-LIFO
-     sequence reversal; not derivable from two_op_sequence_reversible as
-     stated. Tracked as #56 (restate as LIFO sequence).
-
-  2. overwrite_pass_equalizes_storage (rmo_operations.v:422) — model gap.
-     Needs Hgeom strengthening or conclusion relaxation. Tracked as #57.
-
-  3. obliterate_not_injective (rmo_operations.v:535) — downstream of #57;
-     reconnects once #57 closes. Tracked as #58.
-
-The prior single_op_reversible OpRmdir admit (declared 2026-04-19) was
-Qed-closed by PR #67 (2026-06-01) via OpMkdirWithPerms +
-OpCreateFileWithPerms constructor-variant approach — zero new axioms.
+0 Admitted markers. Re-verified 2026-07-16 with `coqc` + `Print Assumptions`
+under Coq 8.18.0: the full _CoqProject (11 files) compiles with zero
+admit/Admitted/Axiom markers. The 3 admits recorded here on 2026-06-02 are all
+now Qed-closed:
+
+  1. mkdir_two_dirs_reversible (filesystem_composition.v:681, now an Example)
+     — CLOSED (#56); Print Assumptions: functional_extensionality_dep only.
+
+  2. overwrite_pass_equalizes_storage (rmo_operations.v:398) — CLOSED (#57);
+     Print Assumptions: Closed under the global context (zero axioms).
+
+  3. obliterate_not_injective (rmo_operations.v:530) — CLOSED (#58);
+     Print Assumptions: functional_extensionality_dep only.
+
+The single_op_reversible OpRmdir model-permission admit (declared 2026-04-19)
+was Qed-closed via OpMkdirWithPerms + OpCreateFileWithPerms constructor variants
+— zero new axioms. The 1 real gap the audit historically tracked
+(obliterate_overwrites_all_blocks) is CLOSED: Print Assumptions reports Closed
+under the global context. Remaining Coq assumptions: functional_extensionality_dep
+(stdlib standard) + is_empty_dir_dec (1 justified classical).
 """
 axiom-detail = "is_empty_dir_dec: Filesystem = Path -> option FSNode is infinite-domain; universal quantification over all paths is not constructively decidable. Migration: switch to FMaps.t FSNode."
-proof-debt-items-closed = [1, 2]
-proof-debt-open = [3]
+proof-debt-items-closed = [1, 2, 3]
+proof-debt-open = []
 
 [dogfooding-status]
 # Section present per CRG v2.0 schema. Honest disclosure follows.
diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml
index af42601..3004b0b 100644
--- a/.machine_readable/bot_directives/methodology.a2ml
+++ b/.machine_readable/bot_directives/methodology.a2ml
@@ -98,7 +98,7 @@ constraints = [
   "Lean -> Rust correspondence is property-tested only (~85% confidence), NOT mechanised — closing this is the critical-path blocker to v1.0.0",
   "Elixir NIF build is broken — impl/elixir/ is reference-only; do not block work on it",
   "BEAM daemon is designed but not implemented — no current SNIF carrier",
-  "Coq has 1 remaining real proof gap: obliterate_overwrites_all_blocks (mechanical induction over overwrite passes) — see docs/PROOF_HOLES_AUDIT.md",
+  "Coq has 0 remaining real proof gaps: obliterate_overwrites_all_blocks is CLOSED (Print Assumptions: Closed under the global context, re-verified 2026-07-16 under Coq 8.18.0) — see docs/PROOF_HOLES_AUDIT.md",
   "Agda has 1 structural axiom (funext) — provable in cubical Agda, intentional in intensional TT",
   "Coq has 1 justified decidability axiom (is_empty_dir_dec) — infinite-domain Filesystem = Path -> option FSNode; switching to FMaps.t FSNode is the documented migration",
   "RMO (GDPR / secure deletion) primitives are stubs in impl/rust-cli/src/commands/secure_deletion.rs — proofs exist for the model, runtime does not yet bind to them",
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index ada4200..af92a87 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -17,6 +17,59 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Full POSIX shell compliance (subset)
 - RMO (Remove-Match-Obliterate) proofs for GDPR compliance
 
+=== Added — 2026-07-16
+
+==== Launcher
+- `just run` (alias `just launch`) — the user-facing launcher for the `vsh`
+  shell, previously missing. Builds and starts the interactive REPL; passes
+  extra arguments through to the binary (`just run --version`,
+  `just run script.vsh`). Verified end-to-end: `--version` prints `vsh 0.9.0`
+  (exit 0), the REPL banner starts interactively, and script execution runs and
+  exits 0.
+- `QUICKSTART-USER.adoc` rewritten from the unfilled RSR template to the real,
+  working flow — it no longer references non-existent recipes (`just setup`,
+  `just uninstall`, `just stapeln-run`, `just install --portable`); every `just`
+  command it now cites is a real recipe (verified via `just --show`). Uninstall
+  documents the honest `cargo uninstall vsh` path.
+
+=== Verified — 2026-07-16
+
+==== Proofs
+- Coq proof-debt re-verified to **0 admits / 0 real gaps** under Coq
+  8.18.0. The full `_CoqProject` (11 files) compiles with no
+  `admit`/`Admitted`/`Axiom` markers. `Print Assumptions` on the
+  load-bearing theorems: `obliterate_overwrites_all_blocks` and
+  `overwrite_pass_equalizes_storage` are *Closed under the global
+  context* (zero axioms); `single_op_reversible`,
+  `operation_sequence_reversible`, `copy_file_reversible`,
+  `mkdir_two_dirs_reversible`, `obliterate_not_injective` depend only on
+  the standard `functional_extensionality_dep`. The historically-tracked
+  "1 real gap" (`obliterate_overwrites_all_blocks`) and the three
+  2026-06-02 admits (#56/#57/#58) are all closed. Remaining assumptions
+  are standard/justified: Coq `functional_extensionality` (stdlib) +
+  `is_empty_dir_dec` (justified classical), Agda `funext` (structural).
+  Docs reconciled: `PROOF_HOLES_AUDIT.md`, `README.adoc`, `FAQ.adoc`,
+  `CLAUDE.md`, `docs/wiki/`, `ROADMAP*.{adoc,md}`,
+  `.machine_readable/6a2/STATE.a2ml`, `bot_directives/methodology.a2ml`.
+
+=== Fixed — 2026-07-16
+
+==== Build / tooling
+- `just build-coq` and `scripts/verify-proofs.sh` now succeed from a
+  clean checkout. Both previously compiled an incomplete file subset
+  (missing `filesystem_composition.v` and others), so `posix_errors.v`
+  failed with "Cannot find a physical path bound to logical path
+  filesystem_composition"; both now compile the full `_CoqProject`
+  chain in dependency order and `mkdir -p extracted` before
+  `extraction.v` (the gitignored output dir), matching the CI oracle in
+  `validation.yml`.
+- `scripts/verify-proofs.sh`: fixed two latent `set -e` bugs that
+  aborted the script before any test ran — `((VAR++))` counters
+  (post-increment returns the pre-value, so the first bump from 0
+  yields exit status 1) replaced with assignment form; and per-test
+  `cd` side effects that leaked between tests are now isolated by
+  running each test command in a subshell.
+
 === Added — 2026-06-02
 
 ==== Implementation
diff --git a/CLAUDE.md b/CLAUDE.md
index dba45db..1d82708 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -86,7 +86,7 @@ The Rust CLI is a functional interactive shell with these features:
 
 - 21,331 lines of Rust across 32 source files (`find impl/rust-cli/src -name '*.rs' | wc -l`; `wc -l` aggregate, measured 2026-06-01)
 - ~478 theorem candidates across 6 proof systems + Idris2 ABI layer (per issue #42 deep-audit inventory, 2026-06-01)
-- 3 proof holes remaining: 1 real gap (Coq `obliterate_overwrites_all_blocks`), 1 justified axiom (Coq `is_empty_dir_dec` — infinite-domain decidability), 1 structural axiom (Agda `funext` — standard in intensional TT) — see `docs/PROOF_HOLES_AUDIT.md`
+- 2 proof holes remaining, **0 real gaps**: 1 justified axiom (Coq `is_empty_dir_dec` — infinite-domain decidability), 1 structural axiom (Agda `funext` — standard in intensional TT). The former real gap (Coq `obliterate_overwrites_all_blocks`) is CLOSED — re-verified 2026-07-16 via `Print Assumptions` (*Closed under the global context*) under Coq 8.18.0 — see `docs/PROOF_HOLES_AUDIT.md`
 - Idris2 ABI layer: **0 proof holes** (all closed 2026-07-01, issue #151 root — builds under `--total`), 0 `partial` markers, 2 registered primitive-eq axioms (`axStringEqRefl`, `axBits8EqRefl`; gated by `.github/scripts/check-idris2-believe-me.sh`)
 - 7 fuzz targets in `impl/rust-cli/fuzz/fuzz_targets/` (parser, arith, job-spec, signal-parse, path-ops, glob-expansion, state-machine)
 
@@ -95,7 +95,7 @@ The Rust CLI is a functional interactive shell with these features:
 ### Critical Priority
 
 1. **No mechanized Lean -> Rust correspondence** — testing only, ~85% confidence
-2. **1 real proof gap** remaining (Coq `obliterate_overwrites_all_blocks` — mechanical induction over overwrite passes), plus 2 documented axioms (1 justified decidability + 1 structural funext) — see `docs/PROOF_HOLES_AUDIT.md`
+2. **0 real proof gaps** — the former Coq `obliterate_overwrites_all_blocks` gap is CLOSED (re-verified 2026-07-16, *Closed under the global context*); 2 documented axioms remain (1 justified decidability + 1 structural funext) — see `docs/PROOF_HOLES_AUDIT.md`
 3. **NOT production-ready** — research prototype only
 
 ### High Priority
@@ -191,7 +191,7 @@ valence-shell/
     mcp/                # MCP server bindings
   proofs/
     lean4/              # Primary proof source (101 theorems)
-    coq/                # CIC proofs + extraction (131 theorems, 3 admits in extraction.v)
+    coq/                # CIC proofs + extraction (131 theorems, 0 admits — re-verified 2026-07-16, Coq 8.18.0)
     agda/               # Type theory proofs (85 theorems, 3 postulates including funext)
     isabelle/           # HOL proofs (76 theorems)
     mizar/              # Set theory proofs (63 theorems)
@@ -326,7 +326,7 @@ MPL-2.0 (Palimpsest License)
 
 ---
 
-**Last Updated**: 2026-06-01 (drift reconcile: 32 src files / 21,331 LoC, 3 proof holes per audit, 478 theorem candidates, 7 fuzz targets)
+**Last Updated**: 2026-07-16 (Coq proof-debt re-verified: 0 admits / 0 real gaps under Coq 8.18.0; 2 justified/structural axioms remain. Prior 2026-06-01 drift reconcile: 32 src files / 21,331 LoC, 478 theorem candidates, 7 fuzz targets)
 **Version**: see `CHANGELOG.md` (release history) and `impl/rust-cli/Cargo.toml` `[package].version` (semver pin)
 **Status**: Advanced research prototype — NOT production-ready
 **Tests**: 736 passing, 0 failures, 14 ignored
diff --git a/FAQ.adoc b/FAQ.adoc
index 064fd4d..b2f1828 100644
--- a/FAQ.adoc
+++ b/FAQ.adoc
@@ -86,8 +86,9 @@ deep-audit inventory in `docs/audits/2026-06-01-deep-audit.adoc`.
 What is solid:
 
 * The 6-system proofs of the model-layer operations. ~478 theorem candidates;
-  1 real gap remaining (Coq `obliterate_overwrites_all_blocks`) + 2 documented
-  axioms (1 justified decidability + 1 structural funext).
+  0 real gaps (Coq `obliterate_overwrites_all_blocks` CLOSED, re-verified
+  2026-07-16 via `Print Assumptions` under Coq 8.18.0) + 2 documented axioms
+  (1 justified decidability + 1 structural funext).
 * The Rust CLI. 736 tests passing, 0 failures, 7 fuzz targets, working shell
   surface (pipelines, redirections, here-docs, job control, variables, control
   structures, glob, quoting).
@@ -116,12 +117,12 @@ plus the Idris2 ABI layer, distributed as:
 |===
 |System |Count |Notes
 |Lean 4 |101 |Primary source of truth
-|Coq |131 |Includes `extraction.v` — 3 admits remaining
+|Coq |131 |Includes `extraction.v` — 0 admits (re-verified 2026-07-16, Coq 8.18.0)
 |Isabelle/HOL |76 |Cross-validation
 |Agda |85 |3 postulates remaining (including funext)
 |Mizar |63 |Set-theoretic foundation
 |Z3 SMT |125 asserts |Automated decision procedures
-|Idris2 (ABI + filesystem) |~22 |2 holes + 10 partial markers
+|Idris2 (ABI + filesystem) |~22 |0 holes, 0 partials, 2 primitive-eq axioms (closed #151/#152)
 |===
 
 If you see a stale number elsewhere in the repo, please file an issue —
@@ -178,8 +179,8 @@ Valence-shell follows the estate boundary-convention policy
 (`feedback_estate_boundary_conventions`):
 
 * In-process FFI (Rust ↔ C) — Zig scaffolding in `impl/zig/`.
-* Formal ABI / proof carrier — Idris2 in `proofs/idris2/` (~22 theorems, 2 holes,
-  10 partial markers per issue #42).
+* Formal ABI / proof carrier — Idris2 in `proofs/idris2/` (~22 theorems, 0 holes,
+  0 partial markers, 2 primitive-eq axioms; closed via #151/#152, builds under `--total`).
 * BEAM ↔ native — would use SNIFs; not currently wired (BEAM daemon is
   designed but not implemented).
 * Compile target / typed-wasm — not currently a target.
diff --git a/Justfile b/Justfile
index 11d5368..a9a131a 100644
--- a/Justfile
+++ b/Justfile
@@ -4,6 +4,9 @@
 # Default recipe - show available commands
 import? "contractile.just"
 
+# `just launch` is a synonym for `just run` (launch the vsh shell)
+alias launch := run
+
 default:
     @just --list
 
@@ -15,13 +18,22 @@ build-all: build-coq build-lean4 build-agda build-isabelle build-mizar build-idr
 verify-all:
     @./scripts/verify-proofs.sh
 
-# Build Coq proofs
+# Build Coq proofs (full _CoqProject chain, in dependency order)
 build-coq:
     @echo "Building Coq proofs..."
-    cd proofs/coq && coqc filesystem_model.v
-    cd proofs/coq && coqc file_operations.v
-    cd proofs/coq && coqc posix_errors.v
-    cd proofs/coq && coqc extraction.v
+    # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
+    cd proofs/coq && mkdir -p extracted
+    cd proofs/coq && coqc -R . ValenceShell filesystem_model.v
+    cd proofs/coq && coqc -R . ValenceShell file_operations.v
+    cd proofs/coq && coqc -R . ValenceShell file_content_operations.v
+    cd proofs/coq && coqc -R . ValenceShell copy_move_operations.v
+    cd proofs/coq && coqc -R . ValenceShell symlink_operations.v
+    cd proofs/coq && coqc -R . ValenceShell permission_operations.v
+    cd proofs/coq && coqc -R . ValenceShell filesystem_composition.v
+    cd proofs/coq && coqc -R . ValenceShell filesystem_equivalence.v
+    cd proofs/coq && coqc -R . ValenceShell posix_errors.v
+    cd proofs/coq && coqc -R . ValenceShell rmo_operations.v
+    cd proofs/coq && coqc -R . ValenceShell extraction.v
     @echo "✓ Coq proofs compiled"
 
 # Build Lean 4 proofs
@@ -68,7 +80,8 @@ verify-idris2: build-idris2
 # Extract Coq to OCaml
 extract:
     @echo "Extracting Coq to OCaml..."
-    cd proofs/coq && coqc extraction.v
+    # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
+    cd proofs/coq && mkdir -p extracted && coqc extraction.v
     @echo "✓ OCaml code extracted"
 
 # Build OCaml FFI (legacy)
@@ -113,6 +126,14 @@ test-cli:
     cd impl/rust-cli && cargo test
     @echo "✓ Rust CLI tests passed"
 
+# Launch the interactive vsh shell (the primary deliverable). Extra args pass
+# through to the binary:
+#   just run              # start the interactive REPL
+#   just run --version    # print version and exit
+#   just run script.vsh   # run a script
+run *ARGS:
+    cd impl/rust-cli && cargo run -- {{ARGS}}
+
 # Build all FFI layers
 build-ffi: build-ffi-zig build-ffi-ocaml
     @echo "✓ All FFI layers built"
diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc
index 63248ab..6d1e93d 100644
--- a/QUICKSTART-USER.adoc
+++ b/QUICKSTART-USER.adoc
@@ -1,125 +1,123 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-// Template: QUICKSTART-USER.adoc — 5-minute path to working software
-// Replace valence-shell, Valence Shell — See README.adoc for details., just run, Valence Shell started successfully. with actuals
 = valence-shell — Quick Start for Users
 :toc:
 :toclevels: 2
 
 == What is valence-shell?
 
-Valence Shell — See README.adoc for details.
+Valence Shell (`vsh`) is a formally verified, reversible Unix-style shell: its
+core filesystem operations are backed by machine-checked proofs, and it provides
+a proven undo/redo layer, named checkpoints, and proof-annotated dry runs. See
+link:README.adoc[README.adoc] for the full overview.
 
-== Prerequisites
-
-Before you begin, ensure you have:
-
-* **just** — task runner (https://github.com/casey/just[install guide])
-* Platform-specific requirements listed below
-
-[cols="1,3"]
-|===
-| Platform | Additional Requirements
+[IMPORTANT]
+====
+v0.9.0 is an **advanced research prototype — NOT production-ready**. Great for
+learning and experimentation; do not use it as your login shell or trust it with
+irreplaceable data.
+====
 
-| Linux
-| See README.adoc
-
-| macOS
-| See README.adoc
+== Prerequisites
 
-| Windows
-| See README.adoc
-|===
+* **Rust toolchain 1.88+** — to build and run the `vsh` CLI
+  (https://rustup.rs[install via rustup]).
+* **just** — task runner (https://github.com/casey/just[install guide]).
 
-== Install
+The six proof systems (Coq, Lean 4, Agda, Isabelle, Mizar, Z3) are **optional** —
+they are only needed to re-check the formal proofs, not to build or run the shell.
 
-=== Option 1: Standard Install (recommended)
+== Launch it (fastest path)
 
 [source,bash]
 ----
-# Clone and set up
 git clone https://github.com/hyperpolymath/valence-shell.git
 cd valence-shell
-just setup
-----
-
-The setup script will:
 
-* Detect your platform and shell
-* Install missing dependencies (with your permission)
-* Configure the application
-* Offer install location choices
-* Run a self-diagnostic to verify everything works
+just run          # build (debug) and start the interactive shell
+# or, equivalently:
+just launch
+----
 
-=== Option 2: Container (via Stapeln)
+`just run` passes any extra arguments through to the binary:
 
 [source,bash]
 ----
-just stapeln-run
+just run --version        # print version and exit
+just run path/to/script   # execute a script non-interactively
 ----
 
-=== Option 3: Portable (no system changes)
+Expected first-run output is the `vsh` banner followed by an interactive prompt.
+Type `help` for commands, `undo` to reverse the last operation, and `exit` to
+leave.
+
+== Build / install
 
 [source,bash]
 ----
-just install --portable --prefix=./valence-shell-portable
+just build-cli     # release build -> impl/rust-cli/target/release/vsh
+just install-cli   # cargo install to ~/.cargo/bin (then just run `vsh`)
+just test-cli      # run the CLI test suite
 ----
 
-== First Run
+After `just install-cli`, the `vsh` binary is on your `PATH`:
 
 [source,bash]
 ----
-just run
+vsh --version
+vsh                # start the shell
 ----
 
-Expected output:
+You can also drive Cargo directly if you prefer:
 
-[source]
+[source,bash]
 ----
-Valence Shell started successfully.
+cd impl/rust-cli
+cargo run                       # start the interactive shell
+cargo build --release           # build the release binary
+./target/release/vsh --version
 ----
 
-== Self-Diagnostic
-
-If something isn't working:
+== Run in a container
 
 [source,bash]
 ----
-just doctor
+just container-build    # build the container image (uses Containerfile)
+just container-run      # run verification in the container
+just container-shell    # interactive shell inside the container
 ----
 
-This checks all dependencies, permissions, paths, and connectivity.
-If it finds issues, it will suggest fixes.
-
-To attempt automatic repair:
+== Self-diagnostic
 
 [source,bash]
 ----
-just heal
+just doctor    # check required tools, hardcoded paths, environment
+just heal      # attempt automatic repair (permissions, stale caches)
 ----
 
-== Get Help
+== Get help
 
-* **In-app**: `just run --help`
 * **Guided tour**: `just tour`
-* **Report a problem**: `just help-me` (pre-fills diagnostic context)
+* **Report a problem** (pre-fills platform diagnostics): `just help-me`
+* **All recipes**: `just --list`
+* **In-shell help**: type `help` at the `vsh` prompt, or `vsh --help`
 * **Wiki**: https://github.com/hyperpolymath/valence-shell/wiki
 
 == Uninstall
 
+If you installed with `just install-cli` (which uses `cargo install`):
+
 [source,bash]
 ----
-just uninstall
+cargo uninstall vsh
 ----
 
-You will be asked:
-
-1. Which uninstall tier (Bennett reversible, parameter-based, standard, or secure)
-2. Whether to include or exclude your data
-3. Whether to clear caches and LLM models
+A source checkout leaves nothing outside the repository directory — delete the
+clone to remove it. Build artifacts can be cleared with `just clean`.
 
-== Next Steps
+== Next steps
 
-* Read the link:README.adoc[README] for full feature overview
-* Read the link:EXPLAINME.adoc[EXPLAINME] for architecture and design decisions
-* Try `just tour` for a guided walkthrough
+* link:README.adoc[README] — full feature overview and verification status
+* link:EXPLAINME.adoc[EXPLAINME] — architecture and the claims-vs-evidence trail
+* link:docs/USER_GUIDE.md[User Guide] — detailed usage
+* link:FAQ.adoc[FAQ] — common questions
diff --git a/README.adoc b/README.adoc
index b2b216d..9c05782 100644
--- a/README.adoc
+++ b/README.adoc
@@ -42,7 +42,7 @@ Valence Shell is a formally verified shell with proven reversibility guarantees.
 == Formal Verification
 * [x] Formally Proven Reversibility: `rmdir(mkdir(p, fs)) = fs`
 * [x] Polyglot Verification: 6 proof systems (Coq, Lean 4, Agda, Isabelle, Mizar, Z3)
-* [x] ~478 Theorem Candidates: Proven across different logical foundations (1 real gap, 1 justified axiom, 1 structural axiom remain — see `docs/PROOF_HOLES_AUDIT.md`)
+* [x] ~478 Theorem Candidates: Proven across different logical foundations (0 real gaps; 1 justified axiom + 1 structural axiom remain — see `docs/PROOF_HOLES_AUDIT.md`)
 * [x] Content Operations: File read/write with proven reversibility
 * [x] MAA Framework: Mutually Assured Accountability with audit trails
 
@@ -358,8 +358,8 @@ Valence Shell sits inside a three-layer architecture; the other two layers are u
 * If preconditions hold, `write(p, old, write(p, new, fs)) = fs`
 * Operations on `p1` don't affect `p2` (when `p1 ≠ p2`)
 * Composition: sequences of operations reverse correctly
-* ~478 theorem candidates proven across 6 verification systems (1 real gap + 2 axioms remain — see `docs/PROOF_HOLES_AUDIT.md`)
-* 2026-06-02 snapshot: 4 admits in `proofs/coq/rmo_operations.v` are annotated with explicit obligations; Idris2 0.8.0 keyword/parse fixes landed alongside (#112/#113/#115/#117) and the build oracle is strict (#118).
+* ~478 theorem candidates proven across 6 verification systems (0 real gaps; 2 justified/structural axioms remain — see `docs/PROOF_HOLES_AUDIT.md`)
+* 2026-07-16 re-verification: `proofs/coq/` compiles with **0 admits** under Coq 8.18.0; `Print Assumptions` on the load-bearing theorems reports *Closed under the global context* or dependence only on standard `functional_extensionality`. Idris2 0.8.0 keyword/parse fixes landed earlier (#112/#113/#115/#117), the build oracle is strict (#118), and the Idris2 layer is hole-free (#151/#152).
 
 === ❌ What Is NOT Guaranteed
 
@@ -604,7 +604,7 @@ See link:LICENSE[LICENSE] for full text.
 
 **Made with ❤️ by humans and AI, for humans who value formal correctness.**
 
-**Status**: Advanced Research Prototype (v0.9.0) | **RSR**: PLATINUM (105/100) | **Proofs**: ~478 theorem candidates (1 real gap remaining) | **Tests**: 736 passing
+**Status**: Advanced Research Prototype (v0.9.0) | **RSR**: PLATINUM (105/100) | **Proofs**: ~478 theorem candidates (0 real gaps; 2 justified axioms) | **Tests**: 736 passing
 
 [.text-center]
 _"Every operation reversible. Every claim proven. Every contributor valued."_
diff --git a/ROADMAP.adoc b/ROADMAP.adoc
index 10a9ea0..a98639d 100644
--- a/ROADMAP.adoc
+++ b/ROADMAP.adoc
@@ -106,8 +106,9 @@ Hard requirements before any v1.0 claim:
 
 * [ ] Mechanized Lean → Rust correspondence (currently property testing
   only, ~85% confidence).
-* [ ] Close all real gaps in `docs/PROOF_HOLES_AUDIT.md` (post-2026-04
-  sweep: 1 real gap, 1 justified axiom, 1 structural).
+* [x] Close all real gaps in `docs/PROOF_HOLES_AUDIT.md` — **DONE**
+  (re-verified 2026-07-16 under Coq 8.18.0): 0 real gaps; 1 justified axiom
+  (`is_empty_dir_dec`) + 1 structural (`funext`) remain.
 * [ ] CRG v2.0 grade B: 6+ diverse external targets, issues fed back.
   See audit `=== External validation` section for the proposed diverse-6
   shape.
diff --git a/docs/PROOF_HOLES_AUDIT.md b/docs/PROOF_HOLES_AUDIT.md
index 7054cd4..cf612f3 100644
--- a/docs/PROOF_HOLES_AUDIT.md
+++ b/docs/PROOF_HOLES_AUDIT.md
@@ -4,9 +4,23 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 # Proof Holes Audit - Valence Shell
 
-**Date**: 2026-07-01 (Idris2 layer closed to 0 holes — issue #151 root; prior: 2026-04-12 believe_me sweep, Coq layer)
+**Date**: 2026-07-16 (Coq real gap re-verified CLOSED via `coqc` + `Print Assumptions` under Coq 8.18.0; prior: 2026-07-01 Idris2 layer to 0 holes — issue #151 root; 2026-04-12 believe_me sweep, Coq layer)
 **Auditor**: Opus (deep audit + proof closure)
-**Total Holes**: 6 across the 4 closed-core proof systems tracked here (down from 31; -2 Coq axioms proved 2026-04-12)
+**Total Holes**: 2 (both standard/justified axioms; **0 real gaps**) across the closed-core proof systems tracked here
+
+> **2026-07-16 prover re-verification.** The full Coq tree (`_CoqProject`,
+> 11 files) compiles under Coq 8.18.0 with **zero `admit`/`Admitted`/`Axiom`**
+> markers. `Print Assumptions` on the load-bearing theorems reports:
+> `obliterate_overwrites_all_blocks` and `overwrite_pass_equalizes_storage` are
+> **Closed under the global context** (zero axioms); `single_op_reversible`,
+> `operation_sequence_reversible`, `copy_file_reversible`,
+> `mkdir_two_dirs_reversible`, `obliterate_not_injective` depend only on the
+> standard `functional_extensionality_dep`. The former "1 real gap"
+> (`obliterate_overwrites_all_blocks`) and the 2026-06-02 `single_op_reversible`
+> `OpRmdir` model-permission admit (closed via `OpMkdirWithPerms`) are both
+> **CLOSED**. Remaining assumptions are all standard/justified: Coq
+> `functional_extensionality_dep` (stdlib) + `is_empty_dir_dec` (justified
+> classical decidability), and Agda `funext` (structural).
 
 > **Idris2 ABI layer (tracked separately in `PROOF-NEEDS.md` /
 > `proofs/idris2/README.md`): 0 holes as of 2026-07-01.** All 17 `?holes` were
@@ -19,10 +33,10 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 | Category | Count | Change | Action Required |
 |----------|-------|--------|-----------------|
-| **Real Gaps** | 1 | -25 | Coq `obliterate_overwrites_all_blocks` only |
-| **Axioms** | 1 | -3 | `is_empty_dir_dec` only (justified, infinite-domain) |
-| **Structural** | 1 | -1 | `funext` only (`_≟ₚ_` proven via `_path-≟_`) |
-| **Total** | **3** | **-28** | Updated 2026-04-12: 2 well-formedness + 5 decidability proofs closed |
+| **Real Gaps** | 0 | -1 | **NONE** — `obliterate_overwrites_all_blocks` CLOSED (re-verified 2026-07-16) |
+| **Axioms** | 1 | 0 | `is_empty_dir_dec` only (justified, infinite-domain) |
+| **Structural** | 1 | 0 | `funext` only (`_≟ₚ_` proven via `_path-≟_`) |
+| **Total** | **2** | **-1** | Both remaining are standard/justified axioms; no proof debt |
 
 ### What Was Closed (2026-04-03 proof closure session)
 
@@ -92,13 +106,13 @@ Replaced with `obliterate_not_injective` — the correct formalization of "not r
 
 Also closed 2026-04-12: `posix_errors.v` 5/6 decidability predicates converted from Axiom to Lemma (constructive proofs). One justified Axiom remains: `is_empty_dir_dec` — `Filesystem = Path -> option FSNode` is an infinite-domain function; universal quantification over all paths cannot be discharged constructively. Migration: switch to `FMaps.t FSNode`.
 
-## Remaining Real Gaps (1)
+## Remaining Real Gaps (0)
 
-### RMO Storage Proofs (1 gap remaining — low priority)
+### RMO Storage Proofs — CLOSED 2026-07-16
 
-| File | Line | Theorem | Gap |
-|------|------|---------|-----|
-| `coq/rmo_operations.v` | 214 | `obliterate_overwrites_all_blocks` | Induction over overwrite passes |
+| File | Line | Theorem | Status |
+|------|------|---------|--------|
+| `coq/rmo_operations.v` | 315 | `obliterate_overwrites_all_blocks` | **CLOSED** — `Print Assumptions` → *Closed under the global context* (zero axioms). The "induction over overwrite passes" is discharged by the helper `multi_pass_overwrite_count_precise` (line 274, `induction patterns`). |
 
 ~~`lean4/RMOOperations.lean` `obliterate_not_injective`~~ **RESOLVED 2026-03-22** — Proved via
 three auxiliary lemmas (`overwriteBlock_determined_by_shape`, `overwritePathBlocks_storage_eq`,
@@ -109,7 +123,9 @@ overwrite pass, mapped blocks become byte-identical; remaining passes operate on
 ~~`agda/RMOOperations.agda` `obliterate-not-reversible`~~ **RESOLVED 2026-04-03** — FALSE statement
 replaced with proven `obliterate-not-injective` matching the Lean 4/Coq formulation.
 
-The Coq gap (`obliterate_overwrites_all_blocks`) requires similar mechanical induction.
+The Coq theorem (`obliterate_overwrites_all_blocks`) is now **proved** with the
+same mechanical induction pattern (helper `multi_pass_overwrite_count_precise`),
+re-verified 2026-07-16 as *Closed under the global context*.
 
 ### Agda Deferred Proofs — ALL RESOLVED 2026-04-03
 
@@ -126,7 +142,7 @@ The Coq gap (`obliterate_overwrites_all_blocks`) requires similar mechanical ind
 
 ## Recommendations
 
-1. **1 remaining gap is low priority** — Coq `obliterate_overwrites_all_blocks` requires mechanical induction, not conceptually hard
+1. **0 remaining real gaps** — Coq `obliterate_overwrites_all_blocks` is proved (re-verified 2026-07-16); no proof debt remains in the Coq tree
 2. **Axiom count is minimal** — 1 structural (funext), 2 well-formedness, 6 decidability, 1 Coq funext = all standard
 3. **Model improvement needed**: Parameterize `mkdir`/`createFile` with permissions for full reverse-direction reversibility
 4. **Consider**: Agda `--cubical` flag provides funext natively, removing the last structural axiom
diff --git a/docs/ROADMAP_TO_V1.md b/docs/ROADMAP_TO_V1.md
index b4023b8..921ec02 100644
--- a/docs/ROADMAP_TO_V1.md
+++ b/docs/ROADMAP_TO_V1.md
@@ -21,8 +21,9 @@ plan builds on.
 ## Where we are (audit-verified, 2026-07-07)
 
 - 736 tests passing, 0 failures (see CLAUDE.md test table)
-- 3 proof holes: 1 real gap (Coq `obliterate_overwrites_all_blocks`),
-  2 documented axioms; Idris2 ABI layer fully closed
+- 2 proof holes, **0 real gaps**: the Coq `obliterate_overwrites_all_blocks`
+  gap is CLOSED (re-verified 2026-07-16, *Closed under the global context*);
+  2 documented axioms remain; Idris2 ABI layer fully closed
 - Lean→Rust correspondence is **tested, not mechanized** (~85–95% confidence)
 - Not a full POSIX shell: word splitting in external args, `~user`,
   subshell `(...)`, SIGCHLD/Ctrl+Z incomplete (`docs/POSIX_COMPLIANCE.md`)
@@ -55,7 +56,7 @@ defaults — vetoable, not ratified by merging this document.
 | **A** | POSIX completeness: word splitting (quote-context threading), subshell `(...)`, `~user`, SIGCHLD/Ctrl+Z | #91, #94 | Keystone — one sustained agent; word splitting first |
 | **B** | Seam sealing: 3 prod `panic!`, 10 `unreachable!`, 28 TODOs | #86, #87, #88 | Pure fan-out, one PR per file |
 | **C** | Test/fuzz/bench expansion: 736→2000+ tests, 7→20 fuzz targets, 15→75 security tests, benches in CI | #82–#85 | Pure fan-out by category |
-| **D** | Proof expansion: 478 theorem candidates across 6 systems; close last Coq gap; restate #130 non-theorem | #76–#81, #130 | Fan-out by prover system |
+| **D** | Proof expansion: 478 theorem candidates across 6 systems; ~~close last Coq gap~~ (DONE — closed + re-verified 2026-07-16); restate #130 non-theorem | #76–#81, #130 | Fan-out by prover system |
 | **E** | Lean→Rust correspondence mechanization | #93 | Keystone — blocked on **D2** |
 | **F** | RMO/GDPR implementation (theory unblocked: #60/#61 closed) | #92 | Blocked on **D4**, then bounded single lane |
 | **G** | Ops hygiene: CI reds, charter, issue-state drift | — | Inline, done first |
diff --git a/docs/wiki/For-Developers.md b/docs/wiki/For-Developers.md
index 1f97fd7..9fd6217 100644
--- a/docs/wiki/For-Developers.md
+++ b/docs/wiki/For-Developers.md
@@ -65,9 +65,11 @@ is very high — the seL4/CompCert pattern.
 **Read the honest status first:** the project maintains a single source of truth
 for open proof holes —
 [`docs/PROOF_HOLES_AUDIT.md`](https://github.com/hyperpolymath/valence-shell/blob/main/docs/PROOF_HOLES_AUDIT.md).
-As of this writing: 1 real gap (Coq `obliterate_overwrites_all_blocks`), 1
-justified decidability axiom, and 1 structural `funext` axiom (Agda). The Idris2
-ABI layer is **hole-free** (closed under `--total`) with 2 registered
+As of this writing: **0 real gaps** (the former Coq `obliterate_overwrites_all_blocks`
+gap is CLOSED — re-verified 2026-07-16 via `Print Assumptions` as *Closed under
+the global context* under Coq 8.18.0), plus 2 documented axioms: 1 justified
+decidability axiom (`is_empty_dir_dec`) and 1 structural `funext` axiom (Agda).
+The Idris2 ABI layer is **hole-free** (closed under `--total`) with 2 registered
 primitive-equality axioms gated by CI.
 
 ## Contributing
diff --git a/docs/wiki/For-Users.md b/docs/wiki/For-Users.md
index 5ef19e4..0857dbd 100644
--- a/docs/wiki/For-Users.md
+++ b/docs/wiki/For-Users.md
@@ -18,18 +18,21 @@ detailed canonical guides live in the repository and are linked throughout.
 ## Install & run (the short path)
 
 The interactive shell is the Rust CLI in `impl/rust-cli/`. It needs only a Rust
-toolchain (1.88+); the six proof systems are **optional** and only needed if you
-want to re-check the proofs yourself.
+toolchain (1.88+) and [`just`](https://github.com/casey/just); the six proof
+systems are **optional** and only needed if you want to re-check the proofs
+yourself.
 
 ```bash
 git clone https://github.com/hyperpolymath/valence-shell.git
-cd valence-shell/impl/rust-cli
+cd valence-shell
 
-cargo build --release            # builds the `vsh` binary
-cargo run                        # start the interactive shell
-./target/release/vsh --version   # or run the release binary directly
+just run              # build and launch the interactive shell (alias: just launch)
+just run --version    # print version and exit
+just install-cli      # install `vsh` to ~/.cargo/bin, then just run `vsh`
 ```
 
+Prefer Cargo directly? `cd impl/rust-cli && cargo run` does the same thing.
+
 Canonical, longer install guide (containers, portable install, self-diagnostics):
 [`QUICKSTART-USER.adoc`](https://github.com/hyperpolymath/valence-shell/blob/main/QUICKSTART-USER.adoc).
 
diff --git a/docs/wiki/Verification-Status.md b/docs/wiki/Verification-Status.md
index a891d86..6801504 100644
--- a/docs/wiki/Verification-Status.md
+++ b/docs/wiki/Verification-Status.md
@@ -48,9 +48,15 @@ is proven; wiring it irrefutably to the code is the remaining research problem.
 
 ## Open proof holes (as of the latest audit)
 
-| Hole | System | Nature |
+**0 real gaps.** Re-verified 2026-07-16 with `coqc` + `Print Assumptions` under
+Coq 8.18.0: the full Coq tree compiles with zero `admit`/`Admitted`/`Axiom`
+markers, and the load-bearing theorems are *Closed under the global context* or
+depend only on standard `functional_extensionality`. The two remaining items are
+standard/justified axioms, not gaps:
+
+| Item | System | Nature |
 |------|--------|--------|
-| `obliterate_overwrites_all_blocks` | Coq | **1 real gap** — mechanical induction over overwrite passes |
+| `obliterate_overwrites_all_blocks` | Coq | **CLOSED** (was the one real gap) — *Closed under the global context* |
 | `is_empty_dir_dec` | Coq | Justified axiom (infinite-domain decidability) |
 | `funext` | Agda | Structural axiom (function extensionality; standard in intensional type theory) |
 
diff --git a/proofs/coq/.gitignore b/proofs/coq/.gitignore
index 07acdd6..7d92fde 100644
--- a/proofs/coq/.gitignore
+++ b/proofs/coq/.gitignore
@@ -34,3 +34,6 @@ dist/
 
 # Extracted OCaml code (output of extraction.v)
 extracted/
+
+# Coq Lia tactic cache (build artifact)
+.lia.cache
diff --git a/scripts/verify-proofs.sh b/scripts/verify-proofs.sh
index 0764ac8..30254e1 100755
--- a/scripts/verify-proofs.sh
+++ b/scripts/verify-proofs.sh
@@ -32,17 +32,19 @@ log_info() {
 
 log_success() {
     echo -e "${GREEN}[✓]${NC} $1"
-    ((PASSED_TESTS++))
+    # Assignment form (not ((VAR++))): post-increment returns the pre-value, so
+    # the first bump from 0 evaluates to 0 -> exit status 1 -> `set -e` aborts.
+    PASSED_TESTS=$((PASSED_TESTS + 1))
 }
 
 log_failure() {
     echo -e "${RED}[✗]${NC} $1"
-    ((FAILED_TESTS++))
+    FAILED_TESTS=$((FAILED_TESTS + 1))
 }
 
 log_skip() {
     echo -e "${YELLOW}[SKIP]${NC} $1"
-    ((SKIPPED_TESTS++))
+    SKIPPED_TESTS=$((SKIPPED_TESTS + 1))
 }
 
 # Check if command exists
@@ -59,12 +61,14 @@ run_test() {
     local name="$1"
     local cmd="$2"
 
-    ((TOTAL_TESTS++))
+    TOTAL_TESTS=$((TOTAL_TESTS + 1))
     log_info "Testing: $name"
 
+    # Run in a subshell so per-test `cd` side effects do not leak into the next
+    # test (commands are written as `cd proofs/X && ...` from the repo root).
     if $VERBOSE; then
         echo "Command: $cmd"
-        if eval "$cmd"; then
+        if ( eval "$cmd" ); then
             log_success "$name passed"
             return 0
         else
@@ -72,7 +76,7 @@ run_test() {
             return 1
         fi
     else
-        if eval "$cmd" &> /dev/null; then
+        if ( eval "$cmd" ) &> /dev/null; then
             log_success "$name passed"
             return 0
         else
@@ -87,21 +91,37 @@ echo "Valence Shell - Proof Verification"
 echo "========================================="
 echo ""
 
-# Coq Verification
+# Coq Verification (full _CoqProject chain, in dependency order)
 if check_command coqc; then
     log_info "Coq 8.x detected"
+    # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
+    mkdir -p proofs/coq/extracted
     run_test "Coq: filesystem_model.v" \
-        "cd proofs/coq && coqc filesystem_model.v"
+        "cd proofs/coq && coqc -R . ValenceShell filesystem_model.v"
     run_test "Coq: file_operations.v" \
-        "cd proofs/coq && coqc file_operations.v"
+        "cd proofs/coq && coqc -R . ValenceShell file_operations.v"
+    run_test "Coq: file_content_operations.v" \
+        "cd proofs/coq && coqc -R . ValenceShell file_content_operations.v"
+    run_test "Coq: copy_move_operations.v" \
+        "cd proofs/coq && coqc -R . ValenceShell copy_move_operations.v"
+    run_test "Coq: symlink_operations.v" \
+        "cd proofs/coq && coqc -R . ValenceShell symlink_operations.v"
+    run_test "Coq: permission_operations.v" \
+        "cd proofs/coq && coqc -R . ValenceShell permission_operations.v"
+    run_test "Coq: filesystem_composition.v" \
+        "cd proofs/coq && coqc -R . ValenceShell filesystem_composition.v"
+    run_test "Coq: filesystem_equivalence.v" \
+        "cd proofs/coq && coqc -R . ValenceShell filesystem_equivalence.v"
     run_test "Coq: posix_errors.v" \
-        "cd proofs/coq && coqc posix_errors.v"
+        "cd proofs/coq && coqc -R . ValenceShell posix_errors.v"
+    run_test "Coq: rmo_operations.v" \
+        "cd proofs/coq && coqc -R . ValenceShell rmo_operations.v"
     run_test "Coq: extraction.v" \
-        "cd proofs/coq && coqc extraction.v"
+        "cd proofs/coq && coqc -R . ValenceShell extraction.v"
 else
     log_skip "Coq not installed"
-    ((TOTAL_TESTS += 4))
-    ((SKIPPED_TESTS += 4))
+    ((TOTAL_TESTS += 11))
+    ((SKIPPED_TESTS += 11))
 fi
 
 echo ""
@@ -143,8 +163,8 @@ if check_command isabelle; then
         "cd proofs/isabelle && isabelle build -D ."
 else
     log_skip "Isabelle not installed"
-    ((TOTAL_TESTS++))
-    ((SKIPPED_TESTS++))
+    TOTAL_TESTS=$((TOTAL_TESTS + 1))
+    SKIPPED_TESTS=$((SKIPPED_TESTS + 1))
 fi
 
 echo ""
@@ -172,13 +192,13 @@ if check_command z3; then
             "z3 proofs/z3/filesystem.smt2"
     else
         log_skip "Z3 proofs not yet created"
-        ((TOTAL_TESTS++))
-        ((SKIPPED_TESTS++))
+        TOTAL_TESTS=$((TOTAL_TESTS + 1))
+        SKIPPED_TESTS=$((SKIPPED_TESTS + 1))
     fi
 else
     log_skip "Z3 not installed"
-    ((TOTAL_TESTS++))
-    ((SKIPPED_TESTS++))
+    TOTAL_TESTS=$((TOTAL_TESTS + 1))
+    SKIPPED_TESTS=$((SKIPPED_TESTS + 1))
 fi
 
 echo ""