docs(cli): map and verify state machines

.agents/skills/verify-collection-admission/SKILL.md

@@ -0,0 +1,26 @@
+---
+name: verify-collection-admission
+description: Verify CLI collection admission across identity, Personal Server approval and foreign-server confirmation. Use for collection readiness or its identity recheck.
+---
+
+# Verify collection admission
+
+Read the [transition map, bounds and scratch controls](../../../verification/collection-admission/README.md).
+The [checker](../../../verification/collection-admission/check.py) pins the
+covered source and replay from main `a55d0a0006da6a743b6452796435afa6ed177dd8`.
+
+Automated collection must refuse another account's server before probing
+credentials. A late approval response must not admit collection for an
+account that changed while preparation was pending.
+
+Use Python 3.12 or newer, installed Node and Vitest, and pinned TLC 1.7.4
+with Java. Set `TLA2TOOLS` and `JAVA` to installed paths. Run from the CLI root.
+
+```sh
+python3 verification/collection-admission/check.py --out "$(mktemp -d)/proof"
+```
+
+Require the current config and offline replay to pass. The named broken
+configurations and their scratch source changes must fail on their intended
+contracts. Read every outcome with Pstack `/statechart`. Reconcile new awaits
+and owner boundaries before advancing the source pins.

.agents/skills/verify-export-settlement/SKILL.md

@@ -0,0 +1,29 @@
+---
+name: verify-export-settlement
+description: Verify queued export owner binding and generation settlement. Use for result publication, pending upload receipts, or retry and sync changes.
+---
+
+# Verify queued export settlement
+
+Read the [transition map, source pins, bounds and replay](../../../verification/export-settlement/README.md).
+This proof was reconciled against CLI main `a55d0a0006da6a743b6452796435afa6ed177dd8`
+and the integrated main snapshot recorded in its checker.
+
+A late upload must leave the current generation's receipt and visible result
+aligned. A foreign collection must preserve pending bytes that belong to
+another owner. The proof checks both with TLC 1.7.4 and the built CLI.
+
+Run from the CLI root with Python 3.12 or newer, the installed package
+dependencies and Java. Set `TLA2TOOLS` and `JAVA` to installed tool paths.
+
+```sh
+python3 verification/export-settlement/check.py
+```
+
+Require both current cases and offline CLI replays to pass. Require each
+broken case and corresponding scratch source mutation to fail on the intended
+contract. Read every TLA+ outcome with Pstack `/statechart`.
+
+When covered source changes, trace publication and settlement at their actual
+lock and commit boundaries. Advance the source pins after the checked model,
+broken controls and restored replays agree.

.agents/skills/verify-hosted-provisioning/SKILL.md

@@ -0,0 +1,28 @@
+---
+name: verify-hosted-provisioning
+description: Verify hosted Personal Server resource ownership across create and delete. Use for Connect's server API, provisioning-row updates, or deprovisioning admission.
+---
+
+# Verify hosted Personal Server provisioning
+
+Read the [transition map, bounds and known finding](../../../verification/hosted-provisioning/README.md).
+The [checker](../../../verification/hosted-provisioning/check.py) pins the reviewed
+route source and requires the model and offline API replay to agree.
+
+An accepted provider resource needs a durable row with the handles required
+for cleanup. A delete during provisioning can race the provider result
+before either handle exists.
+
+Use Python 3.12 or newer, installed Node and CLI and Connect dependencies,
+and pinned TLC 1.7.4 with Java. Set `TLA2TOOLS` and `JAVA` to installed
+paths. Run from the CLI root.
+
+```sh
+python3 verification/hosted-provisioning/check.py
+```
+
+Read the current counterexample and the scratch-guard outcome with Pstack
+`/statechart`. Require the signed route replay to reproduce the current
+finding and the scratch guard to block it. Restore the source and rerun.
+Reconcile the provider boundary, database state, and observed HTTP outcomes
+before moving the source pins.

.agents/skills/verify-mainnet-registration/SKILL.md

@@ -0,0 +1,27 @@
+---
+name: verify-mainnet-registration
+description: Verify mainnet app registration and Account association recovery. Use for the registration journal, gateway confirmation, retry, or ownership check.
+---
+
+# Verify mainnet app registration
+
+Read the [transition map, bounds and replay](../../../verification/mainnet-registration/README.md).
+The [checker](../../../verification/mainnet-registration/check.py) pins the reviewed
+source from CLI main `a55d0a0006da6a743b6452796435afa6ed177dd8`.
+
+Persist the original registration context before the first gateway request.
+Require a matching confirmed app before associating it with Account, and
+confirm Account ownership before clearing the recovery journal.
+
+Use Python 3.12 or newer, installed Node and Vitest, and pinned TLC 1.7.4 with
+Java. Set `TLA2TOOLS` and `JAVA` if mise cannot locate them. Run from the CLI root.
+
+```sh
+python3 verification/mainnet-registration/check.py
+```
+
+Require the current model and real-command replays to pass. The checker must
+observe every named model violation, catch its scratch source mutant, restore
+the source, and pass the baseline again. Read all outcomes with Pstack
+`/statechart`. Update the pinned source only after rechecking the model's
+journal, remote confirmation, and Account ownership boundaries.

.agents/skills/verify-paid-read-recovery/SKILL.md

@@ -0,0 +1,105 @@
+---
+name: verify-paid-read-recovery
+description: Verify interrupted and overlapping CLI paid reads, receipt-file writers and dead-owner recovery. Use when changing src/cli/app/read.ts, src/core/receipts.ts or src/core/receipts-lock.ts. Runs TLA+ models and offline real-code replays without live paid reads.
+---
+
+# Verify paid-read recovery
+
+The promise: an interrupted or overlapping read retains the exact payment
+identity needed to resume, without authorizing another payment for the same read
+intent. A concurrent state update must not erase a saved receipt.
+
+## Source record
+
+Last confirmed source commit: `a55d0a0006da6a743b6452796435afa6ed177dd8`. The runner records the exact source blobs and rejects drift.
+
+| Owner                                                                             | Coverage                                                                                                                                                                                                                               |
+| --------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| `src/cli/app/read.ts`, `runAppRead` and `runPersonalServerRead`                   | Acquire the intent lock before loading saved state; retain it through signing, persistence, transport and error handling. Replay exact headers and refuse rejected-receipt replacement. Contention uses existing `not_ready` / exit 6. |
+| `src/core/receipts.ts`, `withReadLock`, `nextNonce`, `saveReceipt`, `dropReceipt` | Intent exclusion and writer exclusion around the complete file read/modify/write. Preserve temporary-file fsync, rename and directory fsync.                                                                                           |
+| `src/core/receipts-lock.ts`, `acquireReceiptLock`                                 | Atomic publication of an identified owner; retain live/unknown owners, reclaim demonstrably dead ones, and preserve successor locks.                                                                                                   |
+| SDK 4.3.1 direct read/payment helpers                                             | Real fixture signing and request construction. One signed header is reused across transport retries.                                                                                                                                   |
+
+## Run
+
+From the repo root with installed dependencies, Python 3.12+, compatible Node,
+TLC 1.7.4 and Java installed through mise:
+
+```sh
+python3 verification/paid-read-recovery/check.py
+```
+
+The runner exports the recorded fixed commit and overlays only the named
+working-tree source owners and regression tests. Expected blob identities prevent
+silent source/model drift. `--ref` checks a committed revision instead; it still
+must match the checked source blobs. No branch switch or product mutation occurs
+in the working checkout. `TLA2TOOLS` and `JAVA` may select existing local tools;
+the TLC jar hash is pinned and no dependencies are downloaded.
+
+The command runs four fixed models, four negative models, the real-code tests,
+four deliberate source mutations in a disposable copy, then restores all source
+bytes and reruns the baseline. It prints the evidence directory. Exit 0 means all
+expected positive and negative results hold; exit 2 means an execution or proof
+failure. Unexpected external fetches are rejected. Java may need permission for
+its local management socket.
+
+## Read every model with /statechart
+
+Use pstack **`/statechart`**, with the Codex adapter when applicable. Follow the
+installed skill's current runtime instructions and use a scratch folder outside
+the repository. The copied model is `PaidRead.tla`, with `overview.mjs` as the
+view and these configurations:
+
+- `single.cfg`: one reader, one crash/restart.
+- `concurrent.cfg`: two readers, no crash.
+- `writers.cfg`: one reader plus an independent nonce writer sharing the file.
+- `concurrent-crash.cfg`: two readers, one crash/restart.
+- `no-save.cfg`, `no-refusal.cfg`, `no-read-lock.cfg`, `no-write-lock.cfg`:
+  deliberately removed protections. Each must break its original invariant.
+
+`DurableBeforeSend`, `NoDuplicateCharge`, `RejectedNeverReauthorizes` and
+`NoDeadlock` must hold in every fixed configuration. The supplied report records
+state counts, counterexamples and exact guard mutations. A passing reproduction
+test never substitutes for a passing invariant check.
+
+## Real-code owner proof
+
+`test/cli/app-read-loop.test.ts` owns saved-header recovery, rejected receipts,
+store corruption/persistence failure, competing writes and overlapping reads.
+`test/core/receipts-lock.test.ts` covers unknown owners and the stale-reclaimer
+race. Avoid copying these contracts into another fixture test.
+
+The process fixture independently exercises abrupt exits after nonce persistence,
+before receipt rename, after persistence, after send and after simulated
+settlement. It also blocks a second process behind a live reader, kills that
+reader and checks exact-payment recovery. Real SDK signing runs on a public test
+key and synthetic data. Transport and settlement are local fixtures.
+
+Removing pre-send save or rejection refusal must fail the existing owner tests.
+Removing the read lock must fail the overlap test; removing the writer lock must
+fail the competing-write test. Restore every mutation and confirm the baseline
+passes again. Do not weaken the invariant to make a control pass.
+
+## Bounds and maintenance
+
+The fixed models cover one payer, network, grant, scope and a fixed supported
+legacy grant-fee challenge. Successful signing and rename durability after process
+exit are assumed. Lock acquisition abstracts the successful atomic directory
+rename; process death makes its lock reclaimable. Unknown owners, PID reuse and
+inaccessible owner processes fail closed in the implementation. The actual lock
+recovery and successor race also have real-code proof.
+
+Real gateway/chain deduplication, live escrow, access records, server-supplied
+nonces, expiry, power loss, remote filesystems and arbitrary numbers of readers
+are outside this proof. There is no liveness proof. The 1,654-state passing crash
+case exceeds the chart budget, so `/statechart` emits only its passing report.
+
+When an owner changes, read its entire relevant path and update the model from
+the code before changing expected blobs. Keep file reads, renames and releases
+separate where the code separates them. Use `/maintain-formal-verification-skill`
+for skipped verification updates. Follow the updated skill once as the next agent
+would, including all negative controls. Keep product and verification changes
+reviewable separately; no commit or publication is implied.
+
+See `verification/paid-read-recovery/README.md` for the result.
+Do not retrieve credentials or run live paid reads as part of this procedure.

.agents/skills/verify-server-supervision/SKILL.md

@@ -0,0 +1,30 @@
+---
+name: verify-server-supervision
+description: Verify the local Personal Server stop and restart boundary. Use when changing the supervisor's backoff, port probing, replacement launch or Stop handling.
+---
+
+# Verify local Personal Server supervision
+
+Read the [transition map, bounds and known finding](../../../verification/server-supervision/README.md).
+The production source and owner replay were reconciled at
+`a55d0a0006da6a743b6452796435afa6ed177dd8`. The [checker](../../../verification/server-supervision/check.py)
+pins their exact Git blobs and requires the named TLC verdicts and CLI events.
+
+Use Python 3.12 or newer, the installed Node and Vitest, and pinned TLC 1.7.4
+with Java. Set `TLA2TOOLS` and `JAVA` to installed paths if mise cannot locate
+them. Run from the CLI root.
+
+```sh
+python3 verification/server-supervision/check.py --out "$(mktemp -d)/proof"
+```
+
+The current port-probe model and route replay show a late restart. The known
+finding must reproduce. The backoff property must hold. The scratch control
+removing its fence must fail on a restart event. The scratch port fence must
+prevent that event, and the restored source must reproduce both original
+results. The replay uses controlled handles and starts no Personal Server.
+
+Read every outcome with Pstack `/statechart`. After a code change, reconcile
+the source, the model's await boundaries and the exact replay before moving
+the pinned revision. If the port-probe finding is repaired, change its
+expected verdict only after showing the old path fail and the new path pass.