fix(wiki): write-once capture and real CLI/formal-bounded verification (#874)

.codex/skills/verify-llm-wiki-formal/SKILL.md

@@ -0,0 +1,56 @@
+---
+name: verify-llm-wiki-formal
+description: "Use when changing PStack wiki raw-source write semantics, replay/collision handling, or proof claims requiring source-to-code alignment and bounded or TLA+ state verification."
+disable-model-invocation: true
+---
+
+# Formally analyze wiki source immutability (bounded)
+
+Derived from `skills/create-formal-verification-skill/SKILL.md`. This does **not** claim a completed external TLA+ check. The current executed-in-CI target is an exhaustive **bounded real-code state exploration**; a separate TLA+ specification is included for optional independent TLC validation.
+
+## Coverage and sync record
+
+- **Covered production commit:** `bed363e12c5bb31459b263b4d6d9da409a15db80` (the wiki safety implementation in `scripts/llm_wiki.py`; confirm the diff to the current head before using).
+- **Target code:** `scripts/llm_wiki.py::ingest_file` (`dest.open("xb")`, conflict refusal, exact replay), `check_wiki` path checks and `main` CLI. Only `ingest_file` is modeled by the bounded checker.
+- **Safety property:** Once a basename has captured bytes in a wiki root, later ingests under the bounded event alphabet cannot change them; identical replay must not fail.
+- **Bound:** all ordered traces of length 1, 2 and 3 over `{shared.md:A, shared.md:B, other.md:C}` = **39** histories, serialized calls through production Python, isolated temp roots. This is not proof of all byte strings, arbitrary process interleavings, race-free directory ancestry, crash durability, or source→log transactional atomicity.
+- **Code-alignment rule:** after changing any listed ingest path or source destination, inspect `git diff bed363e..HEAD -- scripts/llm_wiki.py`, reason about linearization, update this skill's sync commit only after the tests and negative mutant still agree with the new implementation.
+
+## Model and checker choice
+
+`scripts/verify_llm_wiki_model.py` is a small finite-state exhaustive test harness that calls real production code for each trace and asserts immutability and replay semantics. The explicit mutant `broken_overwrite` must trigger a counterexample. This bounds the **real code path**, unlike a standalone state model.
+
+Optional `model/WikiRawImmutability.tla` and `.cfg` express a smaller abstract `raw/original` transition invariant for TLC. Run TLC **only with independently installed, pinned Java + TLC jar** and record the version, state count and exact command. Missing TLC/Java means `BLOCKED`, not PASS. TLC results would apply to the abstract model, not prove actual Python concurrency.
+
+## Launch
+
+No live service. Python 3.10+ and pytest for bounded code-level checks. TLC is optional. Use the Codex [functional verifier](../verify-llm-wiki/SKILL.md) for CLI user paths.
+
+## Doctor
+
+`python3 -m pytest -q tests/test_llm_wiki_bounded_model.py`. Report only bounded coverage. For TLC, check `java -version` and the pinned jar and report UNTESTED if not available.
+
+## Drive
+
+```sh
+python3 scripts/verify_llm_wiki_model.py
+python3 -m pytest -q tests/test_llm_wiki_bounded_model.py
+# OPTIONAL, only when a known, verified TLC jar is installed:
+# java -cp "$TLC_JAR" tlc2.TLC -config .codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.cfg .codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.tla
+```
+
+## Proof bar
+
+The 39 real-code traces pass; an intentionally overwritten raw source causes `broken_overwrite` to fail a reachable trace; a changing real-code implementation triggers requalification. A missing tool, stale sync commit, unexecuted model, or a mutant that no longer fails is NOT a proof. Any failed actual code invariant is a finding, not something to weaken away.
+
+## Evidence
+
+Capture git commit, coverage bounds, command/output, touched code/functions, actual negative counterexample and model assumptions. Separate `offline` finite trace proof from `formal-TLC` (UNTESTED unless TLC really runs) and from host-live observation. Do not promote a code sync record merely because tests pass on an unchanged model.
+
+## Cleanup
+
+Trace explorer uses unique `TemporaryDirectory` directories and cleans them. Preserve negative control receipts elsewhere. No server, process PID or shared filesystem fixture is owned persistently.
+
+## Helpers
+
+`python3 scripts/verify_llm_wiki_model.py` and `python3 -m pytest -q tests/test_llm_wiki_bounded_model.py`. Use `/maintain-formal-verification-skill` whenever covered code changes without a corresponding recheck.

.codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.cfg

@@ -0,0 +1,8 @@
+CONSTANTS
+  Names = {one, two}
+  Blobs = {A, B}
+  Empty = empty
+SPECIFICATION Spec
+INVARIANTS
+  TypeOK
+  NeverOverwrite

.codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.tla

@@ -0,0 +1,30 @@
+----------------------- MODULE WikiRawImmutability -----------------------
+EXTENDS Naturals, TLC
+CONSTANTS Names, Blobs, Empty
+VARIABLES raw, original
+
+vars == <<raw, original>>
+
+Init ==
+    /\ raw = [n \in Names |-> Empty]
+    /\ original = [n \in Names |-> Empty]
+
+Create(n, b) ==
+    /\ n \in Names
+    /\ b \in Blobs
+    /\ raw[n] = Empty
+    /\ raw' = [raw EXCEPT ![n] = b]
+    /\ original' = [original EXCEPT ![n] = b]
+
+Replay(n, b) ==
+    /\ n \in Names
+    /\ b \in Blobs
+    /\ raw[n] = b
+    /\ UNCHANGED vars
+
+Next == \E n \in Names, b \in Blobs : Create(n, b) \/ Replay(n, b)
+Spec == Init /\ [][Next]_vars
+NeverOverwrite == \A n \in Names : raw[n] = original[n]
+TypeOK == raw \in [Names -> (Blobs \cup {Empty})]
+        /\ original \in [Names -> (Blobs \cup {Empty})]
+=============================================================================

.codex/skills/verify-llm-wiki/SKILL.md

@@ -0,0 +1,48 @@
+---
+name: verify-llm-wiki
+description: "Use when changing the PStack project-local .llm-wiki CLI, raw source capture, Markdown navigation, or source/link integrity verification."
+disable-model-invocation: true
+---
+
+# Verify PStack LLM Wiki CLI
+
+Generated from `skills/create-verification-skill/SKILL.md` and tailored to actual Python CLI entry points. This **host-native Codex skill** is not a portable shared skill or a QStack publisher. Read [the feature map](features/README.md) before a full sweep.
+
+## Launch
+
+No server: the application is a short-lived Python CLI. From the repository root run `bash .codex/skills/verify-llm-wiki/scripts/driver.sh launch`. A usable instance is Python 3 with pytest available, existing `.llm-wiki/config.json` and `scripts/llm_wiki.py`. Scratch drives use pytest `tmp_path` and isolated temporary wiki roots. No shared service, port or provider credentials are required.
+
+## Doctor
+
+`bash .codex/skills/verify-llm-wiki/scripts/driver.sh doctor` checks Python, pytest and the real `scripts/llm_wiki.py check --wiki-dir .llm-wiki`. Doctor is read-only relative to the tracked project wiki, and **cannot** assert typed schema validation, external references, generated-index byte equality, or semantic correctness.
+
+## Drive
+
+`bash .codex/skills/verify-llm-wiki/scripts/driver.sh drive` first runs Doctor, then the actual CLI and pytest contracts in isolated scratch directories: `tests/test_llm_wiki.py`, `tests/test_llm_wiki_safety.py`, `tests/test_llm_wiki_bounded_model.py`, and `scripts/verify_llm_wiki_model.py`. This is a real production-Python-code negative control, not an LLM provider/model or full model-checker execution.
+
+## Proof bar
+
+- Clean tracked wiki passes the structural CLI check; broken/local out-of-root links fail.
+- The first source revision is stored once; conflicting same-basename bytes are refused without altering accepted bytes. Exact replay is idempotent.
+- A symlinked raw directory or capture target cannot redirect the trusted file write in the tested setup.
+- The model verifier exhaustively explores 39 serial traces (length 1–3 over three predefined inputs) through production `ingest_file` and detects a deliberate overwrite mutation.
+- Tests exercise a real CLI nonzero on collision. **No proof** of malicious concurrent directory swaps, all Markdown syntax, arbitrary run-time interleavings, TLA+ results, crash-safe source+log commit, or cross-repository QStack publisher authority.
+- Reduce negative results by FAIL > BLOCKED > UNTESTED > PASS; a skipped optional checker is not a proof.
+
+## Evidence
+
+Record the exact git HEAD, command, Python/pytest version, exit code, 39-trace count, failing-mutant evidence, and affected files. Terminal/CI logs are `offline` evidence. For durable local transcripts, invoke driver with `LLM_WIKI_EVIDENCE_DIR` set to an **owned unique directory**; the driver saves a per-run transcript without overwriting an existing receipt. Never label these results `observed_live` host-native/model execution. Keep stdout/stderr of a broken control as proof, not as a PASS of the broken code.
+
+## Cleanup
+
+No process is launched. Tests use their own pytest scratch roots, and bounded-model checks use `TemporaryDirectory`; both clean their own scratch data. `driver.sh cleanup` prints the owned-resource state and never kills another user's process or deletes durable evidence.
+
+## Helpers
+
+```sh
+bash .codex/skills/verify-llm-wiki/scripts/driver.sh {launch|doctor|drive|cleanup}
+python3 scripts/verify_llm_wiki_model.py
+python3 scripts/scaffold_verification_skill.py --check --target-dir .codex/skills/verify-llm-wiki
+```
+
+The helper uses GNU `timeout` and refuses to run unbounded if it is missing. Every subprocess is bounded to 60 seconds. The companion [formal skill](../verify-llm-wiki-formal/SKILL.md) describes what remains unproved.

.codex/skills/verify-llm-wiki/features/README.md

@@ -0,0 +1,17 @@
+# LLM Wiki verification feature map
+
+## Full sweep
+
+Run all three feature areas in this strict order with `bash .codex/skills/verify-llm-wiki/scripts/driver.sh drive`:
+
+1. [Core CLI and link integrity](core.md)
+2. [Write-once source semantics](source-immutability.md)
+3. [Bounded real-code invariants](bounded-invariants.md)
+
+## Features
+
+1. [Core CLI and link integrity](core.md)
+2. [Write-once source semantics](source-immutability.md)
+3. [Bounded real-code invariants](bounded-invariants.md)
+
+No external provider, scraper or QStack publisher is launched. Offline fixtures are not live-model evidence.

.codex/skills/verify-llm-wiki/features/bounded-invariants.md

@@ -0,0 +1,13 @@
+# Core feature: bounded real-code invariants
+
+## Sub-features
+39 exhaustive ordered input traces through production `ingest_file` and deliberate overwrite-mutant rejection.
+
+## How to get to it (user POV)
+Run `python3 scripts/verify_llm_wiki_model.py` to read PASS/FAIL with the bound and negative control.
+
+## Driving it with Codex
+`python3 -m pytest -q tests/test_llm_wiki_bounded_model.py` checks both real code and mutant.
+
+## Gotchas
+This is bounded serial state-space exploration of real Python, not TLC output, an unbounded theorem, or general concurrent write proof. See `verify-llm-wiki-formal` for the proposed TLA+ model.

.codex/skills/verify-llm-wiki/features/core.md

@@ -0,0 +1,13 @@
+# Core feature: CLI and wiki navigation
+
+## Sub-features
+Structural config, index membership, links, bad CLI input, nested page indexing.
+
+## How to get to it (user POV)
+Run `python3 scripts/llm_wiki.py check --wiki-dir .llm-wiki` and `python3 scripts/llm_wiki.py index --wiki-dir .llm-wiki`.
+
+## Driving it with Codex
+Use `bash .codex/skills/verify-llm-wiki/scripts/driver.sh drive`; pytest creates all negative fixtures under isolated `tmp_path`.
+
+## Gotchas
+A structural pass is not typed schema validation, semantic citation verification, or a promise of Markdown-parser completeness.

.codex/skills/verify-llm-wiki/features/source-immutability.md

@@ -0,0 +1,13 @@
+# Core feature: source-immutability
+
+## Sub-features
+Atomic exclusive create, basename collision refusal, idempotent exact replay, symlink rejection, write-safe read path.
+
+## How to get to it (user POV)
+Run `python3 scripts/llm_wiki.py ingest /tmp/some-file --wiki-dir /tmp/owned-scratch-wiki` with an isolated disposable destination, then repeat with different bytes using the same filename.
+
+## Driving it with Codex
+`python3 -m pytest -q tests/test_llm_wiki_safety.py` operates on scratch wiki copies.
+
+## Gotchas
+The source write and `log.md` append are **not one atomic transaction**; a process crash between them can yield a source without a corresponding log entry. The symlink preflight is not an adversarial OS sandbox or proof against concurrent ancestor replacement.

.codex/skills/verify-llm-wiki/scripts/driver.sh

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+# Codex project-local wiki verifier: bounded, offline, no shared service.
+set -euo pipefail
+ROOT="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../../../.." && pwd)"
+cd "$ROOT"
+export PYTHONPATH="$ROOT${PYTHONPATH:+:$PYTHONPATH}"
+
+if ! command -v timeout >/dev/null 2>&1; then
+  echo "BLOCKED: GNU timeout required for 60s execution bounds" >&2
+  exit 2
+fi
+
+run_bounded() {
+  local label="$1"; shift
+  echo "==> $label"
+  timeout --kill-after=5s 60s "$@" < /dev/null
+}
+
+drive() {
+  doctor
+  run_bounded "original PStack wiki contracts" python3 -m pytest -q tests/test_llm_wiki.py
+  run_bounded "source and path negatives" python3 -m pytest -q tests/test_llm_wiki_safety.py
+  run_bounded "bounded production-code model" python3 -m pytest -q tests/test_llm_wiki_bounded_model.py
+  run_bounded "real-code and mutation trace" python3 scripts/verify_llm_wiki_model.py
+}
+
+doctor() {
+  run_bounded "python" python3 --version
+  run_bounded "pytest" python3 -m pytest --version
+  run_bounded "structural wiki CLI" python3 scripts/llm_wiki.py check --wiki-dir .llm-wiki
+}
+
+if [[ -n "${LLM_WIKI_EVIDENCE_DIR:-}" ]]; then
+  mkdir -p "$LLM_WIKI_EVIDENCE_DIR"
+  receipt="$(mktemp "$LLM_WIKI_EVIDENCE_DIR/verify-llm-wiki.XXXXXXXX.log")"
+  echo "Evidence transcript: $receipt"
+  exec > >(tee -a "$receipt") 2>&1
+  git rev-parse HEAD || true
+fi
+
+case "${1:-doctor}" in
+  launch) run_bounded "python" python3 --version; run_bounded "pytest" python3 -m pytest --version ;;
+  doctor) doctor ;;
+  drive) drive ;;
+  cleanup) echo "No owned persistent processes; scratch roots belong to test fixtures; receipts retained." ;;
+  *) echo "Usage: $0 {launch|doctor|drive|cleanup}" >&2; exit 2 ;;
+esac

.github/workflows/portability-offline.yml

@@ -88,6 +88,13 @@ jobs:
             tests/test_jev_privacy_and_bypass.py \
             tests/test_jev_mapping_and_calibrated_evidence.py \
             tests/test_fast_role_task_fit.py
+      - name: Verify project-local LLM Wiki source safety and bounded model
+        run: |
+          python scripts/scaffold_verification_skill.py --check --target-dir .codex/skills/verify-llm-wiki
+          bash .codex/skills/verify-llm-wiki/scripts/driver.sh launch
+          bash .codex/skills/verify-llm-wiki/scripts/driver.sh drive
+        # Bounded actual-code and negative mutation checks only.
+        # TLC, upstream SDK/binary, models and host-native live runs remain UNTESTED.
       - name: Verify maintained JEV skill doctor on exact PR head
         run: |
           bash .codex/skills/verify-decision-contract/scripts/driver.sh launch

.llm-wiki/WIKI_SCHEMA.md

@@ -1,10 +1,28 @@
-# LLM Wiki Schema
+# PStack Project-Local LLM Wiki Schema and Ownership
 
-## Ownership Rules
+This is a **structural Markdown/Git schema**, not a JSON-Schema-validated ontology or semantic proof. The baseline does not require Node, Rust, embeddings, an LLM provider or a wiki daemon. Normative cross-repository QStack policies live in QStack, not in this file.
 
-| Path | Owner | Rule |
-|------|-------|------|
-| raw/** | extension | immutable after capture |
-| wiki/** | model + user | editable knowledge pages |
-| meta/* | extension | auto-generated |
-| . | human + explicit request | operating rules |
+## Ownership and data-flow rules
+
+| Path | Owner | Contract |
+|---|---|---|
+| `raw/sources/**` | explicit capture/maintainer | Write-once **through `scripts/llm_wiki.py ingest`**; basename collision with different bytes fails, identical replay is a no-op |
+| `wiki/{sources,entities,concepts,requirements,analyses,syntheses}/**` | model + authorized engineer | Curated Markdown; all pages should be linked from the derived navigation index |
+| `index.md` | CLI projection | Generated navigation; `index --write` uses an atomic replacement |
+| `log.md` | CLI and maintainer | Human-readable operation history; **not a transactionally authoritative event store** |
+| `config.json` | maintainer | `name`, `mode`, `topic`, `version` must be nonempty strings |
+| `WIKI_SCHEMA.md` | maintainer | Declares structural storage and ownership policy |
+
+## Structural contract vs unproved properties
+
+`scripts/llm_wiki.py check` checks required paths, config key shape, indexed Markdown pages and reachable local links. It rejects wiki page or link destinations resolving outside the local wiki root, and rejects symlinked mandatory directories. Its Markdown link detector is deliberately limited: it does **not** fully parse all Markdown variants, anchors, remote citations, frontmatter types, typed relations, semantic accuracy, or reproducible compiler outputs.
+
+The ingestion CLI uses atomic **exclusive file creation** to prevent sequential overwrite and straightforward same-name races. It rejects symlinked raw and log directories in the tested case, but a preflight is not an OS sandbox against adversarial concurrent directory replacement. Source copy and activity-log append remain **separate writes**, so a crash can leave incomplete history. Repository write permissions, Git review, and negative controls remain necessary.
+
+## Reference and migration boundaries
+
+`docs/research/llm-wiki-reference-evaluation-2026-10-31.md` defines a source-pinned comparison of Atomicstrata and Geronimo, optional adapter candidates, rollback, and the nine QStack semantic roles. PStack's wiki is **not** QStack's canonical `knowledge/` publisher or `knowledge/operations.jsonl` ledger. No external engine may bypass QStack's independent governance.
+
+## Verification
+
+Use `.codex/skills/verify-llm-wiki/` for actual Python CLI/scratch-path checks and `.codex/skills/verify-llm-wiki-formal/` for the bounded 39-trace real-code model and optional (unexecuted unless evidence is recorded) TLC specification. None of these offline checks establish native six-host execution or live LLM compilation. See [issue #874](https://github.com/tommy-ca/pstack/issues/874).