From 28767f85a731c044fee7ff3fdde00040ee326de3 Mon Sep 17 00:00:00 2001 From: "Lauren (agent)" Date: Thu, 22 Oct 2026 16:18:47 +0000 Subject: [PATCH 1/2] feat(pstack): tell generated verify skills to read each model-check result with /statechart --- .../skills/create-formal-verification-skill/SKILL.md | 2 ++ pstack/skills/create-formal-verification-skill/SKILL.md | 2 ++ 2 files changed, 4 insertions(+) diff --git a/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md b/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md index fe72da6d8..5791e36c1 100644 --- a/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md +++ b/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md @@ -34,6 +34,8 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. +If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each bug the checker finds as its shortest path in plain words, and which of those bugs a change fixes. When the check passes, `/statechart` draws a chart of what the user sees. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. + ## Prove it before you hand off Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change. diff --git a/pstack/skills/create-formal-verification-skill/SKILL.md b/pstack/skills/create-formal-verification-skill/SKILL.md index b97609fd2..cffd87609 100644 --- a/pstack/skills/create-formal-verification-skill/SKILL.md +++ b/pstack/skills/create-formal-verification-skill/SKILL.md @@ -32,6 +32,8 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. +If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each bug the checker finds as its shortest path in plain words, and which of those bugs a change fixes. When the check passes, `/statechart` draws a chart of what the user sees. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. + ## Prove it before you hand off Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change. From 4f6fba8d3a6025ac7f5d7a1886ff02ed7ba13a34 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 23 Oct 2026 19:48:54 +0000 Subject: [PATCH 2/2] fix(pstack): match the /statechart paragraph to what statechart does now Statechart draws how any system moves between states, not only what a user sees, and it draws no path for a broken PROPERTY. Co-authored-by: lauren --- .../skills/create-formal-verification-skill/SKILL.md | 2 +- pstack/skills/create-formal-verification-skill/SKILL.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md b/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md index 5791e36c1..a37e735e8 100644 --- a/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md +++ b/harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md @@ -34,7 +34,7 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. -If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each bug the checker finds as its shortest path in plain words, and which of those bugs a change fixes. When the check passes, `/statechart` draws a chart of what the user sees. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. +If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each invariant violation the checker finds as its shortest path in plain words, and which of those violations a change fixes. When the check passes, `/statechart` draws a chart of how the system moves between states. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. ## Prove it before you hand off diff --git a/pstack/skills/create-formal-verification-skill/SKILL.md b/pstack/skills/create-formal-verification-skill/SKILL.md index cffd87609..37d73f904 100644 --- a/pstack/skills/create-formal-verification-skill/SKILL.md +++ b/pstack/skills/create-formal-verification-skill/SKILL.md @@ -32,7 +32,7 @@ Pick the tool that answers the question at the lowest cost: a model checker, a p Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. -If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each bug the checker finds as its shortest path in plain words, and which of those bugs a change fixes. When the check passes, `/statechart` draws a chart of what the user sees. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. +If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each invariant violation the checker finds as its shortest path in plain words, and which of those violations a change fixes. When the check passes, `/statechart` draws a chart of how the system moves between states. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. ## Prove it before you hand off