From bed363e12c5bb31459b263b4d6d9da409a15db80 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:20:41 +0100
Subject: [PATCH 01/17] fix(wiki): write-once raw ingestion, confine links and
 atomically replace index (#874)

---
 scripts/llm_wiki.py | 71 ++++++++++++++++++++++++++++++++++++---------
 1 file changed, 57 insertions(+), 14 deletions(-)

diff --git a/scripts/llm_wiki.py b/scripts/llm_wiki.py
index 3606b260..fd0427ae 100755
--- a/scripts/llm_wiki.py
+++ b/scripts/llm_wiki.py
@@ -18,9 +18,11 @@
 import datetime
 import hashlib
 import json
+import os
 import re
 from pathlib import Path
 import sys
+import tempfile
 
 DEFAULT_WIKI_DIR = Path(__file__).resolve().parents[1] / ".llm-wiki"
 
@@ -46,6 +48,8 @@ def check_wiki(wiki_dir: Path) -> list[str]:
     errors: list[str] = []
     if not wiki_dir.is_dir():
         return [f"Wiki root directory not found: {wiki_dir}"]
+    wiki_root = wiki_dir.resolve()
+    pages_root = (wiki_dir / "wiki").resolve()
 
     # 1. Required files
     for fname in REQUIRED_TOP_LEVEL_FILES:
@@ -58,6 +62,8 @@ def check_wiki(wiki_dir: Path) -> list[str]:
         target = wiki_dir / dname
         if not target.is_dir():
             errors.append(f"Missing required directory: {dname}")
+        if target.is_symlink():
+            errors.append(f"Symlink directory forbidden in wiki: {dname}")
 
     # 3. Config JSON validation
     config_file = wiki_dir / "config.json"
@@ -67,6 +73,8 @@ def check_wiki(wiki_dir: Path) -> list[str]:
             for req_key in ("name", "mode", "topic", "version"):
                 if req_key not in cfg:
                     errors.append(f"config.json missing required key '{req_key}'")
+                elif not isinstance(cfg[req_key], str) or not cfg[req_key].strip():
+                    errors.append(f"config.json key '{req_key}' must be a nonempty string")
         except Exception as e:
             errors.append(f"config.json is invalid JSON: {e}")
 
@@ -79,9 +87,12 @@ def check_wiki(wiki_dir: Path) -> list[str]:
         for link_match in re.finditer(r"\[([^\]]+)\]\(([^)]+)\)", text):
             target_rel = link_match.group(2).strip()
             # Ignore external or absolute links
-            if target_rel.startswith(("http://", "https://", "#")):
+            if target_rel.startswith(("http://", "https://", "#", "mailto:")):
+                continue
+            resolved = (wiki_dir / target_rel.split("#", 1)[0]).resolve()
+            if not resolved.is_relative_to(pages_root):
+                errors.append(f"index.md contains out-of-root link: {target_rel}")
                 continue
-            resolved = (wiki_dir / target_rel).resolve()
             if not resolved.is_file():
                 errors.append(f"index.md contains broken link: {target_rel} (resolved to {resolved})")
             else:
@@ -91,6 +102,9 @@ def check_wiki(wiki_dir: Path) -> list[str]:
     wiki_content_dir = wiki_dir / "wiki"
     if wiki_content_dir.is_dir():
         for page in wiki_content_dir.rglob("*.md"):
+            if page.is_symlink() or not page.resolve().is_relative_to(pages_root):
+                errors.append(f"Wiki page escapes content root: {page}")
+                continue
             if page.resolve() not in indexed_targets:
                 rel_path = page.relative_to(wiki_dir)
                 errors.append(f"Wiki page not listed in index.md: {rel_path}")
@@ -106,6 +120,9 @@ def check_wiki(wiki_dir: Path) -> list[str]:
                 if not file_target:
                     continue
                 link_resolved = (page.parent / file_target).resolve()
+                if not link_resolved.is_relative_to(wiki_root):
+                    errors.append(f"Page {page.name} contains out-of-root link to: {link_target}")
+                    continue
                 if not link_resolved.exists():
                     errors.append(
                         f"Page {page.name} contains broken relative link to: {link_target}"
@@ -132,7 +149,7 @@ def generate_index_markdown(wiki_dir: Path) -> str:
         cat_dir = wiki_content_dir / category
         if not cat_dir.is_dir():
             continue
-        pages = sorted(cat_dir.glob("*.md"))
+        pages = sorted(cat_dir.rglob("*.md"))
         if not pages:
             continue
         lines.append(f"## {category.capitalize()}")
@@ -161,27 +178,43 @@ def ingest_file(source: Path, wiki_dir: Path, label: str | None = None) -> tuple
     if not source.is_file():
         raise FileNotFoundError(f"Source file not found: {source}")
 
-    raw_sources_dir = wiki_dir / "raw" / "sources"
+    # A source revision is write-once. Reject known symlink aliases before writes;
+    # this check is not an OS sandbox against hostile concurrent directory swaps.
+    wiki_dir = wiki_dir.resolve()
+    raw_dir = wiki_dir / "raw"
+    raw_sources_dir = raw_dir / "sources"
+    for directory in (raw_dir, raw_sources_dir):
+        if directory.is_symlink():
+            raise ValueError(f"Symlink wiki source directory forbidden: {directory}")
     raw_sources_dir.mkdir(parents=True, exist_ok=True)
+    log_file = wiki_dir / "log.md"
+    if log_file.is_symlink():
+        raise ValueError(f"Symlink wiki log forbidden: {log_file}")
 
     dest = raw_sources_dir / source.name
     content = source.read_bytes()
-    dest.write_bytes(content)
-
     digest = hashlib.sha256(content).hexdigest()
+    try:
+        # Exclusive create is atomic on the destination filesystem; no overwrite.
+        with dest.open("xb") as handle:
+            handle.write(content)
+    except FileExistsError:
+        if dest.is_symlink() or not dest.is_file() or dest.read_bytes() != content:
+            raise FileExistsError(f"Immutable raw source collision: {dest}") from None
+        # Exact replays have no additional log event (idempotent ingest).
+        return dest, digest
     now_str = datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%d %H:%M UTC")
 
-    log_file = wiki_dir / "log.md"
     log_entry = (
         f"- **{now_str}**: Ingested `{source.name}` (SHA256: `{digest[:12]}...`)"
         + (f" - {label}" if label else "")
         + "\n"
     )
-    if log_file.is_file():
-        existing = log_file.read_text(encoding="utf-8")
-        log_file.write_text(existing + log_entry, encoding="utf-8")
-    else:
-        log_file.write_text(f"# Wiki Activity Log\n\n{log_entry}", encoding="utf-8")
+    # A failed append can leave an unlogged source; reconcile with a later audit.
+    # This is intentionally not represented as an atomic source+ledger transaction.
+    prefix = "" if log_file.is_file() else "# Wiki Activity Log\n\n"
+    with log_file.open("a", encoding="utf-8") as handle:
+        handle.write(prefix + log_entry)
 
     return dest, digest
 
@@ -205,7 +238,7 @@ def main(argv: list[str] | None = None) -> int:
     subparsers.add_parser(
         "check",
         parents=[parent_parser],
-        help="Verify wiki structure, schema, and link integrity.",
+        help="Verify wiki structure, config shape, and local links (not semantic schema).", 
     )
 
     # index
@@ -242,7 +275,17 @@ def main(argv: list[str] | None = None) -> int:
         generated = generate_index_markdown(wiki_dir)
         if args.write:
             index_path = wiki_dir / "index.md"
-            index_path.write_text(generated, encoding="utf-8")
+            # Atomic replace avoids exposing a partially-written navigation index.
+            with tempfile.NamedTemporaryFile(
+                mode="w", encoding="utf-8", dir=wiki_dir,
+                prefix=".index-", suffix=".tmp", delete=False,
+            ) as handle:
+                handle.write(generated)
+                temporary = Path(handle.name)
+            try:
+                os.replace(temporary, index_path)
+            finally:
+                temporary.unlink(missing_ok=True)
             print(f"Wrote generated index to {index_path}")
             return 0
         else:

From f39d5bc26d1f519a8eefe1eac1ec4accd197a01f Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:22:03 +0100
Subject: [PATCH 02/17] test(wiki): negative controls for immutable source
 capture and local path boundaries (#874)

---
 tests/test_llm_wiki_safety.py | 155 ++++++++++++++++++++++++++++++++++
 1 file changed, 155 insertions(+)
 create mode 100644 tests/test_llm_wiki_safety.py

diff --git a/tests/test_llm_wiki_safety.py b/tests/test_llm_wiki_safety.py
new file mode 100644
index 00000000..7eb9770d
--- /dev/null
+++ b/tests/test_llm_wiki_safety.py
@@ -0,0 +1,155 @@
+"""Security and replay contract tests for the PStack project-local wiki.
+
+The baseline is intentionally structural; these tests do not prove semantic
+extraction, arbitrary Markdown parsing, or a cross-file transaction.
+"""
+
+from __future__ import annotations
+
+from concurrent.futures import ThreadPoolExecutor
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+
+import pytest
+
+ROOT = Path(__file__).resolve().parents[1]
+if str(ROOT) not in sys.path:
+    sys.path.insert(0, str(ROOT))
+from scripts.llm_wiki import check_wiki, generate_index_markdown, ingest_file
+
+BASE_WIKI = ROOT / ".llm-wiki"
+
+
+@pytest.fixture
+def wiki(tmp_path: Path) -> Path:
+    dest = tmp_path / ".llm-wiki"
+    shutil.copytree(BASE_WIKI, dest)
+    return dest
+
+
+def _source(folder: Path, text: str) -> Path:
+    folder.mkdir(parents=True, exist_ok=True)
+    file = folder / "spec.md"
+    file.write_text(text, encoding="utf-8")
+    return file
+
+
+def test_immutable_raw_basename_conflict_is_rejected(wiki: Path, tmp_path: Path) -> None:
+    first = _source(tmp_path / "first", "one")
+    second = _source(tmp_path / "second", "two")
+    dest, _ = ingest_file(first, wiki)
+    log_before = (wiki / "log.md").read_bytes()
+    with pytest.raises(FileExistsError, match="Immutable raw source collision"):
+        ingest_file(second, wiki)
+    assert dest.read_bytes() == b"one"
+    assert (wiki / "log.md").read_bytes() == log_before
+
+
+def test_exact_replay_does_not_duplicate_log(wiki: Path, tmp_path: Path) -> None:
+    source = _source(tmp_path / "in", "identical")
+    first = ingest_file(source, wiki)
+    previous = (wiki / "log.md").read_bytes()
+    second = ingest_file(source, wiki)
+    assert first == second
+    assert (wiki / "log.md").read_bytes() == previous
+
+
+def test_concurrent_conflicting_ingest_has_single_winner(wiki: Path, tmp_path: Path) -> None:
+    first = _source(tmp_path / "first", "A")
+    second = _source(tmp_path / "second", "B")
+    with ThreadPoolExecutor(max_workers=2) as pool:
+        runs = list(pool.map(lambda p: _capture_ingest(p, wiki), (first, second)))
+    assert sorted(runs) == ["collision", "success"]
+    assert (wiki / "raw/sources/spec.md").read_text() in {"A", "B"}
+
+
+def _capture_ingest(source: Path, wiki: Path) -> str:
+    try:
+        ingest_file(source, wiki)
+        return "success"
+    except FileExistsError:
+        return "collision"
+
+
+def _make_symlink(link: Path, target: Path, is_dir: bool = False) -> None:
+    try:
+        link.symlink_to(target, target_is_directory=is_dir)
+    except (OSError, NotImplementedError) as exc:
+        pytest.skip(f"Symlinks unavailable: {exc}")
+
+
+def test_symlink_raw_source_directory_is_rejected(wiki: Path, tmp_path: Path) -> None:
+    source = _source(tmp_path / "in", "safe")
+    outside = tmp_path / "outside"
+    outside.mkdir()
+    sources = wiki / "raw/sources"
+    shutil.rmtree(sources)
+    _make_symlink(sources, outside, is_dir=True)
+    with pytest.raises(ValueError, match="Symlink wiki source directory"):
+        ingest_file(source, wiki)
+    assert not list(outside.iterdir())
+
+
+def test_symlink_raw_target_cannot_be_overwritten(wiki: Path, tmp_path: Path) -> None:
+    source = _source(tmp_path / "in", "safe")
+    outside = tmp_path / "outside.md"
+    outside.write_text("secret")
+    _make_symlink(wiki / "raw/sources/spec.md", outside)
+    with pytest.raises(FileExistsError, match="Immutable raw source collision"):
+        ingest_file(source, wiki)
+    assert outside.read_text() == "secret"
+
+
+def test_symlink_log_refuses_write_before_creating_raw(wiki: Path, tmp_path: Path) -> None:
+    source = _source(tmp_path / "in", "safe")
+    outside = tmp_path / "outside.md"
+    outside.write_text("unchanged")
+    (wiki / "log.md").unlink()
+    _make_symlink(wiki / "log.md", outside)
+    with pytest.raises(ValueError, match="Symlink wiki log"):
+        ingest_file(source, wiki)
+    assert outside.read_text() == "unchanged"
+    assert not (wiki / "raw/sources/spec.md").exists()
+
+
+def test_index_escape_is_rejected(wiki: Path, tmp_path: Path) -> None:
+    (tmp_path / "outside.md").write_text("outside")
+    idx = wiki / "index.md"
+    idx.write_text(idx.read_text() + "\n- [Escape](../outside.md)\n")
+    assert any("out-of-root link" in e for e in check_wiki(wiki))
+
+
+def test_page_escape_is_rejected(wiki: Path) -> None:
+    page = wiki / "wiki/concepts/agentic-orchestrate.md"
+    page.write_text(page.read_text() + "\n[Escape](../../../../outside.md)\n")
+    assert any("out-of-root link" in e for e in check_wiki(wiki))
+
+
+def test_nested_pages_are_included_by_index_generator(wiki: Path) -> None:
+    page = wiki / "wiki/concepts/nested/detail.md"
+    page.parent.mkdir()
+    page.write_text("# Nested Detail\nBounded test fixture.\n")
+    generated = generate_index_markdown(wiki)
+    assert "(wiki/concepts/nested/detail.md)" in generated
+
+
+def test_config_required_value_is_nonempty_string(wiki: Path) -> None:
+    cfg = wiki / "config.json"
+    import json
+    content = json.loads(cfg.read_text())
+    content["mode"] = []
+    cfg.write_text(json.dumps(content))
+    assert any("must be a nonempty string" in e for e in check_wiki(wiki))
+
+
+def test_cli_conflicting_ingest_returns_nonzero(wiki: Path, tmp_path: Path) -> None:
+    first = _source(tmp_path / "first", "one")
+    second = _source(tmp_path / "second", "two")
+    command = [sys.executable, str(ROOT / "scripts/llm_wiki.py"), "ingest"]
+    ok = subprocess.run(command + [str(first), "--wiki-dir", str(wiki)], capture_output=True, text=True, check=False)
+    bad = subprocess.run(command + [str(second), "--wiki-dir", str(wiki)], capture_output=True, text=True, check=False)
+    assert ok.returncode == 0
+    assert bad.returncode != 0
+    assert "Immutable raw source collision" in bad.stderr

From 291917a683721999cf502f58e0abfcb0fff9085a Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:22:45 +0100
Subject: [PATCH 03/17] verify(wiki): bounded actual-code state exploration and
 optional TLC model (#874)

---
 scripts/verify_llm_wiki_model.py | 87 ++++++++++++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 scripts/verify_llm_wiki_model.py

diff --git a/scripts/verify_llm_wiki_model.py b/scripts/verify_llm_wiki_model.py
new file mode 100644
index 00000000..c4ecfcb7
--- /dev/null
+++ b/scripts/verify_llm_wiki_model.py
@@ -0,0 +1,87 @@
+#!/usr/bin/env python3
+"""Bounded exhaustive real-code state-machine check for wiki source immutability.
+
+39 ordered traces (3 distinct inputs, lengths 1-3); actual ingest_file calls
+are exercised. NOT proof of unbounded concurrency or crash consistency.
+A broken overwrite mutant must be detected as a negative control.
+"""
+from __future__ import annotations
+
+from itertools import product
+from pathlib import Path
+import sys
+from tempfile import TemporaryDirectory
+
+ROOT = Path(__file__).resolve().parents[1]
+if str(ROOT) not in sys.path:
+    sys.path.insert(0, str(ROOT))
+from scripts.llm_wiki import ingest_file
+
+EVENTS = (("first", "shared.md", b"A"), ("second", "shared.md", b"B"), ("third", "other.md", b"C"))
+
+
+def broken_overwrite(source: Path, wiki: Path) -> tuple[Path, str]:
+    """Deliberately incorrect implementation, never used in production."""
+    try:
+        return ingest_file(source, wiki)
+    except FileExistsError:
+        target = wiki / "raw" / "sources" / source.name
+        target.write_bytes(source.read_bytes())  # mutation under test
+        return target, "mutant"
+
+
+def explore(ingester) -> int:
+    examined = 0
+    for length in (1, 2, 3):
+        for trace in product(EVENTS, repeat=length):
+            examined += 1
+            with TemporaryDirectory(prefix="wiki-bound-") as temporary:
+                root = Path(temporary)
+                wiki = root / ".llm-wiki"
+                (wiki / "raw" / "sources").mkdir(parents=True)
+                (wiki / "log.md").write_text("# Log\n", encoding="utf-8")
+                accepted: dict[str, bytes] = {}
+                for index, (identity, name, content) in enumerate(trace):
+                    source_dir = root / identity
+                    source_dir.mkdir(exist_ok=True)
+                    source = source_dir / name
+                    source.write_bytes(content)
+                    old = accepted.get(name)
+                    rejected = False
+                    try:
+                        ingester(source, wiki)
+                    except FileExistsError:
+                        rejected = True
+                    if old is None:
+                        if rejected:
+                            raise AssertionError(f"Unexpected first-write rejection at {trace!r}")
+                        accepted[name] = content
+                    elif content != old and not rejected:
+                        raise AssertionError(f"Conflicting source was accepted at step {index}: {trace!r}")
+                    elif content == old and rejected:
+                        raise AssertionError(f"Exact replay was rejected at step {index}: {trace!r}")
+                    for stored_name, expected in accepted.items():
+                        observed = (wiki / "raw" / "sources" / stored_name).read_bytes()
+                        if observed != expected:
+                            raise AssertionError(f"Immutable bytes changed for {stored_name}: {trace!r}")
+    return examined
+
+
+def main() -> int:
+    try:
+        count = explore(ingest_file)
+        print(f"PASS: {count} bounded real-code traces, source immutability + idempotent replay")
+    except Exception as exc:
+        print(f"FAIL: real-code model check: {exc}", file=sys.stderr)
+        return 1
+    try:
+        explore(broken_overwrite)
+    except AssertionError as exc:
+        print(f"PASS: deliberate overwrite mutant detected: {exc}")
+        return 0
+    print("FAIL: overwrite mutant escaped the model checker", file=sys.stderr)
+    return 1
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

From 707b20d49b91dc74a42c382dc69f040300eb26f4 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:23:19 +0100
Subject: [PATCH 04/17] verify(wiki): bounded actual-code state exploration and
 optional TLC model (#874)

---
 tests/test_llm_wiki_bounded_model.py | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 tests/test_llm_wiki_bounded_model.py

diff --git a/tests/test_llm_wiki_bounded_model.py b/tests/test_llm_wiki_bounded_model.py
new file mode 100644
index 00000000..6c37d3bc
--- /dev/null
+++ b/tests/test_llm_wiki_bounded_model.py
@@ -0,0 +1,26 @@
+"""Evidence that bounded source-mutation verification checks production ingest."""
+from __future__ import annotations
+
+import sys
+from pathlib import Path
+import pytest
+
+ROOT = Path(__file__).resolve().parents[1]
+if str(ROOT) not in sys.path:
+    sys.path.insert(0, str(ROOT))
+
+from scripts.llm_wiki import ingest_file
+from scripts.verify_llm_wiki_model import broken_overwrite, explore, main
+
+
+def test_bounded_actual_code_traces() -> None:
+    assert explore(ingest_file) == 39
+
+
+def test_bounded_negative_mutant_is_caught() -> None:
+    with pytest.raises(AssertionError, match="Conflicting source was accepted"):
+        explore(broken_overwrite)
+
+
+def test_standalone_model_verifier_exit_status() -> None:
+    assert main() == 0

From 46c2c90aa0a31ef57b8d0f0c50a0f3df9401da96 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:23:22 +0100
Subject: [PATCH 05/17] verify(wiki): bounded actual-code state exploration and
 optional TLC model (#874)

---
 .../model/WikiRawImmutability.tla             | 30 +++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.tla

diff --git a/.codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.tla b/.codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.tla
new file mode 100644
index 00000000..6f2fa639
--- /dev/null
+++ b/.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})]
+=============================================================================

From 03cadbd01d1489c0920ca80d6391f75382386f24 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:23:24 +0100
Subject: [PATCH 06/17] verify(wiki): bounded actual-code state exploration and
 optional TLC model (#874)

---
 .../verify-llm-wiki-formal/model/WikiRawImmutability.cfg  | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.cfg

diff --git a/.codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.cfg b/.codex/skills/verify-llm-wiki-formal/model/WikiRawImmutability.cfg
new file mode 100644
index 00000000..27288e30
--- /dev/null
+++ b/.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

From 2fc2c16e2fa8bc95f2bafd3d4e1c6d5bc085dbab Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:05 +0100
Subject: [PATCH 07/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .codex/skills/verify-llm-wiki/SKILL.md | 48 ++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki/SKILL.md

diff --git a/.codex/skills/verify-llm-wiki/SKILL.md b/.codex/skills/verify-llm-wiki/SKILL.md
new file mode 100644
index 00000000..db3fc2d9
--- /dev/null
+++ b/.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.

From dac5e86435c7754a1ff68b2f5b2400e2ccf5cd7c Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:07 +0100
Subject: [PATCH 08/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .codex/skills/verify-llm-wiki/features/README.md | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki/features/README.md

diff --git a/.codex/skills/verify-llm-wiki/features/README.md b/.codex/skills/verify-llm-wiki/features/README.md
new file mode 100644
index 00000000..33e13604
--- /dev/null
+++ b/.codex/skills/verify-llm-wiki/features/README.md
@@ -0,0 +1,9 @@
+# LLM Wiki verification feature map
+
+Run in this 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)
+
+No external provider, scraper or QStack governed publisher is launched. Offline fixtures are not live-model evidence.

From 167b047ba185ea4a2b41244261e2a3fd72577725 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:10 +0100
Subject: [PATCH 09/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .codex/skills/verify-llm-wiki/features/core.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki/features/core.md

diff --git a/.codex/skills/verify-llm-wiki/features/core.md b/.codex/skills/verify-llm-wiki/features/core.md
new file mode 100644
index 00000000..1616195f
--- /dev/null
+++ b/.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.

From 9d0441934eba57801b25cdee74d4e29b1407ce88 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:26 +0100
Subject: [PATCH 10/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .../verify-llm-wiki/features/source-immutability.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki/features/source-immutability.md

diff --git a/.codex/skills/verify-llm-wiki/features/source-immutability.md b/.codex/skills/verify-llm-wiki/features/source-immutability.md
new file mode 100644
index 00000000..7c0a7da2
--- /dev/null
+++ b/.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.

From 8dfcbce5a7b54e470bcccc0f5131f780131a26da Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:29 +0100
Subject: [PATCH 11/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .../verify-llm-wiki/features/bounded-invariants.md  | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki/features/bounded-invariants.md

diff --git a/.codex/skills/verify-llm-wiki/features/bounded-invariants.md b/.codex/skills/verify-llm-wiki/features/bounded-invariants.md
new file mode 100644
index 00000000..f0f41fda
--- /dev/null
+++ b/.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.

From 23a52e42cc545623813f89847ab285a18ab0ebe1 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:31 +0100
Subject: [PATCH 12/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .../skills/verify-llm-wiki/scripts/driver.sh  | 47 +++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki/scripts/driver.sh

diff --git a/.codex/skills/verify-llm-wiki/scripts/driver.sh b/.codex/skills/verify-llm-wiki/scripts/driver.sh
new file mode 100644
index 00000000..a87433e9
--- /dev/null
+++ b/.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

From d75e1ebf8a0b9887ec2eeaa230a82cd2e371d69b Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:25:34 +0100
Subject: [PATCH 13/17] skills(wiki): host-native functional and bounded formal
 verification skills (#874)

---
 .codex/skills/verify-llm-wiki-formal/SKILL.md | 56 +++++++++++++++++++
 1 file changed, 56 insertions(+)
 create mode 100644 .codex/skills/verify-llm-wiki-formal/SKILL.md

diff --git a/.codex/skills/verify-llm-wiki-formal/SKILL.md b/.codex/skills/verify-llm-wiki-formal/SKILL.md
new file mode 100644
index 00000000..cd58d307
--- /dev/null
+++ b/.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.

From e21eb9040de0fa42505c19600a41dd09e75548fe Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:27:27 +0100
Subject: [PATCH 14/17] fix(wiki-skill): conform ordered feature-map scaffold
 contract (#874)

---
 .codex/skills/verify-llm-wiki/features/README.md | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/.codex/skills/verify-llm-wiki/features/README.md b/.codex/skills/verify-llm-wiki/features/README.md
index 33e13604..f7660b6f 100644
--- a/.codex/skills/verify-llm-wiki/features/README.md
+++ b/.codex/skills/verify-llm-wiki/features/README.md
@@ -1,9 +1,17 @@
 # LLM Wiki verification feature map
 
-Run in this order with `bash .codex/skills/verify-llm-wiki/scripts/driver.sh drive`:
+## 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 governed publisher is launched. Offline fixtures are not live-model evidence.
+No external provider, scraper or QStack publisher is launched. Offline fixtures are not live-model evidence.

From 674b2bfb354f71e8674c4cf5fa33e10dd9868262 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:27:41 +0100
Subject: [PATCH 15/17] ci(wiki): execute real CLI skill and bounded mutation
 controls offline (#874)

---
 .github/workflows/portability-offline.yml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/portability-offline.yml b/.github/workflows/portability-offline.yml
index 9d3eb343..1e6aaa19 100644
--- a/.github/workflows/portability-offline.yml
+++ b/.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

From 00314088a6c1e00bdc14528595afd96285613a98 Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:29:29 +0100
Subject: [PATCH 16/17] docs(wiki): align project knowledge and ownership
 schema with real verification (#874)

---
 .llm-wiki/WIKI_SCHEMA.md | 34 ++++++++++++++++++++++++++--------
 1 file changed, 26 insertions(+), 8 deletions(-)

diff --git a/.llm-wiki/WIKI_SCHEMA.md b/.llm-wiki/WIKI_SCHEMA.md
index 776eb1c3..123d9982 100644
--- a/.llm-wiki/WIKI_SCHEMA.md
+++ b/.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 |
\ No newline at end of file
+## 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).

From 0029b35fad97aa19fd67c42f35bd0ff3ec6f15ce Mon Sep 17 00:00:00 2001
From: tommy-ca <140900186+tommy-ca@users.noreply.github.com>
Date: Sat, 31 Oct 2026 16:29:32 +0100
Subject: [PATCH 17/17] docs(wiki): align project knowledge and ownership
 schema with real verification (#874)

---
 .../concepts/llm-wiki-project-knowledge.md    | 26 +++++++++++++------
 1 file changed, 18 insertions(+), 8 deletions(-)

diff --git a/.llm-wiki/wiki/concepts/llm-wiki-project-knowledge.md b/.llm-wiki/wiki/concepts/llm-wiki-project-knowledge.md
index 9716693c..950bf10c 100644
--- a/.llm-wiki/wiki/concepts/llm-wiki-project-knowledge.md
+++ b/.llm-wiki/wiki/concepts/llm-wiki-project-knowledge.md
@@ -1,12 +1,22 @@
 # Project-Local LLM Wiki Knowledge System
 
-The project-local LLM Wiki (`.llm-wiki/`) provides a structured, git-tracked knowledge base for PStack engineering.
+PStack's `.llm-wiki/` is a Markdown-first, Git-reviewed knowledge store used by engineering agents and human maintainers. It is not a mandatory semantic compiler or QStack's governed knowledge publisher.
 
-## Purpose and Schema
-- **Layer 1 (`raw/sources/`)**: Immutable snapshots of authoritative specifications, audit manifests, and package descriptors.
-- **Layer 2 (`wiki/`)**: Curated markdown pages covering entities, concepts, requirements, analyses, sources, and syntheses.
-- **Layer 3 (`index.md`, `log.md`, `config.json`)**: Deterministic entrypoint catalog and append-only audit trail.
+## Purpose and storage
 
-## Tooling
-- CLI manager at `scripts/llm_wiki.py` provides `check`, `index`, and `ingest` commands.
-- Automated tests in `tests/test_llm_wiki.py` enforce link integrity, JSON schema validity, and unindexed page detection.
+- **Layer 1 (`raw/sources/`)**: explicit captured source bytes. The PStack Python ingestion CLI creates files exclusively and refuses same-basename changes; direct filesystem changes are not prevented by this tool.
+- **Layer 2 (`wiki/`)**: curated sources, entities, concepts, requirements, analyses and syntheses.
+- **Layer 3 (`index.md`, `log.md`, `config.json`)**: generated navigation, human activity notes and structural configuration. `log.md` is **not** an atomic event ledger.
+
+## Tooling and verification
+
+- `scripts/llm_wiki.py` supports `check`, `index`, `ingest` with Python standard-library dependencies.
+- `tests/test_llm_wiki.py` checks the structural baseline; `tests/test_llm_wiki_safety.py` tests write-once replay, collisions and path/link negatives.
+- `scripts/verify_llm_wiki_model.py` explores 39 bounded serial actual-code ingest traces and verifies that a deliberately broken overwrite variant is detected. It does not prove unbounded concurrency, crash atomicity, or TLA+ conformance.
+- Project-local verification skill: `.codex/skills/verify-llm-wiki/SKILL.md`; bounded formal-analysis skill: `.codex/skills/verify-llm-wiki-formal/SKILL.md`. External TLC remains untested unless a pinned run receipt is produced.
+
+## Reference-engine evaluation
+
+The [reference engine evaluation](../analyses/llm-wiki-reference-evaluation.md) compares Atomicstrata LLMWiki (semantic candidate compilation) with Geronimo LLMWiki (headless graph/search). The default remains the lightweight, offline Python wiki until a measured Arena decision authorizes an optional adapter. QStack retains sole authority over its own canonical publisher, operation ledger and knowledge records.
+
+See `.llm-wiki/WIKI_SCHEMA.md` for the exact implementation limits and ownership rules.