Individual skill
tlaplus-spec-generator
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.
skills/tlaplus-spec-generator/SKILL.md
Source commit 4f38503747e0617504bce5329283ef837d375c09
What was checked
- Matches the observed repository HEAD
- Yes
- Scanner rules are current
- Yes
- Repository scan complete
- No
- Skill scan complete
- No
- Observed behavior
- Local scripts
- Last checked
- Nov 11, 2026
These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.
Install this skill
Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.
An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.
Repository context
- Repository stars (not skill ratings)
- 260
- Repository last updated
- Aug 21, 2026
- License
- Apache-2.0
Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.
- claude-skills Repository topic
- metaprogramming Repository topic
- software-development Repository topic
- software-engineering Repository topic
- claude Repository topic
- claude-code Repository topic
- engineering Derived category
Files and excerpt
File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.
Browse files
SKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesSKILL.mdcore · 9,310 bytesreferences/distributed_patterns.mddoc · 9,367 bytesreferences/tlaplus_syntax.mddoc · 6,016 bytesscripts/generate_spec.pyruns · 3,597 bytesscripts/program_analyzer.pyruns · 8,465 bytesscripts/tlaplus_generator.pyruns · 11,871 bytes
Read excerpt
# 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:
