requirement-to-tlaplus-property-generator
Translates natural-language requirements into TLA+ properties — invariants for safety, temporal formulas for liveness — checkable with TLC. Use when writing the PROPERTY and INVARIANT sections of a TLA+ spec, when formalizing acceptance criteria, or when the user has a requirement and a model but no property.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill requirement-to-tlaplus-property-generator100
Quality
100%
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 follows best practices. It uses third person voice, provides specific concrete actions within the TLA+ formal methods domain, includes an explicit 'Use when...' clause with multiple trigger scenarios, and has highly distinctive terminology that minimizes conflict risk with other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Translates natural-language requirements into TLA+ properties', 'invariants for safety', 'temporal formulas for liveness', 'checkable with TLC'. These are precise, domain-specific capabilities. | 3 / 3 |
Completeness | Clearly answers both what ('Translates natural-language requirements into TLA+ properties') and when ('Use when writing the PROPERTY and INVARIANT sections', 'when formalizing acceptance criteria', 'when the user has a requirement and a model but no property'). Explicit 'Use when...' clause with multiple trigger scenarios. | 3 / 3 |
Trigger Term Quality | Includes strong natural keywords users would say: 'TLA+', 'properties', 'invariants', 'safety', 'liveness', 'TLC', 'PROPERTY', 'INVARIANT', 'acceptance criteria', 'requirement', 'model'. Good coverage of domain terminology. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting TLA+ formal specification properties specifically. The combination of 'TLA+', 'TLC', 'PROPERTY', 'INVARIANT', 'temporal formulas' creates a clear, non-overlapping domain unlikely to conflict with other skills. | 3 / 3 |
Total | 12 / 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 excellent skill that efficiently translates natural language requirements into TLA+ properties. It provides concrete patterns, executable code, a thorough worked example, and explicit anti-patterns—all without wasting tokens on concepts Claude already knows. The structured output format ensures consistent, verifiable results.
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is lean and efficient, assuming Claude understands TLA+ fundamentals. Every section adds value—classification tables, pattern catalogs, and worked examples are all actionable without explaining what TLA+ is or how model checking works. | 3 / 3 |
Actionability | Provides concrete, executable TLA+ code throughout—pattern catalog maps English directly to TLA+ syntax, worked example shows complete property definitions, and the history variable trick for precedence is copy-paste ready. | 3 / 3 |
Workflow Clarity | Clear two-step process (classify → find state predicate) with explicit decision criteria. The 'Do not' section serves as validation checkpoints, and the output format provides a structured checklist including sanity checks. | 3 / 3 |
Progressive Disclosure | Well-organized with clear sections progressing from classification to patterns to worked example to pitfalls. At ~100 lines, the content is appropriately self-contained without needing external references, and sections are clearly delineated. | 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.