tlaplus-model-reduction
Reduces a TLA+ model so TLC can actually check it — shrinks constants, adds state constraints, abstracts data, or applies symmetry — when the state space is too large to enumerate. Use when TLC runs out of memory, when checking takes hours, or when a spec works at N=2 and you need confidence at larger scale.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill tlaplus-model-reduction100
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 clearly articulates specific techniques for TLA+ model reduction, includes natural trigger terms covering both tool names and user-described symptoms, and explicitly states when to use the skill. The description is concise yet comprehensive, targeting a distinct niche with minimal conflict risk.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'shrinks constants, adds state constraints, abstracts data, or applies symmetry'. These are precise, actionable techniques for TLA+ model reduction. | 3 / 3 |
Completeness | Clearly answers both what ('Reduces a TLA+ model... shrinks constants, adds state constraints, abstracts data, or applies symmetry') and when ('Use when TLC runs out of memory, when checking takes hours, or when a spec works at N=2 and you need confidence at larger scale'). | 3 / 3 |
Trigger Term Quality | Includes natural terms users would say: 'TLA+', 'TLC', 'state space', 'runs out of memory', 'checking takes hours', 'N=2'. These cover both tool names and problem symptoms users would describe. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive with clear niche in TLA+/TLC model checking. The specific domain (formal verification), tool names, and problem triggers make conflicts with other skills extremely unlikely. | 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.
Excellent skill content that demonstrates expert-level understanding of TLA+ model reduction. It's concise yet comprehensive, with concrete code examples, a diagnostic framework, and explicit soundness warnings. The worked example grounds abstract techniques in practical application, and the output format ensures Claude reports reductions transparently.
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | Every section earns its place. No explanation of what TLC is or how model checking works—assumes Claude knows TLA+. The diagnostic table, technique list, and worked example are dense with actionable information without padding. | 3 / 3 |
Actionability | Provides concrete, copy-paste ready TLA+ and .cfg snippets for every technique. The worked example shows exact before/after configurations with real numbers. The diagnostic table maps symptoms directly to fixes. | 3 / 3 |
Workflow Clarity | Clear sequence: diagnose first (with specific coverage flags), then apply techniques cheapest-first, with explicit validation via the output format. The 'Do not' section provides guardrails, and soundness caveats force explicit acknowledgment of limitations. | 3 / 3 |
Progressive Disclosure | Well-structured with clear sections progressing from diagnosis → techniques → worked example → edge cases → output format. No external file references needed for this self-contained skill; content is appropriately organized within a single document. | 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.