Repository navigation
pstack: offer formal verification in setup, sync help and guide - #715
Merged
cursor[bot] merged 3 commits intoOct 18, 2026
Merged
Conversation
Ask once at the end of setup whether the user wants a formal verification skill, unless the project already has one. On yes, run /create-formal-verification-skill. The offer matches the existing /create-verification-skill offer. Co-authored-by: lauren <poteto@users.noreply.github.com>
Document /create-formal-verification-skill, the setup-pstack formal verification offer, /ketchup, /sharpen, /in-your-own-words, the Claude Code install, the Opening a PR playbook, the verification skill Helpers section, and Babysit's Origin path. Co-authored-by: lauren <poteto@users.noreply.github.com>
Co-authored-by: lauren <poteto@users.noreply.github.com>
Verdict: PASS+NOTESIndependent verifier (I did not write this PR). Head Repo checks
I also checked each new guide sentence against the skill it describes:
|
| Project | Step 7 offer | Step 8 offer (/create-formal-verification-skill) |
|---|---|---|
| A: no formal verification skill | asked once | asked once, with the skill's exact wording |
B: has lease-model-check |
asked once | not asked. The run named lease-model-check as a project skill that runs a model checker. |
Both projects stayed clean, and each run wrote only its rule file.
Notes (do not block the merge)
- The description says
/create-formal-verification-skillwas "missing everywhere". On main,poteto-help's Pick a skill table already listed it. It was missing only from the guide, the state check, and the recipes. 09-make-it-yours.mdlinks "covers both kinds" to#create-a-project-verification-skill. The formal section has its own anchor,#prove-a-property-with-a-formal-verification-skill. The sentence is true, but the link opens the section above the formal one.- Not part of this PR: in sessions with no
Tasktool, step 1 cannot detect models, and "accept as-is" then makes step 4 ask again with no way out. This PR does not change steps 1 to 4.
CI validate and Cursor Bugbot both passed on abe6307. Bugbot found no issues.
poteto
marked this pull request as ready for review
October 18, 2026 21:57
cursor
Bot
deleted the
lauren/setup-pstack-formal-verification-docs-3e39
branch
October 18, 2026 22:01
caelaxie
added a commit
to pstack-ports/devin-pstack
that referenced
this pull request
Oct 19, 2026
<!-- CURSOR_AGENT_PR_BODY_BEGIN --> synced to [`f9be7aa`](cursor/plugins@f9be7aa). upstream `main` has no later commit that touches `pstack/`. version is `0.15.27` in `plugin.json`, `.devin-plugin/plugin.json`, and the readme marker. ported: - [`75fabace`](cursor/plugins@75fabac) ([#712](cursor/plugins#712)) drop the rewritten-prompt ban from `skills/sharpen/SKILL.md`. kept `triggers: [user]` and the `/pstack:sharpen` description. - [`0148b78c`](cursor/plugins@0148b78) ([#713](cursor/plugins#713)) bump `plugin.json` to `0.15.27`. the same bump is in `.devin-plugin/plugin.json` and the readme marker, which is where this repo records the version. - [`f9be7aa`](cursor/plugins@f9be7aa) ([#715](cursor/plugins#715)) offer formal verification in setup, and sync `poteto-help`, its recipes, and the guide. slash commands keep the `/pstack:` prefix. `.cursor/skills` stays `.devin/skills`. the new setup step is `### 9` because this port already uses `### 8` for the verification offer, after the devin profile steps. skipped: - `harness/pstack/claude-code/` copies in [#712](cursor/plugins#712), [#713](cursor/plugins#713), and [#715](cursor/plugins#715). this port does not carry the generated claude code tree. - [#713](cursor/plugins#713) `pstack/.cursor-plugin/plugin.json`. cursor packaging. the version bump lands in `.devin-plugin/plugin.json` instead. - [#715](cursor/plugins#715) claude code install paragraph in `docs/guide/01-setup.md` (`/plugin marketplace add cursor/plugins`, `~/.claude/rules/pstack-models.md`, link to `docs/harness/claude-code.md`). this port's install section is the devin cli, and that adapter file is not in the repo. - [#715](cursor/plugins#715) `poteto-help` rewrite that adds the claude code install and restates the cursor-only paragraph. this port already replaced that paragraph with the devin wording, and the new text points at the claude code adapter this repo does not carry. <!-- CURSOR_AGENT_PR_BODY_END --> <div><a href="https://cursor.com/agents/bc-9742dd68-493d-5228-b8c3-97349ad35744?cursor_ref=pr_footer&cursor_cta=open_in_web"><picture><source media="(prefers-color-scheme: dark)" srcset="https://cursor.com/assets/images/open-in-web-dark.png"><source media="(prefers-color-scheme: light)" srcset="https://cursor.com/assets/images/open-in-web-light.png"><img alt="Open in Web" width="114" height="28" src="https://cursor.com/assets/images/open-in-web-dark.png"></picture></a> <a href="https://cursor.com/background-agent?bcId=bc-9742dd68-493d-5228-b8c3-97349ad35744&cursor_ref=pr_footer&cursor_cta=open_in_cursor"><picture><source media="(prefers-color-scheme: dark)" srcset="https://cursor.com/assets/images/open-in-cursor-dark.png"><source media="(prefers-color-scheme: light)" srcset="https://cursor.com/assets/images/open-in-cursor-light.png"><img alt="Open in Cursor" width="131" height="28" src="https://cursor.com/assets/images/open-in-cursor-dark.png"></picture></a> </div> Co-authored-by: Cursor Agent <cursoragent@cursor.com> Co-authored-by: Kaitian Xie <caelaxie@users.noreply.github.com>
![https://cursor.com/assets/images/open-in-web-dark.png"><source](https://cursor.com/assets/images/open-in-web-dark.png"><source){kind=link}
![https://cursor.com/assets/images/open-in-web-light.png"><img](https://cursor.com/assets/images/open-in-web-light.png"><img){kind=link}
![https://cursor.com/assets/images/open-in-web-dark.png"></picture></a> <a](https://cursor.com/assets/images/open-in-web-dark.png"></picture></a> <a){kind=link}
![https://cursor.com/assets/images/open-in-cursor-dark.png"><source](https://cursor.com/assets/images/open-in-cursor-dark.png"><source){kind=link}
![https://cursor.com/assets/images/open-in-cursor-light.png"><img](https://cursor.com/assets/images/open-in-cursor-light.png"><img){kind=link}
![https://cursor.com/assets/images/open-in-cursor-dark.png"></picture></a> </div](https://cursor.com/assets/images/open-in-cursor-dark.png"></picture></a> </div){kind=link}
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What changes
/setup-pstackgets a new step 8. If the project has no formal verification skill, setup offers once to run/create-formal-verification-skill. A yes runs it. A no moves on. The offer works the same way as the step 7 verification-skill offer.poteto-helpanddocs/guide/now match the skills pstack ships today:/create-formal-verification-skillwas missing everywhere. It now has its own section in Verify and ship, the setup offer on page 1, the generator list on page 9, a recipe on page 10, a state check inpoteto-help, and a recipe inpoteto-help's recipes file./ketchup,/sharpen, and/in-your-own-wordswere not in the guide. The guide now covers them on pages 2, 7, and 10./ketchupis also inpoteto-help's recipes.poteto-help. Both now give the install commands, thepstack:prefix, the Claude Code path for the model rule, and a link to the adapter.The docs do not mention
maintain-formal-verification-skill, because that skill comes in a separate PR. The pstack version stays the same.Checks
node scripts/check-pstack-docs.mjs: 0 problems, 31 of 31 commands named in the guide.node scripts/generate-pstack-harness-trees.mjs --check: up to date.node scripts/validate-plugins.mjs: all plugins valid.Note
Low Risk
Documentation and optional setup-skill flow only; no runtime product or auth changes.
Reviewed by Cursor Bugbot for commit abe6307. Bugbot is set up for automated code reviews on this repo. Configure here.