TLA+ Expert Skill
Purpose
Provides expert-level TLA+ formal specification assistance for designing, verifying, and reasoning about concurrent and distributed systems within amplihack.
When This Skill Activates
- User asks to write or review a TLA+ specification
- User needs help with model checking (TLC) configuration or output interpretation
- User wants to formally verify a protocol or workflow design
- User asks about invariants, liveness properties, or safety properties
- User wants to apply formal methods to amplihack components
- User mentions PlusCal or wants to translate between PlusCal and TLA+
- User references Lamport, Demirbas, or formal methods best practices
How It Works
This skill delegates to the tla-plus-expert agent which has deep knowledge of:
- TLA+ language and idioms — writing specs, operators, temporal formulas
- TLC model checker — configuration, trace interpretation, state space management
- Seven mental models (Demirbas) — abstraction, global shared memory, local guards, invariants, stepwise refinement, atomicity refinement, communication
- Industry case studies — 8 production uses from AWS, MongoDB, Microsoft Azure
- AI + TLA+ limitations — SysMoBench findings on LLM capabilities and guardrails
- amplihack experiment infrastructure — manifest-driven experiments, heuristic scoring, TLC validation integration
Integration with Existing Infrastructure
The amplihack repo includes a TLA+ experiment runner at crates/amplihack-eval/src/tla_prompt_experiment.rs with:
- Manifest-driven experiment matrix (models x prompt variants x repeats)
- 6 heuristic scoring dimensions
- Real TLC validation support
- Replay and live execution modes
TLA+ specs live in experiments/hive_mind/tla_prompt_language/specs/.
Usage Examples
# Write a spec for a new protocol
/tla-plus-expert Write a TLA+ spec for our consensus voting workflow
# Review an existing spec
/tla-plus-expert Review specs/SmartOrchestrator.tla for correctness
# Help with TLC output
/tla-plus-expert TLC found a counterexample in my spec, help me understand it
# Decide if TLA+ is appropriate
/tla-plus-expert Should I formally specify this retry cascade logic?
# Generate invariants
/tla-plus-expert What invariants should I check for a parallel workstream manager?
Key Resources
- TLA+ specs:
experiments/hive_mind/tla_prompt_language/specs/
- Experiment runner:
crates/amplihack-eval/src/tla_prompt_experiment.rs
- TLC binary:
/usr/local/bin/tlc (if installed)
- Issue #3939: TLA+ integration roadmap
Related Skills
- property-based-testing: The executable counterpart in the formal-methods
triad. Where TLA+ model-checks an abstract design, property-based-testing
exercises the concrete implementation against invariants/round-trip/oracle
properties. Use TLA+ to prove the design; use property-based-testing to check
the code matches it.
- gherkin-expert: Specifies example-driven behavior; complements the
exhaustive design coverage TLA+ provides.
1---2name: tla-plus-expert-23description: TLA+ formal specification expert for writing specs, model checking, and applying formal methods to amplihack workflows4---56# TLA+ Expert Skill78## Purpose910Provides expert-level TLA+ formal specification assistance for designing, verifying, and reasoning about concurrent and distributed systems within amplihack.1112## When This Skill Activates1314- User asks to write or review a TLA+ specification15- User needs help with model checking (TLC) configuration or output interpretation16- User wants to formally verify a protocol or workflow design17- User asks about invariants, liveness properties, or safety properties18- User wants to apply formal methods to amplihack components19- User mentions PlusCal or wants to translate between PlusCal and TLA+20- User references Lamport, Demirbas, or formal methods best practices2122## How It Works2324This skill delegates to the `tla-plus-expert` agent which has deep knowledge of:25261. **TLA+ language and idioms** — writing specs, operators, temporal formulas272. **TLC model checker** — configuration, trace interpretation, state space management283. **Seven mental models** (Demirbas) — abstraction, global shared memory, local guards, invariants, stepwise refinement, atomicity refinement, communication294. **Industry case studies** — 8 production uses from AWS, MongoDB, Microsoft Azure305. **AI + TLA+ limitations** — SysMoBench findings on LLM capabilities and guardrails316. **amplihack experiment infrastructure** — manifest-driven experiments, heuristic scoring, TLC validation integration3233## Integration with Existing Infrastructure3435The amplihack repo includes a TLA+ experiment runner at `crates/amplihack-eval/src/tla_prompt_experiment.rs` with:3637- Manifest-driven experiment matrix (models x prompt variants x repeats)38- 6 heuristic scoring dimensions39- Real TLC validation support40- Replay and live execution modes4142TLA+ specs live in `experiments/hive_mind/tla_prompt_language/specs/`.4344## Usage Examples4546```47# Write a spec for a new protocol48/tla-plus-expert Write a TLA+ spec for our consensus voting workflow4950# Review an existing spec51/tla-plus-expert Review specs/SmartOrchestrator.tla for correctness5253# Help with TLC output54/tla-plus-expert TLC found a counterexample in my spec, help me understand it5556# Decide if TLA+ is appropriate57/tla-plus-expert Should I formally specify this retry cascade logic?5859# Generate invariants60/tla-plus-expert What invariants should I check for a parallel workstream manager?61```6263## Key Resources6465- TLA+ specs: `experiments/hive_mind/tla_prompt_language/specs/`66- Experiment runner: `crates/amplihack-eval/src/tla_prompt_experiment.rs`67- TLC binary: `/usr/local/bin/tlc` (if installed)68- Issue #3939: TLA+ integration roadmap6970## Related Skills7172- **property-based-testing**: The executable counterpart in the formal-methods73 triad. Where TLA+ model-checks an abstract design, property-based-testing74 exercises the concrete implementation against invariants/round-trip/oracle75 properties. Use TLA+ to prove the design; use property-based-testing to check76 the code matches it.77- **gherkin-expert**: Specifies example-driven behavior; complements the78 exhaustive design coverage TLA+ provides.
rysweet