1.17.6: formal verification workflows

Release checkpoint: 9086657cb08d544f9e315c1b5074cac901331447; package tree 26be5ce9990e8422b7b67b6fe683291e843359a5.

Adopts Cursor Pstack 0.15.28, source d457567332aa6989e753ea289f30ea2bfbc80bc0, through PR #165.

Adds formal-verification creation and maintenance skills, optional Setup offers and Help entry points. Ketchup retains every waiting item without a word-count cutoff. Sharpen can return an explicitly requested rewrite while completing the task.

Generated skills use the active host's project directory. The shared Codex/Claude tree, parent Git ownership, saved model descriptors, efforts, recovery and spending policy are preserved. The two formal skills remain model-invocable for parent workflows, including Setup creation after consent; upstream manual-only flags are deliberately excluded. Automatic selection remains unverified. README.md is unchanged. Adaptations and exclusions are recorded in the release checkpoint's UPSTREAM.md.

Validation:

• Exact candidate CI: 993 Bun passes, five platform skips, zero failures; strict/static/provenance, maintenance 27, hook 8 and docs 16 passed.
• Both real hosts loaded the candidate and generated native local skills. The parent inspected, staged and registered generated artifacts. Native baseline, planted-fault, restored and final checks passed. Maintenance identified stale coverage, adapted to an intentional contract change and detected a separate product bug without changing product code or requirements.
• All 240 packaged files at final candidate 2c7c6e2fbb65ffdad61c4b156a4241b7433ec73f match host-tested 585d2ddf55ce586a0a79a2ae0e39d018eb1dc6a8; package tree 26be5ce9990e8422b7b67b6fe683291e843359a5.
• Independent exact-head Shipping verdict and the detailed host evidence are published on PR #165.

Limits: parser checks are bounded real-code tests, not formal proof. No TLA+ engine ran. Generation was supervised across phases, and the parent supplied execution commands. Codex generated-skill loading is supported by registration, intended prompts and execution; no separate load event or captured stdin was retained. The Help formal recipe is partly covered. Setup guards used supplied scenario states; complete yes-to-generator transactions, new probes, persistence and automatic discovery remain unverified. Prior denials, interrupted attempts and Claude stop-on-denial deviations are retained in the PR. Local Node 24 tests failed with 994 passes, four failures and three additional errors in unchanged timing fixtures; the cause remains unproven in issue #141. Linux CI is not a local-green claim.

Newer Cursor changes through 0.15.34 remain separate work in issue #168. This release does not include that backlog.

Previous tested checkpoint and rollback: v1.17.5, commit ff5bdb273df33bccd397b627be2e0cb398a580cc, package tree e678abcef184b3b6b05115eb2affe75b2bb94d14. Pin that immutable tag if rollback is required; preserve personal model assignments and Claude installation state.