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/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/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/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.
 
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"