TLA+ — 18 Operations for AI Agents
TLA+ specifications are where distributed systems get proven before they get built — invariants, temporal properties, model-checked designs. act101 navigates modules and definitions structurally, so agents read specifications with the rigor they were written in.
This page is the canonical reference an AI coding agent uses to refactor, query, and analyze TLA+ code through the act MCP server. 18 operations available: 0 refactor, 18 query, 0 analysis. Each operation is callable from Claude Code, Cursor, Codex, OpenCode, or any MCP-compatible agent host. Click any operation for a stable anchor link suitable for citation.
Worked TLA+ examples
act101 reads a TLA+ module's header, operator/function definitions, module instance aliases, VARIABLES/CONSTANTS declarations, and named THEOREM/ASSUMPTION statements as declarations. skeleton tags the module header class, every operator and function definition function, each declared variable/constant variable/constant, and a named theorem block — TLA+ has no dedicated theorem kind in the vocabulary, so it falls to the catch-all. symbols covers the same set except the module header itself, and labels that same theorem unknown rather than block for the identical node. The unit of structure in this grammar is the top-level operator or declaration: neither query descends into an operator's own conjunction list or bound variables. Each example below is the verbatim output of the command shown, run against the file shown. Query outputs are pretty-printed with the timing block omitted.
Read the module's declarations, operators, and theorem as a skeleton
Mutex.tla specifies mutual exclusion over a set of Procs: two state variables, pc and holder, five operators — Init, Request, Enter, Exit, Next — plus Spec and the MutualExclusion invariant, and a named theorem, MutexSafety, tying them together.
$ act query skeleton Mutex.tlaBefore
---------------------------- MODULE Mutex ----------------------------
EXTENDS Naturals
CONSTANTS Procs
VARIABLES pc, holder
Init == /\ pc = [p \in Procs |-> "idle"]
/\ holder = "none"
Request(p) == /\ pc[p] = "idle"
/\ pc' = [pc EXCEPT ![p] = "waiting"]
/\ UNCHANGED holder
Enter(p) == /\ pc[p] = "waiting"
/\ holder = "none"
/\ pc' = [pc EXCEPT ![p] = "critical"]
/\ holder' = p
Exit(p) == /\ pc[p] = "critical"
/\ pc' = [pc EXCEPT ![p] = "idle"]
/\ holder' = "none"
Next == \E p \in Procs : Request(p) \/ Enter(p) \/ Exit(p)
Spec == Init /\ [][Next]_<<pc, holder>>
MutualExclusion == \A p, q \in Procs :
(pc[p] = "critical" /\ pc[q] = "critical") => p = q
THEOREM MutexSafety == Spec => []MutualExclusion
=============================================================================Output
{
"type": "Skeleton",
"declarations": [
{
"kind": "class",
"name": "Mutex",
"range": {
"start": {
"file": "Mutex.tla",
"line": 1,
"column": 1,
"byte_offset": 0
},
"end": {
"file": "Mutex.tla",
"line": 32,
"column": 78,
"byte_offset": 911
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 1,
"column": 37,
"byte_offset": 36
},
"end": {
"file": "Mutex.tla",
"line": 1,
"column": 42,
"byte_offset": 41
}
}
},
{
"kind": "constant",
"name": "Procs",
"range": {
"start": {
"file": "Mutex.tla",
"line": 4,
"column": 1,
"byte_offset": 89
},
"end": {
"file": "Mutex.tla",
"line": 4,
"column": 16,
"byte_offset": 104
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 4,
"column": 11,
"byte_offset": 99
},
"end": {
"file": "Mutex.tla",
"line": 4,
"column": 16,
"byte_offset": 104
}
}
},
{
"kind": "variable",
"name": "pc",
"range": {
"start": {
"file": "Mutex.tla",
"line": 6,
"column": 1,
"byte_offset": 106
},
"end": {
"file": "Mutex.tla",
"line": 6,
"column": 21,
"byte_offset": 126
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 6,
"column": 11,
"byte_offset": 116
},
"end": {
"file": "Mutex.tla",
"line": 6,
"column": 13,
"byte_offset": 118
}
}
},
{
"kind": "variable",
"name": "holder",
"range": {
"start": {
"file": "Mutex.tla",
"line": 6,
"column": 1,
"byte_offset": 106
},
"end": {
"file": "Mutex.tla",
"line": 6,
"column": 21,
"byte_offset": 126
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 6,
"column": 15,
"byte_offset": 120
},
"end": {
"file": "Mutex.tla",
"line": 6,
"column": 21,
"byte_offset": 126
}
}
},
{
"kind": "function",
"name": "Init",
"range": {
"start": {
"file": "Mutex.tla",
"line": 8,
"column": 1,
"byte_offset": 128
},
"end": {
"file": "Mutex.tla",
"line": 11,
"column": 1,
"byte_offset": 197
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 8,
"column": 1,
"byte_offset": 128
},
"end": {
"file": "Mutex.tla",
"line": 8,
"column": 5,
"byte_offset": 132
}
}
},
{
"kind": "function",
"name": "Request",
"range": {
"start": {
"file": "Mutex.tla",
"line": 11,
"column": 1,
"byte_offset": 197
},
"end": {
"file": "Mutex.tla",
"line": 15,
"column": 1,
"byte_offset": 316
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 11,
"column": 1,
"byte_offset": 197
},
"end": {
"file": "Mutex.tla",
"line": 11,
"column": 8,
"byte_offset": 204
}
}
},
{
"kind": "function",
"name": "Enter",
"range": {
"start": {
"file": "Mutex.tla",
"line": 15,
"column": 1,
"byte_offset": 316
},
"end": {
"file": "Mutex.tla",
"line": 20,
"column": 1,
"byte_offset": 459
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 15,
"column": 1,
"byte_offset": 316
},
"end": {
"file": "Mutex.tla",
"line": 15,
"column": 6,
"byte_offset": 321
}
}
},
{
"kind": "function",
"name": "Exit",
"range": {
"start": {
"file": "Mutex.tla",
"line": 20,
"column": 1,
"byte_offset": 459
},
"end": {
"file": "Mutex.tla",
"line": 24,
"column": 1,
"byte_offset": 570
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 20,
"column": 1,
"byte_offset": 459
},
"end": {
"file": "Mutex.tla",
"line": 20,
"column": 5,
"byte_offset": 463
}
}
},
{
"kind": "function",
"name": "Next",
"range": {
"start": {
"file": "Mutex.tla",
"line": 24,
"column": 1,
"byte_offset": 570
},
"end": {
"file": "Mutex.tla",
"line": 24,
"column": 59,
"byte_offset": 628
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 24,
"column": 1,
"byte_offset": 570
},
"end": {
"file": "Mutex.tla",
"line": 24,
"column": 5,
"byte_offset": 574
}
}
},
{
"kind": "function",
"name": "Spec",
"range": {
"start": {
"file": "Mutex.tla",
"line": 26,
"column": 1,
"byte_offset": 630
},
"end": {
"file": "Mutex.tla",
"line": 26,
"column": 40,
"byte_offset": 669
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 26,
"column": 1,
"byte_offset": 630
},
"end": {
"file": "Mutex.tla",
"line": 26,
"column": 5,
"byte_offset": 634
}
}
},
{
"kind": "function",
"name": "MutualExclusion",
"range": {
"start": {
"file": "Mutex.tla",
"line": 28,
"column": 1,
"byte_offset": 671
},
"end": {
"file": "Mutex.tla",
"line": 29,
"column": 74,
"byte_offset": 783
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 28,
"column": 1,
"byte_offset": 671
},
"end": {
"file": "Mutex.tla",
"line": 28,
"column": 16,
"byte_offset": 686
}
}
},
{
"kind": "block",
"name": "MutexSafety",
"range": {
"start": {
"file": "Mutex.tla",
"line": 31,
"column": 1,
"byte_offset": 785
},
"end": {
"file": "Mutex.tla",
"line": 31,
"column": 49,
"byte_offset": 833
}
},
"name_range": {
"start": {
"file": "Mutex.tla",
"line": 31,
"column": 9,
"byte_offset": 793
},
"end": {
"file": "Mutex.tla",
"line": 31,
"column": 20,
"byte_offset": 804
}
}
}
]
}The skeleton reports twelve declarations: the Mutex module header as class, Procs as constant, pc/holder as variable, Init through MutualExclusion all as function, and MutexSafety as block — TLA+'s catch-all kind for a named theorem.
List every operator, variable, and the theorem as symbols
Next composes Request, Enter, and Exit under existential quantification over Procs; Spec closes Init under Next with a stuttering step on <<pc, holder>>.
$ act query symbols Mutex.tlaBefore
---------------------------- MODULE Mutex ----------------------------
EXTENDS Naturals
CONSTANTS Procs
VARIABLES pc, holder
Init == /\ pc = [p \in Procs |-> "idle"]
/\ holder = "none"
Request(p) == /\ pc[p] = "idle"
/\ pc' = [pc EXCEPT ![p] = "waiting"]
/\ UNCHANGED holder
Enter(p) == /\ pc[p] = "waiting"
/\ holder = "none"
/\ pc' = [pc EXCEPT ![p] = "critical"]
/\ holder' = p
Exit(p) == /\ pc[p] = "critical"
/\ pc' = [pc EXCEPT ![p] = "idle"]
/\ holder' = "none"
Next == \E p \in Procs : Request(p) \/ Enter(p) \/ Exit(p)
Spec == Init /\ [][Next]_<<pc, holder>>
MutualExclusion == \A p, q \in Procs :
(pc[p] = "critical" /\ pc[q] = "critical") => p = q
THEOREM MutexSafety == Spec => []MutualExclusion
=============================================================================Output
{
"type": "Symbols",
"symbols": [
{
"name": "Procs",
"kind": "constant",
"range": {
"start": {
"file": "Mutex.tla",
"line": 4,
"column": 11,
"byte_offset": 99
},
"end": {
"file": "Mutex.tla",
"line": 4,
"column": 16,
"byte_offset": 104
}
},
"visibility": "unknown"
},
{
"name": "pc",
"kind": "variable",
"range": {
"start": {
"file": "Mutex.tla",
"line": 6,
"column": 11,
"byte_offset": 116
},
"end": {
"file": "Mutex.tla",
"line": 6,
"column": 13,
"byte_offset": 118
}
},
"visibility": "unknown"
},
{
"name": "holder",
"kind": "variable",
"range": {
"start": {
"file": "Mutex.tla",
"line": 6,
"column": 15,
"byte_offset": 120
},
"end": {
"file": "Mutex.tla",
"line": 6,
"column": 21,
"byte_offset": 126
}
},
"visibility": "unknown"
},
{
"name": "Init",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 8,
"column": 1,
"byte_offset": 128
},
"end": {
"file": "Mutex.tla",
"line": 8,
"column": 5,
"byte_offset": 132
}
},
"visibility": "unknown"
},
{
"name": "Request",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 11,
"column": 1,
"byte_offset": 197
},
"end": {
"file": "Mutex.tla",
"line": 11,
"column": 8,
"byte_offset": 204
}
},
"visibility": "unknown"
},
{
"name": "Enter",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 15,
"column": 1,
"byte_offset": 316
},
"end": {
"file": "Mutex.tla",
"line": 15,
"column": 6,
"byte_offset": 321
}
},
"visibility": "unknown"
},
{
"name": "Exit",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 20,
"column": 1,
"byte_offset": 459
},
"end": {
"file": "Mutex.tla",
"line": 20,
"column": 5,
"byte_offset": 463
}
},
"visibility": "unknown"
},
{
"name": "Next",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 24,
"column": 1,
"byte_offset": 570
},
"end": {
"file": "Mutex.tla",
"line": 24,
"column": 5,
"byte_offset": 574
}
},
"visibility": "unknown"
},
{
"name": "Spec",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 26,
"column": 1,
"byte_offset": 630
},
"end": {
"file": "Mutex.tla",
"line": 26,
"column": 5,
"byte_offset": 634
}
},
"visibility": "unknown"
},
{
"name": "MutualExclusion",
"kind": "function",
"range": {
"start": {
"file": "Mutex.tla",
"line": 28,
"column": 1,
"byte_offset": 671
},
"end": {
"file": "Mutex.tla",
"line": 28,
"column": 16,
"byte_offset": 686
}
},
"visibility": "unknown"
},
{
"name": "MutexSafety",
"kind": "unknown",
"range": {
"start": {
"file": "Mutex.tla",
"line": 31,
"column": 9,
"byte_offset": 793
},
"end": {
"file": "Mutex.tla",
"line": 31,
"column": 20,
"byte_offset": 804
}
},
"visibility": "unknown"
}
]
}symbols drops the module header itself, for eleven entries, and reports every operator and variable with the same kind the skeleton showed — except MutexSafety, which comes back kind: unknown instead of block for the identical theorem node.
Query
18 query tools, the same on every supported language. Descriptions live in the shared reference: /docs/query-tools.
callers control_flow data_flow definition diagnostics effect_closure effect_summary fix_auto get_type graph import_organize interface mutations references repo_outline skeleton symbols symbols_batch