Agent Skills: tlaplus-modeling

Model and reason about concurrent or distributed systems with TLA+ and PlusCal. Use when: designing multithreaded or distributed behavior before code exists, deriving invariants from an informal design, writing TLA+ specs, creating PlusCal algorithms, model checking with TLC, organizing multi-module specifications, debugging verification failures, or reducing state space. Covers informal concurrency design, MCP tool usage, PlusCal preferred syntax (call/await over goto), TLA+ module organization, and state-space optimization.