formal-spec-generator
Dispatch skill — routes a formal specification request to the right concrete generator based on what's being specified and what needs to be proven. Use when the user asks to formally specify something without naming a target formalism, or when unsure which verification tool fits the problem.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill formal-spec-generator90
Quality
87%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
Discovery
75%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This description has good structure with an explicit 'Use when' clause that clearly defines trigger conditions, earning high marks for completeness and distinctiveness. However, it relies on technical jargon that users may not naturally use, and lacks concrete examples of the specific generators or formalisms it can route to, limiting its specificity and trigger term quality.
Suggestions
Add natural trigger terms users might say, such as 'prove correctness', 'verify my code', 'formal proof', 'TLA+', 'Coq', 'Alloy', or 'model checking'
List specific concrete generators or formalisms this skill can route to (e.g., 'Routes to TLA+, Coq, Alloy, or Z3 generators based on the verification need')
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Names the domain (formal specification routing) and describes the action (routes requests to generators), but lacks concrete examples of what generators or formalisms are available. 'Dispatch skill' and 'routes' are somewhat abstract. | 2 / 3 |
Completeness | Clearly answers both what (routes formal specification requests to the right generator) AND when (explicit 'Use when' clause covering two scenarios: user asks to formally specify without naming a target, or when unsure which verification tool fits). | 3 / 3 |
Trigger Term Quality | Includes some relevant terms like 'formally specify', 'verification tool', and 'formalism', but these are technical jargon. Missing natural user phrases like 'prove correctness', 'verify code', 'formal methods', or specific tool names users might mention. | 2 / 3 |
Distinctiveness Conflict Risk | The niche of formal specification routing is quite distinct. Terms like 'formal specification', 'formalism', and 'verification tool' create a clear, narrow domain unlikely to conflict with general coding or documentation skills. | 3 / 3 |
Total | 10 / 12 Passed |
Implementation
100%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is an exemplary dispatch skill that efficiently routes users to the correct formal verification tool. The content is maximally dense with zero wasted tokens, using tables and decision trees to compress complex routing logic. The 'common misroutings' and 'do not' sections add high value by preventing predictable errors.
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | Extremely lean and efficient. Every section serves a clear purpose with no padding or explanation of concepts Claude already knows. The dispatch table format maximizes information density. | 3 / 3 |
Actionability | Provides concrete routing decisions with specific skill names to invoke. The three routing questions give executable decision logic, and the common misroutings table prevents specific errors with clear corrections. | 3 / 3 |
Workflow Clarity | For a dispatch skill, the workflow is crystal clear: answer three questions, consult the table, route to the appropriate generator. The decision tree structure makes the sequence unambiguous. | 3 / 3 |
Progressive Disclosure | Perfect structure for a dispatch skill: quick reference table up front, decision heuristics in the middle, anti-patterns at the end. References to other skills are one level deep and clearly named. | 3 / 3 |
Total | 12 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- 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.