From tla-plus
Generate TLA+ specifications, PlusCal algorithms, and TLC model configurations for formal verification. Use when the user wants to formally specify systems, verify concurrent algorithms, model distributed systems, check safety/liveness properties, or create state machine specifications.
npx claudepluginhub andrueandersoncs/claude-tla-plus-plugin --plugin tla-plusThis skill uses the workspace's default tool permissions.
You are an expert in TLA+ (Temporal Logic of Actions), a formal specification language for describing and verifying concurrent and distributed systems. When generating TLA+ specifications, follow these guidelines and patterns.
Provides UI/UX resources: 50+ styles, color palettes, font pairings, guidelines, charts for web/mobile across React, Next.js, Vue, Svelte, Tailwind, React Native, Flutter. Aids planning, building, reviewing interfaces.
Fetches up-to-date documentation from Context7 for libraries and frameworks like React, Next.js, Prisma. Use for setup questions, API references, and code examples.
Analyzes competition with Porter's Five Forces, Blue Ocean Strategy, and positioning maps to identify differentiation opportunities and market positioning for startups and pitches.
You are an expert in TLA+ (Temporal Logic of Actions), a formal specification language for describing and verifying concurrent and distributed systems. When generating TLA+ specifications, follow these guidelines and patterns.
Every TLA+ specification follows this structure:
--------------------------- MODULE ModuleName ---------------------------
(* Module documentation *)
EXTENDS Naturals, Sequences, FiniteSets, TLC \* Standard modules
CONSTANTS ConstantName \* Declared constants
VARIABLES var1, var2 \* State variables
----------------------------------------------------------------------------
\* Definitions, operators, and actions go here
=============================================================================
Init == \* Initial state predicate
/\ var1 = initialValue1
/\ var2 = initialValue2
Next == \* Next-state relation (disjunction of actions)
\/ Action1
\/ Action2
\/ \E x \in SomeSet : Action3(x)
Spec == Init /\ [][Next]_<<var1, var2>> \* Full specification
/\ - conjunction (AND)\/ - disjunction (OR)~ - negation (NOT)=> - implication<=> - equivalenceTRUE, FALSE - boolean constants\in - element of\notin - not element of\cup - union\cap - intersection\subseteq - subset or equalSUBSET S - powerset of SUNION S - union of all sets in S{x \in S : P(x)} - set filter{f(x) : x \in S} - set mapCardinality(S) - size of finite set (requires FiniteSets)[x \in S |-> expr] - function definitionf[x] - function applicationDOMAIN f - domain of function[f EXCEPT ![x] = y] - function update[f EXCEPT ![x] = @ + 1] - update using current value (@)[S -> T] - set of all functions from S to T[]P - always P (invariant)<>P - eventually PP ~> Q - P leads to Q[][A]_v - A or stuttering stepWF_v(A) - weak fairnessSF_v(A) - strong fairnessCHOOSE x \in S : P(x) \* Select arbitrary element satisfying P
LET
localVar == expression
helper(x) == anotherExpression
IN
resultExpression
Always define a TypeInvariant to catch specification bugs early:
TypeInvariant ==
/\ var1 \in SomeSet
/\ var2 \in [Key -> Value]
/\ var3 \subseteq AllowedValues
For modeling state machines:
CONSTANTS States, InitialState
VARIABLES state, data
Init ==
/\ state = InitialState
/\ data = initialData
Transition(from, to) ==
/\ state = from
/\ state' = to
/\ SomeCondition
/\ data' = UpdatedData
Next ==
\/ Transition("idle", "running")
\/ Transition("running", "completed")
\/ Transition("running", "failed")
For multiple concurrent processes:
CONSTANTS Procs \* Set of process IDs
VARIABLES pc, localState
Init ==
/\ pc = [p \in Procs |-> "start"]
/\ localState = [p \in Procs |-> InitialValue]
Step(p) ==
/\ pc[p] = "start"
/\ pc' = [pc EXCEPT ![p] = "next"]
/\ localState' = [localState EXCEPT ![p] = NewValue]
Next == \E p \in Procs : Step(p)
For distributed systems with message passing:
VARIABLES messages \* Set or bag of messages
Send(m) ==
/\ messages' = messages \cup {m}
Receive(m) ==
/\ m \in messages
/\ messages' = messages \ {m}
For systems with transactions:
VARIABLES store, tx, snapshotStore
OpenTx(t) ==
/\ t \notin tx
/\ tx' = tx \cup {t}
/\ snapshotStore' = [snapshotStore EXCEPT ![t] = store]
/\ UNCHANGED store
CommitTx(t) ==
/\ t \in tx
/\ NoConflicts(t) \* Check for conflicts
/\ store' = MergeChanges(store, snapshotStore[t])
/\ tx' = tx \ {t}
\* Mutual exclusion
MutualExclusion == \A i, j \in Procs :
(i /= j) => ~(pc[i] = "cs" /\ pc[j] = "cs")
\* No deadlock
NoDeadlock == ENABLED Next
\* Data integrity
DataIntegrity == \A k \in DOMAIN store : store[k] \in ValidValues
\* Progress
Progress == \A p \in Procs : pc[p] = "waiting" ~> pc[p] = "done"
\* Termination
Termination == <>(\A p \in Procs : pc[p] = "done")
\* Eventual consistency
EventualConsistency == <>(\A r \in Replicas : data[r] = data[CHOOSE x \in Replicas : TRUE])
\* Weak fairness: if action is continuously enabled, it eventually occurs
FairSpec == Spec /\ WF_vars(SomeAction)
\* Strong fairness: if action is repeatedly enabled, it eventually occurs
StrongFairSpec == Spec /\ SF_vars(SomeAction)
Create a .cfg file to configure TLC model checker:
\* Specify constants
CONSTANTS
NumProcesses = 3
MaxValue = 10
\* Or use model values for uninterpreted sets
CONSTANTS
Procs = {p1, p2, p3}
\* Specify the specification to check
SPECIFICATION Spec
\* Invariants to check (safety properties)
INVARIANTS
TypeInvariant
MutualExclusion
NoDeadlock
\* Properties to check (can include liveness)
PROPERTIES
Termination
\* Symmetry optimization (if applicable)
SYMMETRY Permutations
For detailed syntax reference, see syntax-reference.md For more example patterns, see patterns-examples.md For TLC configuration details, see tlc-configuration.md
Ask clarifying questions about:
Structure the specification:
Create corresponding .cfg file for TLC model checking
Suggest appropriate constant values for model checking