[LLM-Wiki-v2][F1] Build real and formal wiki verification skills; close safety and schema gaps #874

Logical parent: #871. Depends on: #873 (plain issue links; no native GitHub subissue claim).

Scope and acceptance

Apply canonical skills/create-verification-skill/SKILL.md to generate a host-native project-local verify-llm-wiki CLI drive with Launch/Doctor/Drive/Evidence/Cleanup/Helpers and deterministic isolated scratch instances. Apply skills/create-formal-verification-skill/SKILL.md to model source immutability, page promotion/admission, and concurrent writer/linearizable update properties; pin code spans and sync SHA. Check a deliberate broken variant causes failure (negative control). Add Python tests for no overwrite, basename collision, symlink/path confinement, invalid page type/frontmatter, unindexed/deeply nested page, link resolution, conflicting concurrent ingests, torn log/index, stale digest and CLI exit codes. Repair defects only when independently verified. Formal TLC/SMT unavailable => BLOCKED, not proof. Keep functional vs formal verdicts distinct.

Evidence policy

Acceptance requires a reviewable PR and exact-head reproducible receipts. Planning is not implementation; no claimed Swarm/Arena/Interrogate model execution without actual independent work.

Partial implementation and exact-head evidence (2026-10-31)

• Stacked draft PR #879 on docs(wiki): audit reference engines and propose governed migration (#871) #878 adds scripts/llm_wiki.py raw write-once/exclusive creation, link confinement and atomic index replacement, 11 new negative safety tests, 39-history bounded real-code checker + failing overwrite mutant, native Codex verify-llm-wiki and verify-llm-wiki-formal skills, optional NOT_EXECUTED TLA+ model, and offline CI wiring.
• Earlier implementation head 674b2bfb354f71e8674c4cf5fa33e10dd9868262: Actions 41214985678 SUCCESS. Inspected job log: original wiki tests 9 passed, new safety negatives 11 passed, bounded model tests 3 passed; standalone model reports 39 bounded actual-code traces PASS and deliberate conflicting overwrite mutant detected at two-step trace A→B. Skill scaffold check PASS. This is offline functional evidence only.
• Current successor head 0029b35fad97aa19fd67c42f35bd0ff3ec6f15ce includes schema/wiki documentation changes; Actions 41215096803 was IN_PROGRESS at this inspection. Do not treat prior-head CI as exact-head proof of later changes.
• Remaining OPEN: actual TLC execution/negative TLA check, independent Swarm/Arena/Interrogate and Thermos reviews, crash-safe source+human-log transaction, adversarial directory-swap confinement (beyond simple preflight), independent source/rights review, multi-host observed-live coverage. Source+log writes are not atomic and not claimed as such. This child remains OPEN until acceptance gates are met.