Claude Code plugins for TLA+ formal verification and specification
npx claudepluginhub andrueandersoncs/claude-tla-plus-pluginGenerate TLA+ specifications, PlusCal algorithms, and TLC model configurations for formal verification of distributed systems, concurrent algorithms, and state machines
No description available.
Claude Code marketplace entries for the plugin-safe Antigravity Awesome Skills library and its compatible editorial bundles.
Production-ready workflow orchestration with 79 focused plugins, 184 specialized agents, and 150 skills - optimized for granular installation and minimal token usage
A Claude Code plugin that enables generation of TLA+ specifications, PlusCal algorithms, and TLC model configurations for formal verification of distributed systems, concurrent algorithms, and state machines.
claude --plugin-dir ./claude-tla-plus-plugin
/plugin install tla-plus@marketplace-name
Claude automatically uses the TLA+ generation skill when you ask about:
| Command | Description |
|---|---|
/tla-plus:spec <description> | Generate a complete TLA+ specification |
/tla-plus:pluscal <description> | Generate a PlusCal algorithm |
/tla-plus:invariant <description> | Generate invariants for a spec |
/tla-plus:liveness <description> | Generate liveness properties |
/tla-plus:config <description> | Generate TLC configuration |
/tla-plus:review <file> | Review an existing TLA+ spec |
/tla-plus:spec a simple key-value store with get and put operations
/tla-plus:pluscal Dijkstra's mutual exclusion algorithm for 3 processes
/tla-plus:invariant for my KeyValueStore.tla specification
/tla-plus:liveness ensure all requests eventually complete
/tla-plus:config for KeyValueStore.tla with 2 keys and 3 transactions
/tla-plus:review check my consensus protocol for issues
claude-tla-plus-plugin/
├── .claude-plugin/
│ └── plugin.json # Plugin manifest
├── commands/
│ ├── spec.md # Generate specifications
│ ├── pluscal.md # Generate PlusCal algorithms
│ ├── invariant.md # Generate invariants
│ ├── liveness.md # Generate liveness properties
│ ├── config.md # Generate TLC configuration
│ └── review.md # Review specifications
├── skills/
│ └── tla-plus-generator/
│ ├── SKILL.md # Main skill definition
│ ├── syntax-reference.md # Complete TLA+ syntax
│ ├── patterns-examples.md # Example specifications
│ └── tlc-configuration.md # TLC config guide
├── examples/ # Git submodule: tlaplus/Examples
│ └── specifications/ # 100+ real-world TLA+ specs
└── README.md
This plugin includes the official TLA+ Examples repository as a git submodule in the examples/ directory. This provides 100+ real-world TLA+ specifications for reference.
git clone --recurse-submodules <repo-url>
# Or if already cloned:
git submodule update --init --recursive
examples/specifications/Paxos/ - Paxos consensus algorithmRaft/ - Raft consensus protocolTwoPhase/ - Two-phase committransaction_commit/ - Transaction protocolsewd840/ - Dijkstra's algorithmslamport_mutex/ - Lamport's mutual exclusionThe plugin's skill documentation includes comprehensive examples based on the TLA+ examples repository:
MIT