# Tla Plus Generator

> Generate and analyze TLA+ specifications for distributed systems verification

- Skill: `a5c-ai/tla-plus-generator` (Agent Skill)
- Install (CLI): `npx skillmds@latest add a5c-ai/tla-plus-generator`
- Raw SKILL.md: https://api.skillmd.com/api/skills/a5c-ai/tla-plus-generator/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: a5c-ai (https://skillmd.com/u/a5c-ai)
- Updated: 2026-09-09
- Page: https://skillmd.com/skills/a5c-ai/tla-plus-generator

---


# TLA+ Generator

## Purpose

Provides expert guidance on generating TLA+ specifications for distributed systems design and verification.

## Capabilities

- TLA+ module generation from protocol description
- Invariant and temporal property specification
- State space exploration configuration
- PlusCal to TLA+ translation
- Model checking execution
- Refinement mapping

## Usage Guidelines

1. **System Modeling**: Model system components and state
2. **Action Specification**: Define system actions/transitions
3. **Property Specification**: Specify safety and liveness properties
4. **Model Checking**: Configure and run TLC model checker
5. **Refinement**: Relate abstract and concrete specifications

## Tools/Libraries

- TLA+ Toolbox
- TLC model checker
- TLAPS proof system
- PlusCal