Menu
TLA+ formal specification expert for writing specs, model checking, and applying formal methods to amplihack workflows
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
Based on SOC occupation classification
Auto-generates code flow diagrams from multi-language module analysis. Detects when architecture diagrams become stale (code changed, diagram didn't). Supports Python, TypeScript/JavaScript, Rust, and Go out of the box. Use when: creating new modules, reviewing PRs for architecture impact, or checking diagram freshness across polyglot repositories. Generates mermaid diagrams showing imports, dependencies, and module relationships.
Execute multiple independent development tasks in parallel using subprocess isolation. Each task runs in a clean /tmp clone with Recipe Runner code-enforced workflow execution. Proven pattern: 4/5 PRs created successfully in first production use.
Interactive teaching agent for the goal-seeking agent generator and eval system. Provides a structured 14-lesson curriculum covering agent generation, SDK selection, multi-agent architecture, progressive evaluation (L1-L12), retrieval strategies, intent classification, math code generation, self-improvement loops with patch proposer and reviewer voting, and memory export/import.
Development workflow for features, bugs, refactoring. Normally executed as a sub-recipe by dev-orchestrator/smart-orchestrator. Supports direct invocation via recipe runner for standalone use.
Default task orchestrator for all development and investigation work. Classifies tasks, decomposes into parallel workstreams if appropriate, and routes execution through the recipe runner. Replaces ultrathink-orchestrator.
Writing clear, discoverable software documentation following the Eight Rules and Diataxis framework. Use when creating README files, API docs, tutorials, how-to guides, or any project documentation. Automatically enforces docs/ location, linking requirements, and runnable examples.
| name | tla-plus-expert |
| version | 1.0.0 |
| description | TLA+ formal specification expert for writing specs, model checking, and applying formal methods to amplihack workflows |
| activation_keywords | ["TLA+","TLA","formal specification","formal spec","model checking","model checker","TLC","PlusCal","invariant","liveness property","safety property","temporal logic","state machine spec","protocol verification"] |
| agent | amplihack:specialized:tla-plus-expert |
Provides expert-level TLA+ formal specification assistance for designing, verifying, and reasoning about concurrent and distributed systems within amplihack.
This skill delegates to the tla-plus-expert agent which has deep knowledge of:
The amplihack repo includes a TLA+ experiment runner at crates/amplihack-eval/src/tla_prompt_experiment.rs with:
TLA+ specs live in experiments/hive_mind/tla_prompt_language/specs/.
# 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?
experiments/hive_mind/tla_prompt_language/specs/crates/amplihack-eval/src/tla_prompt_experiment.rs/usr/local/bin/tlc (if installed)