[arjitj2]

Closes #164

What changed

Adapts Cursor Pstack 0.15.28 through d457567 as distribution 1.17.6.

• Add formal-verification creation and maintenance skills, with active-host local registration, bounded-scope reporting and verification-only updates.
• Add independent optional Setup offers and Help pointers. Generation requires explicit consent after successful smoke.
• Keep every Ketchup waiting item without a word-count cutoff. Allow Sharpen to deliver an explicitly requested rewrite while completing the task.

The shared Codex/Claude tree, saved provider policy and README content are preserved. Cursor guides and duplicate packaging remain excluded. Newer Sharpen rewrite-only and Statechart changes are separate work in #168; this is not the latest Cursor checkpoint.

Verification

• Exact-head Linux CI: 39811520183, 993 Bun passes, five platform skips, zero failures; strict/static/provenance, maintenance27, hook8 and docs16 pass.
• Exact package installed in disposable Codex and Claude profiles: 1.17.6, tree 26be5ce9990e8422b7b67b6fe683291e843359a5, all 240 files verified. Final metadata head a57749a has the same package as host-tested 585d2dd.
• Native changed-behavior cases below, with limits stated.
• Independent exact-head Shipping verdict; keep draft until it passes. No merge request is armed.

Both hosts retained all30 Ketchup items from a supplied digest; Claude renamed their labels. Sharpen calculated29 across4 CSV rows against an independent control and returned the requested rewrite. Help named the new formal pair.

Both hosts loaded the formal generator. Its inspected artifacts were staged and registered by the parent in .agents/skills/verify-token-parser or .claude/skills/verify-token-parser. Native project-skill loading and real parser checks then ran: Codex380pass / planted fault65fail / restored380pass / original380pass; Claude377pass / fault65fail / restored377pass / original377pass. This was supervised generation across phases, not autonomous one-turn creation.

Native maintenance read the actual fixture commits, distinguished a no-effect formatting change from an intentional ABC contract change and renamed implementation, and identified the old pass as stale. Updated native checks passed1381 cases in Codex and2757 checks in Claude; planted faults produced175 and350 failures respectively. A separate later commit removed character rejection without changing requirements. Both hosts reported the exact introducing commit and real counterexample, preserved the property, and left product code unchanged.

Setup guard cases used supplied success/failure/consent/harness states. Both hosts selected the correct offers and suppression rules. Existing steps1–10 are byte-identical; unchanged probes and persistence were not repeated. Full setup yes-to-generator transactions and automatic harness discovery remain unverified; generator registration/execution was checked separately. No TLA+ engine ran. The parser fallback is bounded real-code testing, not formal proof. It covers ABC! at lengths0–5 plus sampled nonstrings.

Local Node24 full suite failed:994 passes,4 failures and3 additional errors in unchanged timing fixtures. Cause is unproven; related #141 remains separate. Do not read Linux CI as a local-green claim.

Initial manual-only Skill calls were rejected; direct user slash invocations succeeded. Interrupted and ENOTFOUND attempts are retained. Codex execution stopped on temp/cache restrictions, then passed with the existing direct Python binary. Claude's maintenance proposal continued after a denied compound command; its effects were inspected and retained as a deviation. Later updated native-skill execution passed with constant commands and no denials. These results do not prove universal policy compliance, automatic skill selection or OS confinement.

Independent source review passed with notes through the approved Sol backup after Opus's terminal ENOTFOUND. Provider diversity was reduced. No-comments review found zero applicable code comments. Detailed retained receipts, commands, hashes and failures: /Users/arjitjaiswal/open-pstack-d457567/result.md.

The personal Codex1.17.5 package, unpinned fork source, assignments and all five captured model/instruction/Claude file hashes remain unchanged during validation. A guarded merge, immutable release and verified Codex rollout remain pending.

Documentation impact

UPSTREAM.md, CHANGELOG.md and the verification recipe record the new skills, source decisions and evidence limits. README.md is unchanged. Related monitor #1, catalog #167 and next-unit #168.

[arjitj2]

Independent Opus5.5/high Shipping inspection at a57749a6953240d97afb8e8a17045573c52b7086 returned NO VERDICT, not PASS.

Verdict: no verdict. This is not a PASS, and it gives no authority to land PR165 at a57749a against base a16c327. I stopped partway because the Read tool was denied, so the required checks are incomplete.

What was denied: I asked to read the two generated helpers:

• /Users/arjitjaiswal/open-pstack-d457567/codex-fixture2/verification/check_token.py
• /Users/arjitjaiswal/open-pstack-d457567/claude-fixture2/verification/check_token.py

Both requests were refused ("permissions … you haven't granted it yet"). The contract says not to retry or find another route, so I did not read them with Bash cat and did not run them without reading them first. I also did not start the remaining evidence reads. Earlier Bash reads of other files in that folder had worked.

Commands I ran and what they showed:

• Same package tree on both commits: git rev-parse 585d2dd:plugins/pstack and the same for a57749a both give 26be5ce9990e8422b7b67b6fe683291e843359a5, which has 240 files.
• Only metadata changed after testing: git diff 585d2dd a57749a touches only CHANGELOG.md, UPSTREAM.md and maintenance/upstream-ledger.json.
• README and provider files untouched: comparing base to head for README.md, poteto-mode/references/ and runner/types.ts shows no changes. Saved models, efforts, fallbacks, spending policy and provider optionality are therefore unchanged.
• Version: all three manifests go from 1.17.5 to 1.17.6, a patch bump, never a major one.
• python3 scripts/check-docs.py (CommandLineTools python3): Check-docs: ok.
• python3 scripts/fork-maintenance.py check-ledger: ledger ok: 62 entries, coverage checked.
• One combined Bash command was blocked as needing approval. I reran only the two checks above as separate single commands.

What I reviewed by reading:

• I read AGENTS.md, UPSTREAM.md, the full base-to-head diff (all 16 files, including the six changed skills), result.md, pre-final-integrity.json, maintenance-history.json, source-review-sol.md and comments-review.md.
• The ten source decisions: adapted are 16541c6, 4382e68, 75fabac, f9be7aa, 6b78e9f and 7b353f7; adopted is bc14437; excluded are 0b8e952, 0148b78 and d457567. Each matches what the diff actually changed.
  • The f9be7aa reason says the full Setup yes-path is unverified.
  • The 6b78e9f reason says no TLA+ engine ran.
  • The 7b353f7 reason keeps the record of the earlier policy deviation.
• The ledger has no entries for 88d4751 or eb4db2b, and nothing claims the fork is caught up to the latest upstream.
• The CHANGELOG and NOTICE wording does not claim formal proof, automatic skill selection or a green local suite.
• The integrity file shows all five personal hashes unchanged, product and requirements kept in both fixtures, and fault copies removed.

Not done, so these remain open:

1. Running both helpers against <host>-prebug-product.py (expected 0) and against current <host>-fixture2/token_parser.py (expected 1). Nothing was run.
2. candidate.json was not read.
3. I did not compare either host's native event logs or final replies for verify4/verify3, maintain1, maintain-verify, maintain-bug, setup-guards or manual2. I have not independently confirmed that the generated skill was natively registered, loaded and run on each host, or any of the pass and fail counts. I have only the claims in result.md.
4. I did not compare the changes against the pinned upstream.diff. My review of the decisions used the candidate diff and the earlier independent source review only.
5. The gaps listed in the brief stay as stated in result.md, not checked by me:
   • supervised multi-phase generation rather than autonomous creation;
   • a Python generated-input fallback with no TLA+ engine;
   • Setup tested only on supplied states, with no full yes-path run;
   • the earlier invocation, DNS, launcher and cache failures;
   • the Claude maintenance stop-on-denial violation;
   • the overlapping read-only commands;
   • the local suite failing (994 pass, 4 fail, 3 errors; issue141).

What would unblock this: grant read access to the two check_token.py files and to the native logs in the evidence folder, or have the parent run those reads and the two helper runs and inspect them. After that, a fresh exact-head review needs to finish items 1–4. Even then, landing would still depend on green CI for a57749a itself; CI from older commits does not count.

I wrote no files, made no Git changes and used no network.

Parent follow-up: copied77 required evidence files into the reviewer worktree with an original-path/SHA256 manifest. Parent correct-source replays returned0; bug-source replays returned1 in both fixtures. These parent checks do not replace the missing independent verdict. A scoped fresh-review approval is pending under the saved worker policy; the previous complete receipt is not treated as fallback eligibility or release approval. Final exact-head CI39811520183 is green. PR remains draft.