program-to-tlaplus-spec-generator
Automatically generate TLA+ specifications from program code, repositories, or system implementations. Use when asked to generate TLA+ spec, create TLA+ specification from code, convert program to TLA+, formalize system in TLA+, extract TLA+ model from code, or when working with formal specification of concurrent systems, distributed systems, protocols, algorithms, or state machines that need to be verified.
Install with Tessl CLI
npx tessl i github:ArabelaTso/Skills-4-SE --skill program-to-tlaplus-spec-generator88
Does it follow best practices?
If you maintain this skill, you can automatically optimize it using the tessl CLI to improve its score:
npx tessl skill review --optimize ./path/to/skillValidation for skill structure
Discovery
100%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 is an excellent skill description that hits all the key criteria. It provides specific capabilities, comprehensive trigger terms that users would naturally use, explicit 'Use when...' guidance, and a clear distinctive niche around TLA+ formal specification generation. The description is well-structured and appropriately detailed without being verbose.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple concrete actions: 'generate TLA+ specifications from program code, repositories, or system implementations' and specifies domains like 'concurrent systems, distributed systems, protocols, algorithms, or state machines'. | 3 / 3 |
Completeness | Clearly answers both what ('Automatically generate TLA+ specifications from program code, repositories, or system implementations') and when with explicit 'Use when...' clause containing multiple trigger scenarios. | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural trigger terms users would say: 'generate TLA+ spec', 'create TLA+ specification from code', 'convert program to TLA+', 'formalize system in TLA+', 'extract TLA+ model from code', plus domain terms like 'concurrent systems', 'distributed systems', 'protocols'. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive with clear niche around TLA+ formal specification. The specific technology (TLA+) and use cases (formal verification of concurrent/distributed systems) make it unlikely to conflict with other skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
70%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This skill provides a well-structured workflow for generating TLA+ specifications from code, with clear sequential steps and good progressive disclosure through external references. However, it could be more concise by removing explanations of concepts Claude already knows, and more actionable by including complete, executable TLA+ examples rather than templates and abstract descriptions.
Suggestions
Replace the skeleton TLA+ module template with a complete, working example showing a real transformation (e.g., a simple counter program to TLA+ spec)
Remove explanatory content Claude already knows, such as definitions of safety vs liveness properties and basic concurrent/distributed system characteristics
Add a concrete before/after example showing actual source code and its corresponding complete TLA+ specification
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The skill is reasonably efficient but includes some unnecessary explanation that Claude would already know (e.g., explaining what safety vs liveness properties are, basic definitions of concurrent vs distributed systems). Some sections could be tightened. | 2 / 3 |
Actionability | Provides good structural guidance and templates, but the TLA+ code examples are mostly skeleton/template code rather than complete executable examples. The patterns section describes approaches abstractly rather than showing concrete transformations. | 2 / 3 |
Workflow Clarity | Excellent sequential workflow with 9 clearly numbered steps. Each step has clear outputs and the process flows logically from analysis through generation. The workflow is well-structured for a complex multi-step task. | 3 / 3 |
Progressive Disclosure | Good structure with clear overview, detailed workflow, and appropriate references to external files (tlaplus_syntax.md, language_patterns.md) for detailed content. Content is well-organized with clear section headers. | 3 / 3 |
Total | 10 / 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.