diff --git a/harness/pstack/claude-code/docs/guide/01-setup.md b/harness/pstack/claude-code/docs/guide/01-setup.md index e28f5cbab..2c2ef3413 100644 --- a/harness/pstack/claude-code/docs/guide/01-setup.md +++ b/harness/pstack/claude-code/docs/guide/01-setup.md @@ -12,6 +12,8 @@ In a Cursor chat, run: Cursor confirms the plugin is installed. +In Claude Code, run `/plugin marketplace add cursor/plugins`, then `/plugin install pstack@cursor-plugins`. Claude Code prefixes plugin commands, so each command in this guide takes a `pstack:` prefix there, such as `/pstack:setup-pstack`, which writes its model rule to `~/.claude/rules/pstack-models.md`. The [Claude Code adapter](../harness/claude-code.md) covers the other differences. + ## Pick your models Run: @@ -28,7 +30,7 @@ You only override what you care about. A role with no line in the rule keeps the You might be wondering what happens if you use Auto. Set a role to `inherit-parent` or `auto` and pstack omits the subagent `model` field, so the subagent inherits your parent chat model. Both values mean the same thing, and neither is a model slug. For a panel role the value is a list, and one subagent runs per entry, so the list length sets the panel size. Setup also configures `swarm workers`, the default model for every `/swarm` worker unless a race names a model for each arm. -## Accept the verification offer, or don't +## Accept the verification offers, or don't At the end of setup, `/setup-pstack` looks for a way to prove app behavior in your project, either a `verify-*` skill or an existing harness. If it finds neither, it offers once to generate one with [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md). @@ -36,6 +38,8 @@ Say yes and it writes `.cursor/skills/verify-/`, a project-local skill that If you're new to pstack, say yes. An agent that can check its own work keeps going until the check passes. An agent that can't hands every result back to you to check by hand. Of everything in this guide, the verification skill pays off the most. +Then setup offers once to generate a formal verification skill with [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md), unless the project already has one. Tests check the cases someone thought to write. A formal verification skill checks one key property of your code, such as "a job never runs twice at once", in every case within a stated scope. Say yes when your code has concurrency, retries, a state machine, or a parser, where a bug is costly and tests rarely reach the case that breaks. Otherwise say no, and run it later if that changes. [Verify and ship](./06-verify-and-ship.md#prove-a-property-with-a-formal-verification-skill) covers it. + After setup, start a new chat. The model rule applies to new sessions. ## Keep the cost in check diff --git a/harness/pstack/claude-code/docs/guide/02-poteto-mode.md b/harness/pstack/claude-code/docs/guide/02-poteto-mode.md index 0e6568e17..db16b5e95 100644 --- a/harness/pstack/claude-code/docs/guide/02-poteto-mode.md +++ b/harness/pstack/claude-code/docs/guide/02-poteto-mode.md @@ -25,7 +25,7 @@ flowchart TD J --> K ``` -The diagram shows the common routes. There are also playbooks for hillclimbing a metric, diagnosing runtime symptoms and captured traces, prototypes, visual parity, authoring and evaluating skills, autonomous runs, babysitting a PR or stack to merge-ready, shipping a verified stack, running a PR queue or a stack on autopilot, orchestrating project-scale programs, session pickup, pausing safely, multi-phase plans, and worktree cleanup. The [playbook directory](../../skills/poteto-mode/playbooks/) has the full set. +The diagram shows the common routes. There are also playbooks for hillclimbing a metric, diagnosing runtime symptoms and captured traces, prototypes, visual parity, authoring and evaluating skills, autonomous runs, opening a PR, babysitting a PR or stack to merge-ready, shipping a verified stack, running a PR queue or a stack on autopilot, orchestrating project-scale programs, session pickup, pausing safely, multi-phase plans, and worktree cleanup. The [playbook directory](../../skills/poteto-mode/playbooks/) has the full set. ## Say the goal, not the ceremony @@ -64,7 +64,15 @@ For a noisy report, such as a long thread or a vague bug, make the restatement t /poteto-mode read this thread. restate the underlying issue in your own words, in plain english. don't change any code yet. ``` -A misreading shows up in the restatement, before any code exists. Correct it there, and it costs you one message instead of one wrong fix. +A misreading shows up in the restatement, before any code exists. Correct it there, and it costs you one message instead of one wrong fix. For the restatement alone, with no playbook, run [`/in-your-own-words`](../../skills/in-your-own-words/SKILL.md). It restates what the agent thinks your goals are and what problem you're trying to solve. + +When you're unsure whether a task is aimed right, put [`/sharpen`](../../skills/sharpen/SKILL.md) in front of it: + +```text +/sharpen write a migration guide for the v2 config format. +``` + +Before it starts, the agent asks how a top expert would do the task, what you're really after, and whether the ask is over- or underspecified. It drops constraints that don't serve the goal as readily as it adds ones that do, leaves your choices open, and keeps one outside check that the result is right. Then it does the work. ## Follow up short diff --git a/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md b/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md index 2fa0c8d8f..62a0a059b 100644 --- a/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md +++ b/harness/pstack/claude-code/docs/guide/06-verify-and-ship.md @@ -1,6 +1,6 @@ # Verify the result and open a PR -"It compiles" is not evidence. The [Prove It Works principle](../../skills/principle-prove-it-works/SKILL.md) makes the agent check the real artifact before it reports success, and your job is to make "the real artifact" checkable. This page covers stating a finish condition, vetting a measured number, generating a verification skill for your app, opening the PR, and driving it to merged. +"It compiles" is not evidence. The [Prove It Works principle](../../skills/principle-prove-it-works/SKILL.md) makes the agent check the real artifact before it reports success, and your job is to make "the real artifact" checkable. This page covers stating a finish condition, vetting a measured number, generating a verification skill for your app, formally verifying a property tests rarely reach, opening the PR, and driving it to merged. Verification is the slowest step in most agent work, because it's the step that usually waits on a human. Make the agent able to do it, and you stop being the bottleneck. Skip it, and running more agents only gets you more unchecked work to review. @@ -58,7 +58,7 @@ The UI bullet above hides a real requirement. The agent needs a scripted way to [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) interviews the repository, not you. It works out what a user touches, how the app launches locally, what can drive it (an existing harness first, otherwise browser and CDP, a PTY, or plain HTTP), what evidence proves behavior, and whether two instances can run side by side. It asks you only what the code can't answer. -It writes `.cursor/skills/verify-/`, agent-facing instructions with exact Launch, Doctor, Drive, Evidence, and Cleanup sections, plus a feature map under `features/` that indexes what the app does and what result proves each feature works. The skill ships a [worked feature-map example](../../skills/create-verification-skill/references/feature-map-example/) with a README index and one file per feature using the four required H2s. Before handing it over, the generator proves the skill once end to end: launch, doctor check, drive one feature, capture evidence, clean up. If that proof fails, don't use the output. +It writes `.cursor/skills/verify-/`, agent-facing instructions with exact Launch, Doctor, Drive, Evidence, and Cleanup sections, a Helpers section for any script it ships, plus a feature map under `features/` that indexes what the app does and what result proves each feature works. The skill ships a [worked feature-map example](../../skills/create-verification-skill/references/feature-map-example/) with a README index and one file per feature using the four required H2s. Before handing it over, the generator proves the skill once end to end: launch, doctor check, drive one feature, capture evidence, clean up, then confirm the evidence survived the cleanup. If that proof fails, don't use the output. From then on, "verify it in the app" is a step any agent can execute, in this repo, with no setup conversation. Name it in the prompt when you want the proof in a specific form: @@ -93,6 +93,26 @@ Apps change, and feature maps go out of date. Run this at least once a day, idea [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) audits the generated skill: one read-only source reader per feature in parallel, then one live pass that drives every mapped feature. It ends in exactly one of three outcomes. `clean` means full coverage and nothing to ship. `changed` means one PR of proven corrections, confined to the verification skill's own directory. `blocked` names the blocker. It never edits product code. If the live pass catches a product regression, it reports the regression instead of hiding it with a doc edit. +## Prove a property with a formal verification skill + +A verification skill proves the paths you drive. Some bugs live on paths nobody drives: two retries that overlap, a lock that expires mid-write, a state change that arrives out of order. Tests rarely reach those cases. For code where such a bug is costly, run: + +```text +/create-formal-verification-skill +``` + +[`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md) picks the target from the code: a promise the code makes, where a break harms users and tests rarely reach the case that breaks it. It picks the strongest target, not the easiest to verify. Name an area or a bug to start there instead: + +```text +/create-formal-verification-skill the job lease and retry logic. a job must never run twice at once. +``` + +The question picks the tool. Whether events can happen in a bad order suits a model checker over a small model of the design. Whether the code behaves for every input suits a verifier that runs on the code. A property that must hold at every size can need a proof. The agent tells you which tool it chose and why. + +It verifies one property and shows that property failing on a broken variant of the code, because a check you've never seen fail proves nothing. When the current code already breaks the property, you get the counterexample as a short sequence of steps in your code's terms. The property stays as stated, so the finding stays a finding. Product code doesn't change unless you ask. + +It writes a project-local skill that tells the next agent whether a change touches the verified code, how to run the check with one command, and how to tell a real bug from a modeling error. Before handing it over, the generator follows that skill once on a scratch change that breaks the property, and the check must catch it. The handoff says what was verified, with which tool and bounds, what the check found, and what it doesn't cover. A pass covers the model or the bound, not the whole system. + ## Open the PR ```text @@ -109,7 +129,7 @@ An open PR starts collecting blockers immediately. Checks fail, reviewers commen /poteto-mode babysit this pr. get it green. ``` -Babysit watches the PR with a bundled watcher and takes blockers in order: conflicts, then review threads, then CI. Every known fix batches into one push, so the checks restart once instead of after every fix. The comment triage is skeptical, because humans and bots file real catches and noise in the same list. A real finding gets a fix, and noise gets dismissed with the disproof posted on the thread. When all you want is status, ask smaller and Babysit answers without starting the loop: +Babysit watches the PR, with a bundled watcher on GitHub or the Origin CLI when it's available, and takes blockers in order: conflicts, then review threads, then CI. Every known fix batches into one push, so the checks restart once instead of after every fix. The comment triage is skeptical, because humans and bots file real catches and noise in the same list. A real finding gets a fix, and noise gets dismissed with the disproof posted on the thread. When all you want is status, ask smaller and Babysit answers without starting the loop: ```text /poteto-mode check on pr 123. anything outstanding? diff --git a/harness/pstack/claude-code/docs/guide/07-overnight.md b/harness/pstack/claude-code/docs/guide/07-overnight.md index 043ea5197..948466776 100644 --- a/harness/pstack/claude-code/docs/guide/07-overnight.md +++ b/harness/pstack/claude-code/docs/guide/07-overnight.md @@ -67,6 +67,8 @@ When you're back, ask for the run in review form: Before the skill hands back its summary, it spawns a reviewer on a different model family to read the trail and the transcript, and the reply ends with an Attention section listing what deserves your scrutiny. Read that section first, then the log rows it points at. You're auditing decisions, not re-reading the whole night. +For a quick status instead of an audit, run [`/ketchup`](../../skills/ketchup/SKILL.md) in the chat that ran the work. It reads only, and tells you in plain words what changed since your last message, with the screenshots and small diagrams the work produced. Then it lists each call waiting on you, such as a merge, an approval, or a choice between options, with its pick, the evidence, and the risk, so you can decide from the reply alone. + ## When the night holds a queue, not a task The contract above drives one task to one finish condition. Some nights hold more, a queue of independent changes or a whole program. Three playbooks scale the same trust up. diff --git a/harness/pstack/claude-code/docs/guide/09-make-it-yours.md b/harness/pstack/claude-code/docs/guide/09-make-it-yours.md index cb3c20188..457341aa4 100644 --- a/harness/pstack/claude-code/docs/guide/09-make-it-yours.md +++ b/harness/pstack/claude-code/docs/guide/09-make-it-yours.md @@ -59,7 +59,7 @@ When you already know the workflow you want to capture: Writing a skill matches the [Authoring or modifying a skill playbook](../../skills/poteto-mode/playbooks/authoring-a-skill.md), which routes through Cursor's built-in `create-skill`, validates the frontmatter and links, and ships the result through the Opening a PR playbook. Agent-facing prose has a higher bar than human prose, because an unhelpful sentence becomes an instruction some future agent follows. Let the playbook hold that bar rather than writing a `SKILL.md` freehand. -One special case has its own generator. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers both. +Two special cases have their own generators. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. A skill that checks a property of your code with a model checker, a proof, or another verifier is a formal verification skill, so use [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md). [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers both kinds. ## Write docs to a standard with `/technical-writing` diff --git a/harness/pstack/claude-code/docs/guide/10-recipes-and-pitfalls.md b/harness/pstack/claude-code/docs/guide/10-recipes-and-pitfalls.md index 6d2ef465c..fb4743c29 100644 --- a/harness/pstack/claude-code/docs/guide/10-recipes-and-pitfalls.md +++ b/harness/pstack/claude-code/docs/guide/10-recipes-and-pitfalls.md @@ -18,7 +18,15 @@ Mechanics first, history second. Each skill's report tells you which sources it /poteto-mode read this thread. restate the underlying issue in your own words, in plain english. don't change any code yet. ``` -A misreading shows up in the restatement, where it costs one message to correct. Keep your own theory to yourself until the agent has stated its own. +A misreading shows up in the restatement, where it costs one message to correct. Keep your own theory to yourself until the agent has stated its own. `/in-your-own-words` asks for the restatement alone, with no playbook. + +## Aim a task before it starts + +```text +/sharpen write the onboarding doc for the new billing service. +``` + +The agent asks how an expert would do the task, what you're really after, and whether the ask says too much or too little. It keeps one outside check that the result is right, then does the work. ## Prototype before you pick @@ -76,6 +84,14 @@ The qualifiers do real work. "don't change anything yet" keeps it read-only, and "if it repros on main" lets the run stop early when the bug is already gone. The video lets you check the fix before you read the diff. +## Prove a property tests rarely reach + +```text +/create-formal-verification-skill the retry queue. a message must never be delivered twice. +``` + +You get one property checked in every case within a stated scope, a counterexample in your code's terms if the code already breaks it, and a project skill the next agent runs on any change to that code. + ## Vet a number before you post it ```text @@ -134,6 +150,14 @@ You rarely need more words. You need the right name, and [the principles page](. That's the whole prompt. [`/bro`](../../skills/bro/SKILL.md) restates the last message like one human talking to another, no jargon, shorter. Use it when a reply is technically thorough and you still don't know what it said. +## Catch up on a chat you left running + +```text +/ketchup +``` + +[`/ketchup`](../../skills/ketchup/SKILL.md) tells you in plain words what changed since your last message, then lists each call waiting on you with its pick, evidence, and risk. It changes nothing while it reports. + ## The pitfalls - **Enumerating skills in the prompt.** "use /how then /architect then /arena" reorders steps the playbook already sequences. State the goal and constraints. Name a skill only to override a default. diff --git a/harness/pstack/claude-code/docs/guide/README.md b/harness/pstack/claude-code/docs/guide/README.md index 627bfb222..17422b992 100644 --- a/harness/pstack/claude-code/docs/guide/README.md +++ b/harness/pstack/claude-code/docs/guide/README.md @@ -9,7 +9,7 @@ Here's what you'll learn: 3. [Understand the code](./03-understand.md). A read-only investigation, then `/how`, `/why`, `/teach`, and `/recall` before you edit anything. 4. [Design the change](./04-design.md). `/architect`, `/arena`, `/swarm`, `/interrogate`, prototypes, and plans before code locks in a shape. 5. [Build and clean the change](./05-build-and-clean.md). The build playbooks, `/tdd`, `/unslop`, and `/no-comments`. -6. [Verify and ship](./06-verify-and-ship.md). Prove behavior on the real app, vet numbers with `/benchmark-checklist`, then open a focused PR and drive it to merged. +6. [Verify and ship](./06-verify-and-ship.md). Prove behavior on the real app, formally verify what tests rarely reach, vet numbers with `/benchmark-checklist`, then open a focused PR and drive it to merged. 7. [Run work while you sleep](./07-overnight.md). Trust before loops, an overnight contract, a decision log you can audit, and Projects and automations that scale past one agent. 8. [Steer with principle names](./08-principles.md). The 24 names that redirect an agent mid-task. 9. [Make it yours](./09-make-it-yours.md). Your own mode, `/correct` for repeated mistakes, and how to test a skill change. diff --git a/harness/pstack/claude-code/skills/poteto-help/SKILL.md b/harness/pstack/claude-code/skills/poteto-help/SKILL.md index f2bd10675..fc89d3b53 100644 --- a/harness/pstack/claude-code/skills/poteto-help/SKILL.md +++ b/harness/pstack/claude-code/skills/poteto-help/SKILL.md @@ -28,6 +28,7 @@ Check the state that changes the answer, and mention it only when it does: - No `~/.cursor/rules/pstack-models.mdc` means `/setup-pstack` hasn't run for this user, so every role uses its default model. - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When the model rule is missing and it matters, ask whether the user wants to pick a model for each role and a reasoning budget now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -37,14 +38,16 @@ When the model rule is missing and it matters, ask whether the user wants to pic ## Get set up 1. Install with `/add-plugin pstack` in chat, or from Customize in the sidebar. -2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It asks for a reasoning budget, maps a model to each role, and writes a rule. The rule applies to new chats. +2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It asks for a reasoning budget, maps a model to each role, and writes a rule. The rule applies to new chats. Then it offers once each to generate a verification skill and a formal verification skill for the project, unless the project already has one. 3. Start a real task with `/poteto-mode`, a goal, and a check that can pass or fail. Installing changes nothing until the user invokes a skill. Only `/setup-pstack` loads from the user's words. The [README](../../README.md) and [guide page 1](../../docs/guide/01-setup.md) have the details. Offer to word their first prompt with them, per [`references/prompting.md`](references/prompting.md). If cost is the worry, say where the tokens go and how to spend fewer. pstack spends extra tokens on subagents and review panels. Rerun `/setup-pstack` and pick a smaller budget or cheaper models. A role set to `auto` or `inherit-parent` runs on the chat's model, which saves tokens when the chat runs on Auto or a cheaper model. A shorter panel list runs fewer subagents, one for each entry. Save `/poteto-mode` for work that needs rigor. -pstack is built for Cursor. Its skills use the Agent Skills format, so other tools can read them. But most workflow skills, including `/poteto-mode`, `/how`, `/why`, and `/teach`, spawn Cursor subagents with per-role models, and Custom Modes and `/loop` are Cursor features, so those parts may not work there. +pstack is built for Cursor, and it also installs in Claude Code with `/plugin marketplace add cursor/plugins`, then `/plugin install pstack@cursor-plugins`. There, each command takes a `pstack:` prefix, such as `/pstack:poteto-mode`. The [Claude Code adapter](../../docs/harness/claude-code.md) maps the Cursor names, and a step that needs a Cursor-only feature, such as Bugbot or Automations, is skipped with a one-line note. + +Other tools can read the skills, because they use the Agent Skills format. But most workflow skills, including `/poteto-mode`, `/how`, `/why`, and `/teach`, spawn Cursor subagents with per-role models, and Custom Modes and `/loop` are Cursor features, so those parts may not work there. ## Start a task with `/poteto-mode` diff --git a/harness/pstack/claude-code/skills/poteto-help/references/recipes.md b/harness/pstack/claude-code/skills/poteto-help/references/recipes.md index d13da3a08..2d785761d 100644 --- a/harness/pstack/claude-code/skills/poteto-help/references/recipes.md +++ b/harness/pstack/claude-code/skills/poteto-help/references/recipes.md @@ -34,6 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too. +- `/create-formal-verification-skill prove holds in , even when interleave or retry.` - `/swarm check every package under against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr . anything outstanding?` @@ -43,6 +44,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/poteto-mode im going to bed. in a fresh worktree off . done means . keep a decision log. don't ask me before committing. /loop until done. if you're truly stuck after a few hours, stop and write up why.` - `/show-me-your-work catch me up on what you did last night.` Read its Attention section first. +- `/ketchup` catches you up on this chat since your last message and lists every call that waits on you. - `/poteto-mode full autopilot on this queue. each item is independent.` - `/poteto-mode autopilot these changes but stack them, don't ship. i'll land the stack.` - `/reflect capture what we learned so the next run doesn't repeat it.` Approve only edits that change a future decision. diff --git a/harness/pstack/claude-code/skills/setup-pstack/SKILL.md b/harness/pstack/claude-code/skills/setup-pstack/SKILL.md index 4b657c24e..672bb4bef 100644 --- a/harness/pstack/claude-code/skills/setup-pstack/SKILL.md +++ b/harness/pstack/claude-code/skills/setup-pstack/SKILL.md @@ -74,3 +74,7 @@ Tell the user the rule was written and that it applies to new sessions. Re-runni ### 7. Offer a verification skill (optional) Check whether the project has a way to drive the real app for proof (a `verify-*` skill, or an existing harness). If not, offer once: "want a project-local verification skill, so agents can drive the app the way a user does and prove changes work? I can generate one with /create-verification-skill." On yes, invoke `/create-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. + +### 8. Offer a formal verification skill (optional) + +Check whether the project already has a formal verification skill (a project skill that runs a model checker, a proof, or another verifier against the code). If not, offer once: "want a formal verification skill, so agents can prove a key property of your code holds in every case in scope, not only the cases tests reach? I can generate one with /create-formal-verification-skill." On yes, invoke `/create-formal-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. diff --git a/pstack/docs/guide/01-setup.md b/pstack/docs/guide/01-setup.md index e28f5cbab..2c2ef3413 100644 --- a/pstack/docs/guide/01-setup.md +++ b/pstack/docs/guide/01-setup.md @@ -12,6 +12,8 @@ In a Cursor chat, run: Cursor confirms the plugin is installed. +In Claude Code, run `/plugin marketplace add cursor/plugins`, then `/plugin install pstack@cursor-plugins`. Claude Code prefixes plugin commands, so each command in this guide takes a `pstack:` prefix there, such as `/pstack:setup-pstack`, which writes its model rule to `~/.claude/rules/pstack-models.md`. The [Claude Code adapter](../harness/claude-code.md) covers the other differences. + ## Pick your models Run: @@ -28,7 +30,7 @@ You only override what you care about. A role with no line in the rule keeps the You might be wondering what happens if you use Auto. Set a role to `inherit-parent` or `auto` and pstack omits the subagent `model` field, so the subagent inherits your parent chat model. Both values mean the same thing, and neither is a model slug. For a panel role the value is a list, and one subagent runs per entry, so the list length sets the panel size. Setup also configures `swarm workers`, the default model for every `/swarm` worker unless a race names a model for each arm. -## Accept the verification offer, or don't +## Accept the verification offers, or don't At the end of setup, `/setup-pstack` looks for a way to prove app behavior in your project, either a `verify-*` skill or an existing harness. If it finds neither, it offers once to generate one with [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md). @@ -36,6 +38,8 @@ Say yes and it writes `.cursor/skills/verify-/`, a project-local skill that If you're new to pstack, say yes. An agent that can check its own work keeps going until the check passes. An agent that can't hands every result back to you to check by hand. Of everything in this guide, the verification skill pays off the most. +Then setup offers once to generate a formal verification skill with [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md), unless the project already has one. Tests check the cases someone thought to write. A formal verification skill checks one key property of your code, such as "a job never runs twice at once", in every case within a stated scope. Say yes when your code has concurrency, retries, a state machine, or a parser, where a bug is costly and tests rarely reach the case that breaks. Otherwise say no, and run it later if that changes. [Verify and ship](./06-verify-and-ship.md#prove-a-property-with-a-formal-verification-skill) covers it. + After setup, start a new chat. The model rule applies to new sessions. ## Keep the cost in check diff --git a/pstack/docs/guide/02-poteto-mode.md b/pstack/docs/guide/02-poteto-mode.md index 0e6568e17..db16b5e95 100644 --- a/pstack/docs/guide/02-poteto-mode.md +++ b/pstack/docs/guide/02-poteto-mode.md @@ -25,7 +25,7 @@ flowchart TD J --> K ``` -The diagram shows the common routes. There are also playbooks for hillclimbing a metric, diagnosing runtime symptoms and captured traces, prototypes, visual parity, authoring and evaluating skills, autonomous runs, babysitting a PR or stack to merge-ready, shipping a verified stack, running a PR queue or a stack on autopilot, orchestrating project-scale programs, session pickup, pausing safely, multi-phase plans, and worktree cleanup. The [playbook directory](../../skills/poteto-mode/playbooks/) has the full set. +The diagram shows the common routes. There are also playbooks for hillclimbing a metric, diagnosing runtime symptoms and captured traces, prototypes, visual parity, authoring and evaluating skills, autonomous runs, opening a PR, babysitting a PR or stack to merge-ready, shipping a verified stack, running a PR queue or a stack on autopilot, orchestrating project-scale programs, session pickup, pausing safely, multi-phase plans, and worktree cleanup. The [playbook directory](../../skills/poteto-mode/playbooks/) has the full set. ## Say the goal, not the ceremony @@ -64,7 +64,15 @@ For a noisy report, such as a long thread or a vague bug, make the restatement t /poteto-mode read this thread. restate the underlying issue in your own words, in plain english. don't change any code yet. ``` -A misreading shows up in the restatement, before any code exists. Correct it there, and it costs you one message instead of one wrong fix. +A misreading shows up in the restatement, before any code exists. Correct it there, and it costs you one message instead of one wrong fix. For the restatement alone, with no playbook, run [`/in-your-own-words`](../../skills/in-your-own-words/SKILL.md). It restates what the agent thinks your goals are and what problem you're trying to solve. + +When you're unsure whether a task is aimed right, put [`/sharpen`](../../skills/sharpen/SKILL.md) in front of it: + +```text +/sharpen write a migration guide for the v2 config format. +``` + +Before it starts, the agent asks how a top expert would do the task, what you're really after, and whether the ask is over- or underspecified. It drops constraints that don't serve the goal as readily as it adds ones that do, leaves your choices open, and keeps one outside check that the result is right. Then it does the work. ## Follow up short diff --git a/pstack/docs/guide/06-verify-and-ship.md b/pstack/docs/guide/06-verify-and-ship.md index 2fa0c8d8f..62a0a059b 100644 --- a/pstack/docs/guide/06-verify-and-ship.md +++ b/pstack/docs/guide/06-verify-and-ship.md @@ -1,6 +1,6 @@ # Verify the result and open a PR -"It compiles" is not evidence. The [Prove It Works principle](../../skills/principle-prove-it-works/SKILL.md) makes the agent check the real artifact before it reports success, and your job is to make "the real artifact" checkable. This page covers stating a finish condition, vetting a measured number, generating a verification skill for your app, opening the PR, and driving it to merged. +"It compiles" is not evidence. The [Prove It Works principle](../../skills/principle-prove-it-works/SKILL.md) makes the agent check the real artifact before it reports success, and your job is to make "the real artifact" checkable. This page covers stating a finish condition, vetting a measured number, generating a verification skill for your app, formally verifying a property tests rarely reach, opening the PR, and driving it to merged. Verification is the slowest step in most agent work, because it's the step that usually waits on a human. Make the agent able to do it, and you stop being the bottleneck. Skip it, and running more agents only gets you more unchecked work to review. @@ -58,7 +58,7 @@ The UI bullet above hides a real requirement. The agent needs a scripted way to [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) interviews the repository, not you. It works out what a user touches, how the app launches locally, what can drive it (an existing harness first, otherwise browser and CDP, a PTY, or plain HTTP), what evidence proves behavior, and whether two instances can run side by side. It asks you only what the code can't answer. -It writes `.cursor/skills/verify-/`, agent-facing instructions with exact Launch, Doctor, Drive, Evidence, and Cleanup sections, plus a feature map under `features/` that indexes what the app does and what result proves each feature works. The skill ships a [worked feature-map example](../../skills/create-verification-skill/references/feature-map-example/) with a README index and one file per feature using the four required H2s. Before handing it over, the generator proves the skill once end to end: launch, doctor check, drive one feature, capture evidence, clean up. If that proof fails, don't use the output. +It writes `.cursor/skills/verify-/`, agent-facing instructions with exact Launch, Doctor, Drive, Evidence, and Cleanup sections, a Helpers section for any script it ships, plus a feature map under `features/` that indexes what the app does and what result proves each feature works. The skill ships a [worked feature-map example](../../skills/create-verification-skill/references/feature-map-example/) with a README index and one file per feature using the four required H2s. Before handing it over, the generator proves the skill once end to end: launch, doctor check, drive one feature, capture evidence, clean up, then confirm the evidence survived the cleanup. If that proof fails, don't use the output. From then on, "verify it in the app" is a step any agent can execute, in this repo, with no setup conversation. Name it in the prompt when you want the proof in a specific form: @@ -93,6 +93,26 @@ Apps change, and feature maps go out of date. Run this at least once a day, idea [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) audits the generated skill: one read-only source reader per feature in parallel, then one live pass that drives every mapped feature. It ends in exactly one of three outcomes. `clean` means full coverage and nothing to ship. `changed` means one PR of proven corrections, confined to the verification skill's own directory. `blocked` names the blocker. It never edits product code. If the live pass catches a product regression, it reports the regression instead of hiding it with a doc edit. +## Prove a property with a formal verification skill + +A verification skill proves the paths you drive. Some bugs live on paths nobody drives: two retries that overlap, a lock that expires mid-write, a state change that arrives out of order. Tests rarely reach those cases. For code where such a bug is costly, run: + +```text +/create-formal-verification-skill +``` + +[`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md) picks the target from the code: a promise the code makes, where a break harms users and tests rarely reach the case that breaks it. It picks the strongest target, not the easiest to verify. Name an area or a bug to start there instead: + +```text +/create-formal-verification-skill the job lease and retry logic. a job must never run twice at once. +``` + +The question picks the tool. Whether events can happen in a bad order suits a model checker over a small model of the design. Whether the code behaves for every input suits a verifier that runs on the code. A property that must hold at every size can need a proof. The agent tells you which tool it chose and why. + +It verifies one property and shows that property failing on a broken variant of the code, because a check you've never seen fail proves nothing. When the current code already breaks the property, you get the counterexample as a short sequence of steps in your code's terms. The property stays as stated, so the finding stays a finding. Product code doesn't change unless you ask. + +It writes a project-local skill that tells the next agent whether a change touches the verified code, how to run the check with one command, and how to tell a real bug from a modeling error. Before handing it over, the generator follows that skill once on a scratch change that breaks the property, and the check must catch it. The handoff says what was verified, with which tool and bounds, what the check found, and what it doesn't cover. A pass covers the model or the bound, not the whole system. + ## Open the PR ```text @@ -109,7 +129,7 @@ An open PR starts collecting blockers immediately. Checks fail, reviewers commen /poteto-mode babysit this pr. get it green. ``` -Babysit watches the PR with a bundled watcher and takes blockers in order: conflicts, then review threads, then CI. Every known fix batches into one push, so the checks restart once instead of after every fix. The comment triage is skeptical, because humans and bots file real catches and noise in the same list. A real finding gets a fix, and noise gets dismissed with the disproof posted on the thread. When all you want is status, ask smaller and Babysit answers without starting the loop: +Babysit watches the PR, with a bundled watcher on GitHub or the Origin CLI when it's available, and takes blockers in order: conflicts, then review threads, then CI. Every known fix batches into one push, so the checks restart once instead of after every fix. The comment triage is skeptical, because humans and bots file real catches and noise in the same list. A real finding gets a fix, and noise gets dismissed with the disproof posted on the thread. When all you want is status, ask smaller and Babysit answers without starting the loop: ```text /poteto-mode check on pr 123. anything outstanding? diff --git a/pstack/docs/guide/07-overnight.md b/pstack/docs/guide/07-overnight.md index 625144b30..dd4230d8c 100644 --- a/pstack/docs/guide/07-overnight.md +++ b/pstack/docs/guide/07-overnight.md @@ -67,6 +67,8 @@ When you're back, ask for the run in review form: Before the skill hands back its summary, it spawns a reviewer on a different model family to read the trail and the transcript, and the reply ends with an Attention section listing what deserves your scrutiny. Read that section first, then the log rows it points at. You're auditing decisions, not re-reading the whole night. +For a quick status instead of an audit, run [`/ketchup`](../../skills/ketchup/SKILL.md) in the chat that ran the work. It reads only, and tells you in plain words what changed since your last message, with the screenshots and small diagrams the work produced. Then it lists each call waiting on you, such as a merge, an approval, or a choice between options, with its pick, the evidence, and the risk, so you can decide from the reply alone. + ## When the night holds a queue, not a task The contract above drives one task to one finish condition. Some nights hold more, a queue of independent changes or a whole program. Three playbooks scale the same trust up. diff --git a/pstack/docs/guide/09-make-it-yours.md b/pstack/docs/guide/09-make-it-yours.md index cb3c20188..457341aa4 100644 --- a/pstack/docs/guide/09-make-it-yours.md +++ b/pstack/docs/guide/09-make-it-yours.md @@ -59,7 +59,7 @@ When you already know the workflow you want to capture: Writing a skill matches the [Authoring or modifying a skill playbook](../../skills/poteto-mode/playbooks/authoring-a-skill.md), which routes through Cursor's built-in `create-skill`, validates the frontmatter and links, and ships the result through the Opening a PR playbook. Agent-facing prose has a higher bar than human prose, because an unhelpful sentence becomes an instruction some future agent follows. Let the playbook hold that bar rather than writing a `SKILL.md` freehand. -One special case has its own generator. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers both. +Two special cases have their own generators. A skill that must drive your app and prove behavior is a verification skill, so use [`/create-verification-skill`](../../skills/create-verification-skill/SKILL.md) and [`/maintain-verification-skill`](../../skills/maintain-verification-skill/SKILL.md) instead. A skill that checks a property of your code with a model checker, a proof, or another verifier is a formal verification skill, so use [`/create-formal-verification-skill`](../../skills/create-formal-verification-skill/SKILL.md). [Verify and ship](./06-verify-and-ship.md#create-a-project-verification-skill) covers both kinds. ## Write docs to a standard with `/technical-writing` diff --git a/pstack/docs/guide/10-recipes-and-pitfalls.md b/pstack/docs/guide/10-recipes-and-pitfalls.md index 6d2ef465c..fb4743c29 100644 --- a/pstack/docs/guide/10-recipes-and-pitfalls.md +++ b/pstack/docs/guide/10-recipes-and-pitfalls.md @@ -18,7 +18,15 @@ Mechanics first, history second. Each skill's report tells you which sources it /poteto-mode read this thread. restate the underlying issue in your own words, in plain english. don't change any code yet. ``` -A misreading shows up in the restatement, where it costs one message to correct. Keep your own theory to yourself until the agent has stated its own. +A misreading shows up in the restatement, where it costs one message to correct. Keep your own theory to yourself until the agent has stated its own. `/in-your-own-words` asks for the restatement alone, with no playbook. + +## Aim a task before it starts + +```text +/sharpen write the onboarding doc for the new billing service. +``` + +The agent asks how an expert would do the task, what you're really after, and whether the ask says too much or too little. It keeps one outside check that the result is right, then does the work. ## Prototype before you pick @@ -76,6 +84,14 @@ The qualifiers do real work. "don't change anything yet" keeps it read-only, and "if it repros on main" lets the run stop early when the bug is already gone. The video lets you check the fix before you read the diff. +## Prove a property tests rarely reach + +```text +/create-formal-verification-skill the retry queue. a message must never be delivered twice. +``` + +You get one property checked in every case within a stated scope, a counterexample in your code's terms if the code already breaks it, and a project skill the next agent runs on any change to that code. + ## Vet a number before you post it ```text @@ -134,6 +150,14 @@ You rarely need more words. You need the right name, and [the principles page](. That's the whole prompt. [`/bro`](../../skills/bro/SKILL.md) restates the last message like one human talking to another, no jargon, shorter. Use it when a reply is technically thorough and you still don't know what it said. +## Catch up on a chat you left running + +```text +/ketchup +``` + +[`/ketchup`](../../skills/ketchup/SKILL.md) tells you in plain words what changed since your last message, then lists each call waiting on you with its pick, evidence, and risk. It changes nothing while it reports. + ## The pitfalls - **Enumerating skills in the prompt.** "use /how then /architect then /arena" reorders steps the playbook already sequences. State the goal and constraints. Name a skill only to override a default. diff --git a/pstack/docs/guide/README.md b/pstack/docs/guide/README.md index 627bfb222..17422b992 100644 --- a/pstack/docs/guide/README.md +++ b/pstack/docs/guide/README.md @@ -9,7 +9,7 @@ Here's what you'll learn: 3. [Understand the code](./03-understand.md). A read-only investigation, then `/how`, `/why`, `/teach`, and `/recall` before you edit anything. 4. [Design the change](./04-design.md). `/architect`, `/arena`, `/swarm`, `/interrogate`, prototypes, and plans before code locks in a shape. 5. [Build and clean the change](./05-build-and-clean.md). The build playbooks, `/tdd`, `/unslop`, and `/no-comments`. -6. [Verify and ship](./06-verify-and-ship.md). Prove behavior on the real app, vet numbers with `/benchmark-checklist`, then open a focused PR and drive it to merged. +6. [Verify and ship](./06-verify-and-ship.md). Prove behavior on the real app, formally verify what tests rarely reach, vet numbers with `/benchmark-checklist`, then open a focused PR and drive it to merged. 7. [Run work while you sleep](./07-overnight.md). Trust before loops, an overnight contract, a decision log you can audit, and Projects and automations that scale past one agent. 8. [Steer with principle names](./08-principles.md). The 24 names that redirect an agent mid-task. 9. [Make it yours](./09-make-it-yours.md). Your own mode, `/correct` for repeated mistakes, and how to test a skill change. diff --git a/pstack/skills/poteto-help/SKILL.md b/pstack/skills/poteto-help/SKILL.md index 30f468927..7e834744b 100644 --- a/pstack/skills/poteto-help/SKILL.md +++ b/pstack/skills/poteto-help/SKILL.md @@ -26,6 +26,7 @@ Check the state that changes the answer, and mention it only when it does: - No `~/.cursor/rules/pstack-models.mdc` means `/setup-pstack` hasn't run for this user, so every role uses its default model. - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When the model rule is missing and it matters, ask whether the user wants to pick a model for each role and a reasoning budget now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -35,14 +36,16 @@ When the model rule is missing and it matters, ask whether the user wants to pic ## Get set up 1. Install with `/add-plugin pstack` in chat, or from Customize in the sidebar. -2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It asks for a reasoning budget, maps a model to each role, and writes a rule. The rule applies to new chats. +2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It asks for a reasoning budget, maps a model to each role, and writes a rule. The rule applies to new chats. Then it offers once each to generate a verification skill and a formal verification skill for the project, unless the project already has one. 3. Start a real task with `/poteto-mode`, a goal, and a check that can pass or fail. Installing changes nothing until the user invokes a skill. Only `/setup-pstack` loads from the user's words. The [README](../../README.md) and [guide page 1](../../docs/guide/01-setup.md) have the details. Offer to word their first prompt with them, per [`references/prompting.md`](references/prompting.md). If cost is the worry, say where the tokens go and how to spend fewer. pstack spends extra tokens on subagents and review panels. Rerun `/setup-pstack` and pick a smaller budget or cheaper models. A role set to `auto` or `inherit-parent` runs on the chat's model, which saves tokens when the chat runs on Auto or a cheaper model. A shorter panel list runs fewer subagents, one for each entry. Save `/poteto-mode` for work that needs rigor. -pstack is built for Cursor. Its skills use the Agent Skills format, so other tools can read them. But most workflow skills, including `/poteto-mode`, `/how`, `/why`, and `/teach`, spawn Cursor subagents with per-role models, and Custom Modes and `/loop` are Cursor features, so those parts may not work there. +pstack is built for Cursor, and it also installs in Claude Code with `/plugin marketplace add cursor/plugins`, then `/plugin install pstack@cursor-plugins`. There, each command takes a `pstack:` prefix, such as `/pstack:poteto-mode`. The [Claude Code adapter](../../docs/harness/claude-code.md) maps the Cursor names, and a step that needs a Cursor-only feature, such as Bugbot or Automations, is skipped with a one-line note. + +Other tools can read the skills, because they use the Agent Skills format. But most workflow skills, including `/poteto-mode`, `/how`, `/why`, and `/teach`, spawn Cursor subagents with per-role models, and Custom Modes and `/loop` are Cursor features, so those parts may not work there. ## Start a task with `/poteto-mode` diff --git a/pstack/skills/poteto-help/references/recipes.md b/pstack/skills/poteto-help/references/recipes.md index d13da3a08..2d785761d 100644 --- a/pstack/skills/poteto-help/references/recipes.md +++ b/pstack/skills/poteto-help/references/recipes.md @@ -34,6 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too. +- `/create-formal-verification-skill prove holds in , even when interleave or retry.` - `/swarm check every package under against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr . anything outstanding?` @@ -43,6 +44,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/poteto-mode im going to bed. in a fresh worktree off . done means . keep a decision log. don't ask me before committing. /loop until done. if you're truly stuck after a few hours, stop and write up why.` - `/show-me-your-work catch me up on what you did last night.` Read its Attention section first. +- `/ketchup` catches you up on this chat since your last message and lists every call that waits on you. - `/poteto-mode full autopilot on this queue. each item is independent.` - `/poteto-mode autopilot these changes but stack them, don't ship. i'll land the stack.` - `/reflect capture what we learned so the next run doesn't repeat it.` Approve only edits that change a future decision. diff --git a/pstack/skills/setup-pstack/SKILL.md b/pstack/skills/setup-pstack/SKILL.md index 90a9e5753..cb61b8d3e 100644 --- a/pstack/skills/setup-pstack/SKILL.md +++ b/pstack/skills/setup-pstack/SKILL.md @@ -72,3 +72,7 @@ Tell the user the rule was written and that it applies to new sessions. Re-runni ### 7. Offer a verification skill (optional) Check whether the project has a way to drive the real app for proof (a `verify-*` skill, or an existing harness). If not, offer once: "want a project-local verification skill, so agents can drive the app the way a user does and prove changes work? I can generate one with /create-verification-skill." On yes, invoke `/create-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. + +### 8. Offer a formal verification skill (optional) + +Check whether the project already has a formal verification skill (a project skill that runs a model checker, a proof, or another verifier against the code). If not, offer once: "want a formal verification skill, so agents can prove a key property of your code holds in every case in scope, not only the cases tests reach? I can generate one with /create-formal-verification-skill." On yes, invoke `/create-formal-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing.