New: 98,000+ skills indexed from GitHub repos with 100+ stars · every skill safety-checkedBrowse top skillsTop skills
Esc to closeBrowse all skills
Submit a skillBrowse skills
Submit a skillBrowse skills

Agent skill

Requirement To Tlaplus Property Generator

by ArabelaTso in ArabelaTso/Skills-4-SE

Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents.

Apache-2.0Auto-check passedAgent Workflows

Install Requirement To Tlaplus Property Generator

skills CLI
$ npx skills add ArabelaTso/Skills-4-SE --skill requirement-to-tlaplus-property-generator -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI
$ gh skill install ArabelaTso/Skills-4-SE requirement-to-tlaplus-property-generator --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy
$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .claude/skills && cp -r skills-src/skills/requirement-to-tlaplus-property-generator .claude/skills/requirement-to-tlaplus-property-generator && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Facts

Skill name
requirement-to-tlaplus-property-generator
GitHub stars
253
Token cost
~1.9k tokens
SKILL.md length
654 words
Files
4 (incl. references)
Skills in repo
170
Repo updated
First seen
Licence
Apache-2.0

At a glance

Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents.

  • Works in 5 steps: Analyze the Requirement → Resolve Ambiguities → Map to TLA+ Constructs → …
  • Translating system requirements
  • SKILL.md covers Overview, Workflow, Common Requirement Patterns and Handling Complex Requirements, plus 4 more sections
  • Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Requirement To Tlaplus Property Generator is an agent skill from ArabelaTso/Skills-4-SE. Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents. Resolves ambiguities, asks clarifying questions for underspecified requirements, and outputs TLA+-compatible property definitions with semantic explanations. Use when translating system requirements, specifications, or behavioral constraints into formal TLA+ temporal logic properties for verification with TLC model checker.

Its SKILL.md is about 1.9k tokens, which your agent loads only when the skill is triggered. The skill folder holds 4 other files, including reference files (for example `references/clarification_patterns.md`, `references/requirement_patterns.md` and `references/tlaplus_syntax.md`).

It sits in Agent Workflows, covering Requirements gathering and Translation. The repository describes itself as: A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows. The licence is Apache-2.0.

When your agent uses it

  • Translating system requirements
  • Behavioral constraints into formal TLA+ temporal logic properties for verification with TLC model checker

Example prompts

  • “/requirement-to-tlaplus-property-generator”

Workflow steps

5 steps, taken from the step headings in SKILL.md.

  1. Analyze the Requirement
  2. Resolve Ambiguities
  3. Map to TLA+ Constructs
  4. Generate TLA+ Property Definition
  5. Provide Semantic Explanation

What it can do on your machine

Read from SKILL.md and the folder at commit 4f38503. It shows what the files ask for, not the result of running them.

  • Tool permissions

    Pre-approves nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.

    From allowed-tools in the SKILL.md frontmatter.

  • Runs code

    No scripts in the folder and no shell commands in SKILL.md (its code samples are tla).

    From the folder's file list and the shell code blocks in SKILL.md.

  • Network

    No URLs in SKILL.md.

    From URLs in SKILL.md, links to its own repository left out.

  • Credentials

    Names no API keys, tokens, secrets or passwords.

    From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Requirement To Tlaplus Property Generator loads about 1.9k tokens when it runs, and up to ~8.6k if it reads all its reference files. Until then it costs about 127 tokens; SKILL.md has 654 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it
~127
When it runs · the whole SKILL.md, loaded when a task matches
~1.9k
With references · SKILL.md plus every file in references/, read only if the agent opens them
~8.6k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check passed

The automated check found no risky patterns in SKILL.md.

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from ArabelaTso/Skills-4-SE at commit 4f38503, republished under its Apache-2.0 licence (© ArabelaTso). 654 words, ~1,905 tokens.

Download SKILL.mdSave it as .claude/skills/requirement-to-tlaplus-property-generator/SKILL.md (or your agent's skills folder). This skill also uses 3 other files; get the full folder from GitHub.
name
requirement-to-tlaplus-property-generator
description
Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents. Resolves ambiguities, asks clarifying questions for underspecified requirements, and outputs TLA+-compatible property definitions with semantic explanations. Use when translating system requirements, specifications, or behavioral constraints into formal TLA+ temporal logic properties for verification with TLC model checker.

Requirement to TLA+ Property Generator

Overview

This skill transforms natural-language requirements into formal TLA+ properties, enabling rigorous verification of system specifications. It handles invariants, safety properties, and liveness properties, resolving ambiguities and seeking clarification when needed.

Workflow

Step 1: Analyze the Requirement

Parse and understand the input requirement:

  1. Identify requirement type:

    • Invariant: "The system always maintains property P"
    • Safety: "Bad thing X never happens"
    • Liveness: "Good thing Y eventually happens"
    • Fairness: "Process Z gets a fair chance"

  2. Extract key elements:

    • State variables involved
    • Conditions and constraints
    • Temporal aspects (always, eventually, until, etc.)
    • Quantifiers (for all, exists)

  3. Detect ambiguities:

    • Undefined terms or variables
    • Unclear temporal scope
    • Missing boundary conditions
    • Implicit assumptions
Step 2: Resolve Ambiguities

When ambiguities are detected, use one of these strategies:

Strategy A: Reasonable Interpretation If the ambiguity has a standard interpretation in the domain, resolve it automatically and document the assumption.

Example:

  • Requirement: "The buffer never overflows"
  • Interpretation: "buffer_size <= MAX_BUFFER_SIZE" (assuming MAX_BUFFER_SIZE is defined)

Strategy B: Ask Clarifying Questions For critical or non-obvious ambiguities, ask the user:

  • "Does 'eventually' mean within a bounded time or unbounded?"
  • "Should this property hold for all processes or just specific ones?"
  • "What is the initial state assumption?"

See references/clarification_patterns.md for common question templates.

Step 3: Map to TLA+ Constructs

Translate the requirement into TLA+ syntax:

Invariants (Type Invariant or State Predicate):

tla
TypeOK == /\ var1 \in ValidSet1
          /\ var2 \in ValidSet2
          /\ condition

StateInvariant == predicate_over_state_variables

Safety Properties (Always):

tla
Safety == []P  \* P holds in all reachable states

Liveness Properties (Eventually):

tla
Liveness == <>P  \* P eventually holds
Liveness2 == [](P => <>Q)  \* If P holds, Q eventually holds

Fairness:

tla
Fairness == WF_vars(Action)  \* Weak fairness
Fairness2 == SF_vars(Action)  \* Strong fairness

See references/tlaplus_syntax.md for comprehensive syntax reference.

Step 4: Generate TLA+ Property Definition

Create the complete property definition:

  1. Choose appropriate name: Descriptive and follows TLA+ conventions
  2. Write the formula: Use correct TLA+ temporal operators
  3. Add comments: Explain the property's intent
  4. Include in spec: Show where to place it in the TLA+ module

Example output:

tla
\* Property: Buffer never overflows
\* Requirement: "The system must ensure the buffer size never exceeds capacity"
\* Type: Safety (Invariant)
BufferSafety == buffer_size <= MAX_BUFFER_SIZE

\* Add to specification:
\* Spec == Init /\ [][Next]_vars /\ BufferSafety
Step 5: Provide Semantic Explanation

Explain what the property means:

  1. Plain English: Restate in clear, unambiguous language
  2. Violation scenario: Describe what would violate this property
  3. Verification approach: How TLC will check it
  4. Related properties: Mention dependencies or related properties

Common Requirement Patterns

Pattern 1: Mutual Exclusion

Requirement: "At most one process can be in the critical section"

TLA+ Property:

tla
MutualExclusion ==
    \A p1, p2 \in Processes :
        (p1 # p2) => ~(pc[p1] = "critical" /\ pc[p2] = "critical")
Pattern 2: Eventual Progress

Requirement: "Every request is eventually served"

TLA+ Property:

tla
EventualService ==
    \A req \in Requests :
        (req.status = "pending") ~> (req.status = "completed")
Pattern 3: Bounded Response

Requirement: "The system responds within N steps"

TLA+ Property:

tla
\* Note: TLA+ doesn't directly express bounded liveness
\* Use auxiliary counter variable
BoundedResponse ==
    [](request_made => <>(response_sent \/ timeout_counter > N))
Pattern 4: Ordering Constraint

Requirement: "Event A must occur before event B"

TLA+ Property:

tla
OrderingConstraint ==
    [](event_B_occurred => event_A_occurred_before)

See references/requirement_patterns.md for more patterns.

Show full SKILL.md (260 more words)Show less

Handling Complex Requirements

Compound Requirements

Break down complex requirements into multiple properties:

Requirement: "The system must process requests in FIFO order and complete each within 10 steps"

Decomposition:

  1. FIFO ordering property
  2. Bounded completion property
  3. Conjunction of both
Conditional Requirements

Use implication for conditional properties:

Requirement: "If the system is in safe mode, no writes are allowed"

TLA+ Property:

tla
SafeModeConstraint == [](safe_mode => ~write_enabled)
Quantified Requirements

Use TLA+ quantifiers appropriately:

Requirement: "All active processes eventually terminate"

TLA+ Property:

tla
AllTerminate ==
    \A p \in Processes :
        (status[p] = "active") ~> (status[p] = "terminated")

Best Practices

  1. Start simple: Begin with basic invariants before complex temporal properties
  2. Be explicit: Document all assumptions and interpretations
  3. Use meaningful names: Property names should reflect their purpose
  4. Test incrementally: Verify simple properties first
  5. Consider negation: Sometimes it's easier to express "bad thing never happens"
  6. Check consistency: Ensure properties don't contradict each other

Common Pitfalls

Pitfall 1: Confusing safety and liveness

  • Safety: "Nothing bad happens" ([]P)
  • Liveness: "Something good happens" (<>P)

Pitfall 2: Unbounded liveness without fairness

  • Liveness properties often require fairness assumptions

Pitfall 3: Over-specification

  • Too many constraints may make the spec unrealizable

Pitfall 4: Implicit state assumptions

  • Always make initial state assumptions explicit

Output Format

For each requirement, provide:

  1. Original Requirement: Quote the input
  2. Property Type: Invariant/Safety/Liveness/Fairness
  3. TLA+ Definition: Complete, syntactically correct property
  4. Semantic Explanation: What it means in plain language
  5. Assumptions: Any assumptions made during translation
  6. Integration: How to add it to the TLA+ specification
  7. Verification Notes: Tips for checking with TLC

References

© ArabelaTso, Apache-2.0. Rendered from Markdown: HTML in the file is shown as text, images as links, and headings moved down two levels. Raw file

Files

SKILL.md and 3 other files (references) in skills/requirement-to-tlaplus-property-generator of ArabelaTso/Skills-4-SE.

  • SKILL.md
  • references/clarification_patterns.md
  • references/requirement_patterns.md
  • references/tlaplus_syntax.md

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Requirement To Tlaplus Property Generator next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Requirement To Tlaplus Property Generator compared with similar skills
SkillStarsUsed inTokensAuto-checkLicenceRepo updated
Requirement To Tlaplus Property Generator this skillArabelaTso/Skills-4-SE253—~1.9kAutomated safety check: PassApache-2.0
Writing Quotationmathbullet/skills173—~1.7kAutomated safety check: PassMIT
Lambda Langsickn33/agentic-awesome-skills47k1 repos~1.2kAutomated safety check: PassMIT
Yao Meta Skillyaojingang/yao-meta-skill2.7k—~768Automated safety check: PassMIT
Dsh Web Documentationzhu1090093659/dsh-web8.6k—~479Automated safety check: PassApache-2.0
China Travel Kittczyliu/china-travel-kit194—~1.3kAutomated safety check: PassMIT

Similar skills

  • Writing Quotation

    mathbullet/skills

    Formatting rules for quoting external sources (papers, articles, web pages, prompt templates) inside a Markdown document.

    173 GitHub stars~1.7k tokensUpdated 1 mo ago
    Agent WorkflowsAuto-check passed

  • Lambda Lang

    sickn33/agentic-awesome-skills

    Native agent-to-agent language for compact multi-agent messaging.

    47k GitHub starsUsed in 1 repo~1.2k tokens
    Agent WorkflowsAuto-check passed

  • Yao Meta Skill

    yaojingang/yao-meta-skill

    Create, improve, or evaluate an existing skill from workflows, prompts, SOPs, scripts.

    2.7k GitHub stars~768 tokensUpdated 1 mo ago
    Agent WorkflowsAuto-check passed

  • Dsh Web Documentation

    zhu1090093659/dsh-web

    A skill your agent uses when adding or editing dsh-web README files, docs, AGENTS.md instructions, user-facing configuration text, or bilingual documentation pairs.

    8.6k GitHub stars~479 tokensUpdated today
    Agent WorkflowsAuto-check passed

  • China Travel Kit

    tczyliu/china-travel-kit

    Research and plan first-time independent trips in China with bilingual, source-aware city data and official live-check entry points.

    194 GitHub stars~1.3k tokensUpdated 1 mo ago
    Writing & ContentAuto-check passed

  • Gearcoleco Romhacking

    drhelius/Gearcoleco

    Hack, modify, and translate ColecoVision and Super Game Module ROMs using the Gearcoleco emulator MCP server.

    142 GitHub stars~3.9k tokensUpdated today
    Agent WorkflowsAuto-check passed

More from ArabelaTso/Skills-4-SE

All 170 skills in this repo

  • Framework Migration Assistant

    ArabelaTso/Skills-4-SE

    Automatically migrate Python web applications between frameworks (Flask → FastAPI, Django → FastAPI).

    253 GitHub stars~1.9k tokensUpdated 1 mo ago
    Auto-check passed

  • Metamorphic Test Generator

    ArabelaTso/Skills-4-SE

    Generate test cases using metamorphic testing by applying transformations based on metamorphic properties.

    253 GitHub stars~798 tokensUpdated 1 mo ago
    Auto-check passed

  • Reproduction Trace Instrumenter

    ArabelaTso/Skills-4-SE

    Instruments programs to capture execution traces specifically for reproducing reported bugs, enabling consistent replay and diagnosis of failures.

    253 GitHub stars~2.4k tokensUpdated 1 mo ago
    Auto-check passed

  • Spring Mvc To Boot Migrator

    ArabelaTso/Skills-4-SE

    Automatically migrate Spring MVC applications to Spring Boot.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

  • State Snapshot Instrumenter

    ArabelaTso/Skills-4-SE

    Instrument programs (Python, C/C++, Java) to capture snapshots of key program states at runtime, including variables, memory, and call stacks.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

Categories

Questions about Requirement To Tlaplus Property Generator

What does Requirement To Tlaplus Property Generator do?

Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents. Requirement To Tlaplus Property Generator is an agent skill from ArabelaTso/Skills-4-SE. Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents.

When should I use Requirement To Tlaplus Property Generator?

Requirement To Tlaplus Property Generator fits situations like: translating system requirements; behavioral constraints into formal TLA+ temporal logic properties for verification with TLC model checker.

How do I install Requirement To Tlaplus Property Generator in Claude Code?

Run `npx skills add ArabelaTso/Skills-4-SE --skill requirement-to-tlaplus-property-generator -a claude-code`. Or copy the skill folder (skills/requirement-to-tlaplus-property-generator in ArabelaTso/Skills-4-SE) into .claude/skills/requirement-to-tlaplus-property-generator in your project. Claude Code loads it when a task matches its description.

How do I install Requirement To Tlaplus Property Generator in Codex?

Run `npx skills add ArabelaTso/Skills-4-SE --skill requirement-to-tlaplus-property-generator -a codex`. Or copy the skill folder (skills/requirement-to-tlaplus-property-generator in ArabelaTso/Skills-4-SE) into .agents/skills/requirement-to-tlaplus-property-generator in your project. Codex loads it when a task matches its description.

Can I use Requirement To Tlaplus Property Generator in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add ArabelaTso/Skills-4-SE --skill requirement-to-tlaplus-property-generator -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/requirement-to-tlaplus-property-generator, .gemini/skills/requirement-to-tlaplus-property-generator, .github/skills/requirement-to-tlaplus-property-generator and .opencode/skills/requirement-to-tlaplus-property-generator in your project.

What does Requirement To Tlaplus Property Generator need to run?

SKILL.md names no scripts, command-line tools or credentials: Requirement To Tlaplus Property Generator is instructions for the agent only.

Does Requirement To Tlaplus Property Generator access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Requirement To Tlaplus Property Generator safe to install?

Our automated static check of SKILL.md found no risky patterns, such as piping downloads into a shell, reading credential files or hidden Unicode. It is not a guarantee. Review the folder before installing.

What licence does Requirement To Tlaplus Property Generator use?

Requirement To Tlaplus Property Generator is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Requirement To Tlaplus Property Generator use?

About 1.9k tokens (SKILL.md is roughly 7.6k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full. Its references folder adds about 6.7k tokens, read only when the agent opens those files.

What are the alternatives to Requirement To Tlaplus Property Generator?

Skills that share tags, products or a category with Requirement To Tlaplus Property Generator: Writing Quotation (mathbullet/skills, 173 stars), Lambda Lang (sickn33/agentic-awesome-skills, 47k stars), Yao Meta Skill (yaojingang/yao-meta-skill, 2.7k stars) and Dsh Web Documentation (zhu1090093659/dsh-web, 8.6k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Requirement To Tlaplus Property Generator?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 170 skills in this directory. The repository was last updated on August 21, 2026.

Source: ArabelaTso/Skills-4-SE on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.