CtrlK
BlogDocsLog inGet started
Tessl Logo
SkillPublic

create-formal-verification-skill

Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits. Use for /create-formal-verification-skill, "model-check this race", "prove this invariant", or when concurrency, retries, state machines, parsers, or unsafe code need more than tests.

Quality

91%

Does it follow best practices?

Run evals on this skill

Adds up to 20 points to the overall score

View guide
SecuritybySnyk

Passed

No findings from the security scan

SKILL.md
Quality
Evals
Security

Quality

Content

85%Weight 40%Scale 1-5

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

A lean, well-sequenced process skill: every section gives concrete, judgment-bearing directives, the prove-before-handoff step provides genuine validation with feedback loops, and external detail is properly deferred to clearly-labeled one-level-deep references. The only weaknesses are a brief known-concept explanation in the opening paragraph and the lack of a structural template for the generated skill, both minor.

DimensionReasoningScore

Conciseness

The body is dense and directive — "Show each property failing on a broken variant of the code it guards", "Use this repo's real commands, paths, and nouns, and leave no placeholders" — with almost no padding. However, the opening spends two sentences explaining the tests-vs-verification concept ("A test checks the cases that someone thought to write. Formal verification checks every case in a stated scope: every order of steps in a model, every input up to a bound, or every input") that Claude already knows, which is a minor instance of trimmable over-explanation; this fits anchor 4 rather than the every-token-earns-its-place anchor 5.

4 / 5

Actionability

Concrete, executable directives throughout: tool-selection rules ("Whether events can happen in a bad order usually suits a model checker… TLA+ is the default for that in any language"; "If no verifier runs on this language… test the real code with generated inputs, not a hand model of the function"), a seven-item quality checklist, and a concrete validation procedure ("Follow the generated skill once… on a scratch change that breaks the property in the real code"). The minor gap keeping it below anchor 5 is that no skeleton or example frontmatter for the generated skill is provided, leaving its structure to be invented; per the scoring note, the absence of code in an instruction-only skill is not penalized since the guidance is actionable.

4 / 5

Workflow Clarity

The sections are sequenced in execution order (choose target → choose tool → generate → prove → hand off) with an explicit validation step and feedback loop — "If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change" — a post-validation checkpoint ("confirm that the check is back where it started: passing, or failing only on the findings you will report"), and a checklist ("What makes it good"). This matches the anchor-5 pattern of clear sequence, explicit validation, and error-recovery loops; anchor 4 would require missing checkpoints, which are all present.

5 / 5

Progressive Disclosure

The body is under 50 lines with well-organized sections and no bundle files, which per the rubric's simple-skill note can score 5 on organization alone. Its two external references are one level deep, clearly signaled with purpose and read-timing ("read [the Claude Code adapter]… once per session"; "read every result with the pstack /statechart skill… It shows each invariant violation the checker finds as its shortest path in plain words"), and it explicitly delegates volatile details ("Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts").

5 / 5

Total

18

/

20

Passed

Description

95%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

A strong description: it states a concrete, well-scoped capability in third-person imperative voice and pairs it with an explicit "Use for…" trigger clause containing quoted user phrases and natural domain keywords. The only limitation is that it describes one composite action rather than enumerating several distinct capabilities, which keeps specificity just below the top anchor.

DimensionReasoningScore

Specificity

Explicitly states two heavily-qualified concrete actions — "Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits" — with concrete scope (any language, tool-agnostic, cost/coverage targeting) and capability phrases "model-check this race" / "prove this invariant". This is noticeably above the anchor-3 example ('Processes PDF files and extracts content') in precision, but it does not list the several distinct actions of an anchor-5 description, so 4 fits best.

4 / 5

Completeness

Clearly answers "what" ("Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits") and "when" with an explicit "Use for…" clause containing concrete trigger phrases, exactly matching the anchor-5 example pattern. Neither the what nor the when could be more explicit.

5 / 5

Trigger Term Quality

Includes quoted literal user utterances — "model-check this race", "prove this invariant", "/create-formal-verification-skill" — plus natural domain nouns ("concurrency, retries, state machines, parsers, or unsafe code") and the phrase "need more than tests", giving comprehensive coverage of what a user with this need would actually say. It clearly matches the comprehensive/synonym anchor rather than the 'a few natural terms missing' anchor below it.

5 / 5

Distinctiveness Conflict Risk

It occupies a clear niche — generating a project-local formal-verification skill — with distinct triggers ("model-check this race", "prove this invariant", "/create-formal-verification-skill") and the qualifier "need more than tests" separating it from ordinary testing skills, so conflict risk is minimal. It is not merely 'mostly distinct' as at anchor 4; no closely related skill would capture these triggers.

5 / 5

Total

19

/

20

Passed

Validation

93%

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 15 / 16 Passed

Validation for skill structure

CriteriaDescriptionResult

relative_links

Relative link issues: 2 suspicious

Warning

Total

15

/

16

Passed

Repository

cursor/plugins

Path

harness/pstack/claude-code/skills/create-formal-verification-skill/SKILL.md

Reviewed

Table of Contents

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.