fix(pstack): add TLA+ default and no-verifier fallback to create-formal-verification-skill

[poteto]

Why

create-formal-verification-skill gave no fallback for a language with no formal verifier. In a preregistered eval on a JavaScript library with no verifier, 6 of 9 runs with the old paragraph proved their claim only on a hand-written copy of the function. With the new paragraph, all 9 runs checked the shipped code.

What changed

• The event-order sentence now makes TLA+ the default for that question in any language. The old sentence that recommended TLA+ for concurrent and distributed designs is gone.
• When no verifier runs on the language, a new sentence tells the agent to say so and to test the real code with generated inputs, not a hand model of the function.
• generate-pstack-harness-trees.mjs regenerated the claude-code harness copy.

Scope

• The new paragraph is byte for byte the text that the eval tested. The eval tested the two changes together, not one at a time, and without the edits in pstack: add maintain-formal-verification-skill #716. The pstack version does not change.
• pstack: add maintain-formal-verification-skill #716 edits other paragraphs of this skill and its harness copy. The two branches merge with no conflict.
• The user guide summarizes this paragraph and does not mention the TLA+ default or the fallback. A follow-up can add them after pstack: add maintain-formal-verification-skill #716, which also edits that guide page.

Blast Radius

Every run of /create-formal-verification-skill now defaults to TLA+ for event-order questions, and tests the real code with generated inputs when no verifier runs on the language. The eval found no regression on a Java connection pool or a C parser.

Verification

• The eval ran Claude, GPT, and Gemini on five open-source repos, with at most 3 runs per model and repo for each paragraph. One blind judge model gave each run one pass for each of four criteria that the run met. In both scoring views, both changes met their preregistered gates, with no regression and no harm on the other repos. Pooled, the new paragraph scores 3.62 passes per run against about 3.2, and it also ranks higher for Claude and for Gemini. About half of the pooled gain is in honest statements of what the check covers, which neither change mentions. Outside the JavaScript library, the old paragraph already met the target criteria in almost every run, so the eval cannot show a gain for the TLA+ change.
• The open item is that the two scoring views disagree on whether GPT ranks the new paragraph above the old. Both views put GPT near a tie. The primary view gives the new paragraph 3.78 passes per run against 3.75, and the sensitivity view gives the new paragraph 3.67 against 3.79. The sensitivity view also scores finished runs that the preregistered rule excluded only for a failed gh call or for seeing the name of an empty sandbox folder. The difference comes from three GPT runs with the new paragraph that only the sensitivity view scores. Two of them listed worker threads, which the JavaScript circuit breaker that they checked does not have, and the eval found no link from that text to the new wording. The primary view also has no scored GPT run on the C parser.
• node scripts/validate-plugins.mjs, node scripts/generate-pstack-harness-trees.mjs --check, and node scripts/check-pstack-docs.mjs pass.

  

---

Note

Low Risk
Documentation-only change to agent skill guidance; no runtime or product code paths.

^{Reviewed by Cursor Bugbot for commit 5bd8f4a. Bugbot is set up for automated code reviews on this repo. Configure here.}