Skill Claude CodeCodex
Add a new variable to an existing TLA+ specification without changing its semantics. Ensures the variable is declared, initialized, and added to all UNCHANGED statements. Use when the user asks to add, introduce, or declare a new variable in a TLA+ spec, or mentions UNCHANGED statements.
Skill Claude CodeCodex
Generate a high-level TLA+ model from source code (C, C++, Rust, etc.). Analyzes code to understand its purpose, creates abstractions, writes TLA+ specification, and proposes invariants and properties. Use when the user wants to model source code in TLA+, create a formal specification from implementation, or verify…
Skill Claude CodeCodex
Split a TLA+ action into two sequential actions by introducing a new program counter (pc) state. Handles pc variable updates, UNCHANGED statements, TypeOk predicates, and follows naming conventions with renumbering. Use when the user asks to split, divide, or break an action into two parts, or wants to add an…