From 8359b8b64a067ae9068f836b0293817cb8a4ca22 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 19 Oct 2026 05:09:11 +0000 Subject: [PATCH 1/2] docs(pstack): match guide page 6 to create-formal-verification-skill's tool choice #721 made TLA+ the default for event-order questions in any language, and added a fallback: when no verifier runs on the language, the agent says so and tests the real code with generated inputs. The guide's tool-choice paragraph still described the old wording. Claude Code harness copy regenerated. Co-authored-by: lauren --- harness/pstack/claude-code/docs/guide/06-verify-and-ship.md | 2 +- pstack/docs/guide/06-verify-and-ship.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 711b5a92a..3c7b3c4dd 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 @@ -107,7 +107,7 @@ A verification skill proves the paths you drive. Some bugs live on paths nobody /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. +The question picks the tool. Whether events can happen in a bad order suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code behaves for every input suits a verifier that runs on the code. If no verifier runs on your language, the agent says so and tests the real code with generated inputs, not a hand-written model of the function. 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. diff --git a/pstack/docs/guide/06-verify-and-ship.md b/pstack/docs/guide/06-verify-and-ship.md index 711b5a92a..3c7b3c4dd 100644 --- a/pstack/docs/guide/06-verify-and-ship.md +++ b/pstack/docs/guide/06-verify-and-ship.md @@ -107,7 +107,7 @@ A verification skill proves the paths you drive. Some bugs live on paths nobody /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. +The question picks the tool. Whether events can happen in a bad order suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code behaves for every input suits a verifier that runs on the code. If no verifier runs on your language, the agent says so and tests the real code with generated inputs, not a hand-written model of the function. 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. From b2a3fd3ebb23846e1c02daf55357254db984be19 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 19 Oct 2026 05:09:11 +0000 Subject: [PATCH 2/2] chore(pstack): bump to 0.15.28 Co-authored-by: lauren --- harness/pstack/claude-code/.claude-plugin/plugin.json | 2 +- harness/pstack/claude-code/plugin.json | 2 +- pstack/.cursor-plugin/plugin.json | 2 +- pstack/plugin.json | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/harness/pstack/claude-code/.claude-plugin/plugin.json b/harness/pstack/claude-code/.claude-plugin/plugin.json index dc9927da8..333c73942 100644 --- a/harness/pstack/claude-code/.claude-plugin/plugin.json +++ b/harness/pstack/claude-code/.claude-plugin/plugin.json @@ -1,7 +1,7 @@ { "$schema": "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json", "name": "pstack", - "version": "0.15.27", + "version": "0.15.28", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.", "author": { "name": "Lauren Tan" diff --git a/harness/pstack/claude-code/plugin.json b/harness/pstack/claude-code/plugin.json index dc9927da8..333c73942 100644 --- a/harness/pstack/claude-code/plugin.json +++ b/harness/pstack/claude-code/plugin.json @@ -1,7 +1,7 @@ { "$schema": "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json", "name": "pstack", - "version": "0.15.27", + "version": "0.15.28", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.", "author": { "name": "Lauren Tan" diff --git a/pstack/.cursor-plugin/plugin.json b/pstack/.cursor-plugin/plugin.json index 1b0f0e4d2..7754f381a 100644 --- a/pstack/.cursor-plugin/plugin.json +++ b/pstack/.cursor-plugin/plugin.json @@ -1,7 +1,7 @@ { "name": "pstack", "displayName": "pstack", - "version": "0.15.27", + "version": "0.15.28", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.", "author": { "name": "Lauren Tan" diff --git a/pstack/plugin.json b/pstack/plugin.json index dc9927da8..333c73942 100644 --- a/pstack/plugin.json +++ b/pstack/plugin.json @@ -1,7 +1,7 @@ { "$schema": "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json", "name": "pstack", - "version": "0.15.27", + "version": "0.15.28", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.", "author": { "name": "Lauren Tan"