tlaplus-spec-generator
Translates natural-language or pseudocode descriptions of concurrent and distributed systems into TLA+ specifications ready for the TLC model checker. Identifies state variables, actions, type invariants, safety properties, and liveness properties from the description. Use when formalizing a protocol, when the user describes a distributed algorithm to verify, when designing a consensus or locking scheme, or when starting formal verification of a concurrent system.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill tlaplus-spec-generator97
Quality
96%
Does it follow best practices?
Impact
Pending
No eval scenarios have been run
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 clearly defines a specialized niche in formal verification with TLA+. It provides specific capabilities (translating descriptions, identifying formal specification components), uses appropriate domain terminology that users would naturally employ, and includes a comprehensive 'Use when' clause with multiple trigger scenarios. The description is well-structured, uses proper third-person voice, and would effectively distinguish this skill from others in a large skill library.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Translates natural-language or pseudocode descriptions', 'Identifies state variables, actions, type invariants, safety properties, and liveness properties'. These are precise, actionable capabilities. | 3 / 3 |
Completeness | Clearly answers both what ('Translates...into TLA+ specifications', 'Identifies state variables...') AND when with explicit 'Use when' clause covering four distinct trigger scenarios: formalizing protocols, verifying distributed algorithms, designing consensus/locking schemes, and starting formal verification. | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'TLA+', 'distributed systems', 'concurrent systems', 'protocol', 'distributed algorithm', 'consensus', 'locking scheme', 'formal verification', 'model checker'. Good coverage of domain terminology. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting TLA+ and formal verification of concurrent/distributed systems. The specific mention of TLC model checker, type invariants, safety/liveness properties creates clear boundaries unlikely to conflict with general coding or documentation skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
92%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a high-quality skill that provides excellent actionable guidance for translating system descriptions into TLA+ specifications. The step-by-step workflow is clear, the worked example is complete and instructive, and the edge cases section addresses real-world complications. The only weakness is the document length could benefit from progressive disclosure to separate reference material.
Suggestions
Consider moving the 'Edge cases' section to a separate EDGE_CASES.md file and linking to it, reducing the main skill's token footprint
The worked example could be extracted to EXAMPLES.md with additional examples for different system types (message-passing, consensus, etc.)
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is lean and efficient, assuming Claude's competence with TLA+ syntax and focusing on decision-making guidance. Every section earns its place with actionable insights rather than explaining basic concepts Claude would already know. | 3 / 3 |
Actionability | Provides fully executable TLA+ code with complete module and .cfg file examples. The worked example is copy-paste ready, and the extraction tables give concrete patterns for translating prose to spec components. | 3 / 3 |
Workflow Clarity | Clear 5-step sequence from deciding if TLA+ is appropriate through assembling the module. Each step has explicit criteria and the final 'Do not' section includes validation guidance ('Don't hand over a spec you haven't run through TLC once'). | 3 / 3 |
Progressive Disclosure | Content is well-organized with clear sections, but it's a monolithic document (~200 lines) that could benefit from splitting edge cases or the worked example into separate files. References to other skills (cpp-to-dafny-translator, etc.) are good but inline content is heavy. | 2 / 3 |
Total | 11 / 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.