Agent skill

Tlaplus Spec Generator

Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems.

Apache-2.0Auto-check passedDatabases

Install Tlaplus Spec Generator

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill tlaplus-spec-generator -a claude-code

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

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE tlaplus-spec-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/tlaplus-spec-generator .claude/skills/tlaplus-spec-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/

Paste into Claude Code

Install the "tlaplus-spec-generator" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator into .claude/skills/tlaplus-spec-generator/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "tlaplus-spec-generator", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill tlaplus-spec-generator -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE tlaplus-spec-generator --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .agents/skills && cp -r skills-src/skills/tlaplus-spec-generator .agents/skills/tlaplus-spec-generator && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "tlaplus-spec-generator" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator into .agents/skills/tlaplus-spec-generator/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "tlaplus-spec-generator", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill tlaplus-spec-generator -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE tlaplus-spec-generator --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/skills/tlaplus-spec-generator .cursor/skills/tlaplus-spec-generator && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "tlaplus-spec-generator" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator into .cursor/skills/tlaplus-spec-generator/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "tlaplus-spec-generator", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/ArabelaTso/Skills-4-SE.git --path skills/tlaplus-spec-generator

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill tlaplus-spec-generator -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE tlaplus-spec-generator --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/skills/tlaplus-spec-generator .gemini/skills/tlaplus-spec-generator && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "tlaplus-spec-generator" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator into .gemini/skills/tlaplus-spec-generator/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "tlaplus-spec-generator", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE tlaplus-spec-generator

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill tlaplus-spec-generator -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .github/skills && cp -r skills-src/skills/tlaplus-spec-generator .github/skills/tlaplus-spec-generator && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "tlaplus-spec-generator" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator into .github/skills/tlaplus-spec-generator/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "tlaplus-spec-generator", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add ArabelaTso/Skills-4-SE --skill tlaplus-spec-generator -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install ArabelaTso/Skills-4-SE tlaplus-spec-generator --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/skills/tlaplus-spec-generator .opencode/skills/tlaplus-spec-generator && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "tlaplus-spec-generator" agent skill from https://github.com/ArabelaTso/Skills-4-SE/tree/main/skills/tlaplus-spec-generator into .opencode/skills/tlaplus-spec-generator/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "tlaplus-spec-generator", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: tlaplus-spec-generator
GitHub stars: 253
Token cost: ~2.3k tokens
SKILL.md length: 664 words
Files: 6 (incl. scripts, references)
Skills in repo: 150
Repo updated: Aug 21, 2026
First seen: Oct 7, 2026
Licence: Apache-2.0

At a glance

Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems.

Works in 5 steps: Analyze Source Code → Specify System Parameters → Generated Output → …
Generate TLA+ specs from program implementations
SKILL.md covers Overview, Workflow, Abstraction Levels and Common Use Cases, plus 7 more sections
Runs Python scripts from its folder; calls python3

What it does

Tlaplus Spec Generator is an agent skill from ArabelaTso/Skills-4-SE. Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems. Use when users need to: (1) Generate TLA+ specs from program implementations, (2) Model distributed systems, consensus protocols, or concurrent algorithms, (3) Extract state variables, actions, and invariants from code, (4) Create formal specifications for model checking with TLC, (5) Verify safety and liveness properties of distributed systems. Particularly effective for message-passing…

Its SKILL.md is about 2.3k tokens, which your agent loads only when the skill is triggered. The skill folder holds 7 other files, including scripts and reference files (for example `references/distributed_patterns.md`, `references/tlaplus_syntax.md` and `scripts/generate_spec.py`).

It sits in Databases, covering Database administration. It works with C++ and Python. 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

Generate TLA+ specs from program implementations
Model distributed systems
Consensus protocols
Concurrent algorithms

Example prompts

“/tlaplus-spec-generator”

Requirements

Python 3

Workflow steps

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

Analyze Source Code
Specify System Parameters
Generated Output
Refine the Specification
Model Check with TLC

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
Ships 3 files in scripts/ (Python), which the agent can run.
Shell commands in SKILL.md call:
- python3
From the folder's file list and the shell code blocks in SKILL.md.
Network
Links to these hosts (documentation or services it may open):
- lamport.azurewebsites.net
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

Tlaplus Spec Generator loads about 2.3k tokens when it runs, and up to ~6.2k if it reads all its reference files. Until then it costs about 155 tokens; SKILL.md has 664 words of instructions outside code blocks.

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

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); the scripts in this folder are not scanned.

SKILL.md

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

Download SKILL.mdSave it as .claude/skills/tlaplus-spec-generator/SKILL.md (or your agent's skills folder). This skill also uses 5 other files; get the full folder from GitHub.

name: tlaplus-spec-generator
description: Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems. Use when users need to: (1) Generate TLA+ specs from program implementations, (2) Model distributed systems, consensus protocols, or concurrent algorithms, (3) Extract state variables, actions, and invariants from code, (4) Create formal specifications for model checking with TLC, (5) Verify safety and liveness properties of distributed systems. Particularly effective for message-passing systems, replication protocols, consensus algorithms, and distributed transactions.

TLA+ Spec Generator

Automatically generate TLA+ specifications from program implementations for formal verification of distributed systems.

Overview

This skill transforms imperative programs (C/C++, Python) into declarative TLA+ specifications. It analyzes program structure to identify state variables, actions, and system behavior, then generates well-structured TLA+ modules suitable for model checking with TLC.

Workflow

1. Analyze Source Code

Generate TLA+ specification from source files:

bash

# Single file
python3 scripts/generate_spec.py program.py -o Spec.tla

# Multiple files
python3 scripts/generate_spec.py server.py client.py protocol.py -o Protocol.tla

# With module name
python3 scripts/generate_spec.py distributed_system.c -o System.tla --module-name DistributedSystem

The generator automatically:

Detects programming language
Parses source code
Identifies state variables and actions
Extracts system structure
Generates TLA+ specification

2. Specify System Parameters

For distributed systems, specify the number of processes:

bash

python3 scripts/generate_spec.py consensus.py -o Consensus.tla --processes 3

This creates a constant N in the TLA+ spec representing the number of processes/nodes.

3. Generated Output

The generator produces two files:

1. Spec.tla - Complete TLA+ specification:

tla

---- MODULE Spec ----
EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS N  \* Number of processes

VARIABLES
  state,
  messages,
  committed

vars == <<state, messages, committed>>

TypeOK ==
  /\ state \in [1..N -> {"Init", "Working", "Done"}]
  /\ messages \in SUBSET Messages
  /\ committed \in SUBSET Operations

Init ==
  /\ state = [p \in 1..N |-> "Init"]
  /\ messages = {}
  /\ committed = {}

SendMessage(p, msg) ==
  /\ state[p] = "Working"
  /\ messages' = messages \cup {msg}
  /\ UNCHANGED <<state, committed>>

Next ==
  \/ \E p \in 1..N, msg \in Messages : SendMessage(p, msg)

Spec == Init /\ [][Next]_vars

====

2. Spec_mapping.txt - Explanation of program-to-TLA+ mapping:

State variables and their types
Actions and what they modify
Processes identified
Constants defined

4. Refine the Specification

The generated spec is a starting point. Refine it by:

Review state variables - Ensure all relevant state is captured
Complete action definitions - Add preconditions and effects
Add invariants - Define safety properties
Add temporal properties - Define liveness properties
Adjust abstraction - Balance detail vs. tractability

5. Model Check with TLC

Create a TLC configuration file (Spec.cfg):

CONSTANTS
  N = 3

SPECIFICATION Spec

INVARIANT TypeOK

Run TLC model checker:

bash

tlc Spec.tla -config Spec.cfg

Abstraction Levels

Control the level of abstraction:

bash

# Low abstraction (more detail, larger state space)
python3 scripts/generate_spec.py program.py -o Spec.tla --abstraction low

# Medium abstraction (balanced, recommended)
python3 scripts/generate_spec.py program.py -o Spec.tla --abstraction medium

# High abstraction (minimal states, protocol-level)
python3 scripts/generate_spec.py program.py -o Spec.tla --abstraction high

Medium abstraction (default):

Booleans → preserved
Integers → bounded ranges (0..N)
Enums → preserved as string sets
Collections → sequences or sets
Focus on control flow and key state

Common Use Cases

Distributed Consensus Protocol

Scenario: Implementing Raft or Paxos consensus algorithm.

Approach:

Generate spec from implementation
Identify processes (nodes), state variables (term, log, votes)
Extract actions (RequestVote, AppendEntries, etc.)
Add safety properties (leader uniqueness, log consistency)
Verify with TLC

See: distributed_patterns.md

Message-Passing System

Scenario: Distributed system with processes communicating via messages.

Approach:

Generate spec from message handlers
Model network as set of messages in transit
Define Send and Receive actions
Add properties (message ordering, delivery guarantees)
Check for deadlocks and livelocks

See: distributed_patterns.md

Replication Protocol

Scenario: Primary-backup or multi-master replication.

Approach:

Generate spec from replication logic
Model replicas and their logs
Define replication and commit actions
Add consistency properties
Verify under failures

See: distributed_patterns.md

Leader Election

Scenario: Implementing leader election algorithm.

Approach:

Generate spec from election code
Model process states (follower, candidate, leader)
Extract election actions
Add safety (at most one leader) and liveness (eventually a leader)
Verify correctness

See: distributed_patterns.md

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

Advanced Options

Focus on Specific Functions

Extract only relevant functions:

bash

python3 scripts/generate_spec.py system.py -o Spec.tla \
  --focus-functions send_message receive_message commit_transaction

Track Specific Variables

Explicitly specify state variables:

bash

python3 scripts/generate_spec.py system.py -o Spec.tla \
  --track-vars state messages committed_ops leader_id

Refining Generated Specs

Generated specs need refinement. Common refinements:

1. Complete action preconditions:

tla

\* Generated (incomplete)
SendMessage(p, msg) ==
  /\ messages' = messages \cup {msg}

\* Refined (with precondition)
SendMessage(p, msg) ==
  /\ state[p] = "Active"        \* Precondition
  /\ msg \notin messages         \* No duplicates
  /\ messages' = messages \cup {msg}
  /\ UNCHANGED <<state, committed>>

2. Add invariants:

tla

\* Safety properties
SafetyInvariant ==
  /\ \A p \in Procs : state[p] \in ValidStates
  /\ Cardinality({p \in Procs : state[p] = "Leader"}) <= 1

\* Add to spec
INVARIANT TypeOK
INVARIANT SafetyInvariant

3. Add liveness properties:

tla

\* Eventually reach consensus
PROPERTY <>[](\A p \in Procs : state[p] = "Committed")

\* Every request is eventually processed
PROPERTY \A req \in Requests : [](Submitted(req) => <>Processed(req))

4. Add fairness:

tla

\* Weak fairness: continuously enabled actions eventually happen
Spec == Init /\ [][Next]_vars /\ WF_vars(ReceiveMessage)

\* Strong fairness: infinitely often enabled actions eventually happen
Spec == Init /\ [][Next]_vars /\ SF_vars(ElectLeader)

Tips

Start with small models - Use N=2 or N=3 processes initially
Check TypeOK first - Ensures basic correctness before complex properties
Use symmetry - Add SYMMETRY Permutations(Procs) to reduce state space
Abstract data values - Focus on protocol behavior, not data content
Iterate abstraction - If TLC is too slow, increase abstraction
Read the mapping file - Understand how program maps to TLA+
Consult patterns - See reference docs for common distributed system patterns

Common Issues

State explosion: TLC runs out of memory or takes too long.

Solution: Increase abstraction, reduce N, add state constraints, use symmetry

Deadlock detected: TLC finds states with no enabled actions.

Solution: Check action preconditions, ensure progress is always possible, add fairness

Invariant violated: TLC finds counterexample.

Solution: Review counterexample trace, fix implementation or weaken invariant

Spec too abstract: Properties are trivially true.

Solution: Decrease abstraction, track more variables, preserve more detail

References

tlaplus_syntax.md: Complete TLA+ syntax reference with examples
distributed_patterns.md: Common patterns for distributed systems (consensus, replication, leader election)

Scripts

generate_spec.py: Main generation script (orchestrates entire process)
program_analyzer.py: Program analysis module (extracts state, actions, processes)
tlaplus_generator.py: TLA+ generation module (produces TLA+ specifications)

External Tools

TLA+ Toolbox: IDE for writing and checking TLA+ specs (https://lamport.azurewebsites.net/tla/toolbox.html)
TLC Model Checker: Command-line model checker (included with Toolbox)
TLAPS: TLA+ Proof System for theorem proving (optional)

Files

SKILL.md and 5 other files (scripts, references) in skills/tlaplus-spec-generator of ArabelaTso/Skills-4-SE.

SKILL.md
references/distributed_patterns.md
references/tlaplus_syntax.md
scripts/generate_spec.py
scripts/program_analyzer.py
scripts/tlaplus_generator.py

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Tlaplus Spec 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.

Tlaplus Spec Generator compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Tlaplus Spec Generator this skillArabelaTso/Skills-4-SE	253	—	~2.3k	Automated safety check: Pass	Apache-2.0	1 mo ago
Elodin DBelodin-sys/elodin	547	—	~2.8k	Automated safety check: Pass	Apache-2.0	yesterday
Sap Hana Cloud Data Intelligencesecondsky/sap-skills	462	—	~3.2k	Automated safety check: Pass	GPL-3.0	3 days ago
MoviePilot Database Operationjxxghp/MoviePilot	12k	—	~7.3k	Automated safety check: Pass	GPL-3.0	yesterday
DBoracle/skills	873	—	~1.4k	Automated safety check: Pass	UPL-1.0	2 days ago
Triage Tt Metal Assertstenstorrent/tt-mlir	312	—	~7.8k	Automated safety check: Pass	Apache-2.0	yesterday

Similar skills

Elodin DB
elodin-sys/elodin
Work with Elodin-DB, the time-series telemetry database. An agent skill from elodin-sys/elodin.
547 GitHub stars~2.8k tokensUpdated yesterday
Data & AnalyticsAuto-check passed
Sap Hana Cloud Data Intelligence
secondsky/sap-skills
Develops data processing pipelines, integrations, and machine learning scenarios in SAP Data Intelligence Cloud.
462 GitHub stars~3.2k tokensUpdated 3 days ago
Data & AnalyticsAuto-check passed
MoviePilot Database Operation
jxxghp/MoviePilot
Inspects, queries and carefully modifies the MoviePilot SQLite or PostgreSQL database through a bundled script that reads connection settings itself, without needing the password in the prompt.
12k GitHub stars~7.3k tokensUpdated yesterday
DatabasesAuto-check passed
DB
oracle/skills
Official
Oracle Database guidance for SQL, PL/SQL, SQLcl, ORDS, Oracle Vector SDK, administration, app development, performance, security, migrations, and agent-safe database workflows.
873 GitHub stars~1.4k tokensUpdated 2 days ago
DatabasesAuto-check passed
Triage Tt Metal Asserts
tenstorrent/tt-mlir
Triage a tt-metal uplift diff or digest of TTFATAL validation changes against what tt-mlir guarantees at each optimization level (0: workarounds only, 1: optimizer with DRAM-only fallback, 2: L1…
312 GitHub stars~7.8k tokensUpdated yesterday
DatabasesAuto-check passed
Redis Inspector
evolution-foundation/evo-nexus
Reads keys and server state from Redis instances configured in .env through a read-only Python client, choosing connections by label or index.
545 GitHub stars~1.3k tokensUpdated 4 mo ago
DatabasesAuto-check: notes

Questions about Tlaplus Spec Generator

What does Tlaplus Spec Generator do?

Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems. Tlaplus Spec Generator is an agent skill from ArabelaTso/Skills-4-SE. Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems.

When should I use Tlaplus Spec Generator?

Tlaplus Spec Generator fits situations like: generate TLA+ specs from program implementations; model distributed systems; consensus protocols; concurrent algorithms.

How do I install Tlaplus Spec Generator in Claude Code?

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

How do I install Tlaplus Spec Generator in Codex?

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

Can I use Tlaplus Spec 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 tlaplus-spec-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/tlaplus-spec-generator, .gemini/skills/tlaplus-spec-generator, .github/skills/tlaplus-spec-generator and .opencode/skills/tlaplus-spec-generator in your project.

What does Tlaplus Spec Generator need to run?

Going by SKILL.md and its folder, Tlaplus Spec Generator needs Python for the scripts in its folder and the command-line tools its instructions call (python3). Our summary lists: Python 3.

Does Tlaplus Spec Generator access the network?

SKILL.md names 1 domain. As links in the text: lamport.azurewebsites.net. This is read from the text; nothing was executed.

Is Tlaplus Spec 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. The check reads SKILL.md only: the scripts in the folder are not scanned, so read them before running anything.

What licence does Tlaplus Spec Generator use?

Tlaplus Spec 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 Tlaplus Spec Generator use?

About 2.3k tokens (SKILL.md is roughly 9.3k 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 3.8k tokens, read only when the agent opens those files.

What are the alternatives to Tlaplus Spec Generator?

Skills that share tags, products or a category with Tlaplus Spec Generator: Elodin DB (elodin-sys/elodin, 547 stars), Sap Hana Cloud Data Intelligence (secondsky/sap-skills, 462 stars), MoviePilot Database Operation (jxxghp/MoviePilot, 12k stars) and DB (oracle/skills, 873 stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Tlaplus Spec Generator?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 150 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.

Install Tlaplus Spec Generator

Facts

At a glance

What it does

When your agent uses it

Example prompts

Requirements

Workflow steps

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

TLA+ Spec Generator

Overview

Workflow

1. Analyze Source Code

2. Specify System Parameters

3. Generated Output

4. Refine the Specification

5. Model Check with TLC

Abstraction Levels

Common Use Cases

Distributed Consensus Protocol

Message-Passing System

Replication Protocol

Leader Election

Advanced Options

Focus on Specific Functions

Track Specific Variables

Refining Generated Specs

Tips

Common Issues

References

Scripts

External Tools

Files

Compare with similar skills

Similar skills

More from ArabelaTso/Skills-4-SE

Related

Questions about Tlaplus Spec Generator