program-to-tlaplus-spec-generator
Extracts a TLA+ specification from concurrent or distributed code, modeling the state machine, actions, and fairness conditions for model checking with TLC. Use when verifying concurrency properties of production code, when designing a protocol and wanting to check it before implementation, or when the user has a race condition and needs to prove the fix.
Install with Tessl CLI
npx tessl i github:santosomar/general-secure-coding-agent-skills --skill program-to-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 capability for TLA+ formal verification. It provides specific actions, comprehensive trigger terms covering the formal methods domain, and explicit 'Use when' guidance with three concrete scenarios. The technical specificity ensures it won't conflict with other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Extracts a TLA+ specification', 'modeling the state machine, actions, and fairness conditions', 'model checking with TLC'. These are precise, technical operations. | 3 / 3 |
Completeness | Clearly answers both what (extracts TLA+ specs, models state machines/actions/fairness for TLC) AND when with explicit 'Use when' clause covering three distinct scenarios: verifying concurrency, designing protocols, and debugging race conditions. | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'TLA+', 'concurrent', 'distributed code', 'model checking', 'TLC', 'concurrency properties', 'protocol', 'race condition'. Good coverage of domain-specific terms users would naturally use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting TLA+ formal verification specifically. Terms like 'TLA+', 'TLC', 'fairness conditions', and 'model checking' are unique to this domain and 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 an excellent skill that efficiently teaches TLA+ specification extraction through concrete examples and clear workflows. The worked example with buggy Go code translated to TLA+ is particularly effective. Minor improvement possible in progressive disclosure by better organizing references to related skills/documentation.
Suggestions
Add explicit links to related skills (e.g., make 'tlaplus-model-reduction' a proper markdown link to the referenced skill file)
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | Every section earns its place. No explanation of what TLA+ is or basic concepts Claude knows. The tables, examples, and do-not lists are dense with actionable information without padding. | 3 / 3 |
Actionability | Provides complete, executable TLA+ code with a worked example showing real Go code translated to a full TLA+ module. The output format template and step-by-step process are copy-paste ready. | 3 / 3 |
Workflow Clarity | Clear 3-step process (identify state → identify actions → write actions) with explicit guidance on atomicity boundaries. The 'Do not' section serves as validation checkpoints, and the sanity-check advice about verifying the model terminates is a feedback loop. | 3 / 3 |
Progressive Disclosure | Content is well-organized with clear sections and tables, but it's a single monolithic file. The reference to 'tlaplus-model-reduction' suggests related skills exist but could be better signaled with explicit links to related documentation. | 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.