majiayu000 TLA+ Specification Skill
When to Use This Skill
Use this skill when:
- Tla Specification tasks - Working on tla+ formal specification language for distributed systems and concurrent algorithms
- Planning or design - Need guidance on Tla Specification approaches
- Best practices - Want to follow established patterns and standards
Overview
TLA+ formal specification language for designing and verifying distributed systems and concurrent algorithms.
MANDATORY: Documentation-First Approach
Before writing TLA+ specifications:
- Invoke
docs-managementskill for formal methods patterns - Verify TLA+ syntax via MCP servers (perplexity for latest practices)
- Base all guidance on Leslie Lamport's TLA+ documentation
Why TLA+?
TLA+ enables:
- Precise Design: Mathematical precision in system design
- Early Bug Detection: Find concurrency bugs before coding
- Model Checking: Exhaustive verification with TLC
- Documentation: Executable specifications that document intent
- Industry Adoption: Used by Amazon (AWS), Microsoft, MongoDB, etc.
TLA+ Structure
Basic Module Template
--------------------------- MODULE OrderWorkflow ---------------------------
\* Order Workflow Specification
\* Models the lifecycle of an order from creation to completion
EXTENDS Integers, Sequences, FiniteSets, TLC
CONSTANTS
MaxOrders, \* Maximum number of concurrent orders
MaxItems, \* Maximum items per order
Customers, \* Set of customer IDs
Products \* Set of product IDs
VARIABLES
orders, \* Function from OrderId -> Order state
inventory, \* Function from ProductId -> quantity
payments, \* Set of processed payment records
notifications \* Sequence of sent notifications
vars == <<orders, inventory, payments, notifications>>
-----------------------------------------------------------------------------
\* Type Definitions
-----------------------------------------------------------------------------
OrderStatus == {"Draft", "Submitted", "Paid", "Shipped", "Delivered", "Cancelled"}
Order == [
id: Nat,
customerId: Customers,
items: SUBSET (Products \X Nat), \* Set of (product, quantity) pairs
status: OrderStatus,
total: Nat
]
TypeInvariant ==
/\ orders \in [SUBSET Nat -> Order \cup {NULL}]
/\ inventory \in [Products -> Nat]
/\ payments \in SUBSET [orderId: Nat, amount: Nat, timestamp: Nat]
/\ notifications \in Seq([type: STRING, orderId: Nat])
-----------------------------------------------------------------------------
\* Initial State
-----------------------------------------------------------------------------
Init ==
/\ orders = [o \in {} |-> NULL]
/\ inventory = [p \in Products |-> 100] \* Start with 100 of each
/\ payments = {}
/\ notifications = <<>>
-----------------------------------------------------------------------------
\* Actions
-----------------------------------------------------------------------------
\* Create a new draft order
CreateOrder(customerId, orderId) ==
/\ orderId \notin DOMAIN orders
/\ Cardinality(DOMAIN orders) < MaxOrders
/\ orders' = orders @@ (orderId :> [
id |-> orderId,
customerId |-> customerId,
items |-> {},
status |-> "Draft",
total |-> 0
])
/\ UNCHANGED <<inventory, payments, notifications>>
\* Add item to draft order
AddItem(orderId, productId, quantity) ==
/\ orderId \in DOMAIN orders
/\ orders[orderId].status = "Draft"
/\ quantity > 0
/\ quantity <= inventory[productId]
/\ Cardinality(orders[orderId].items) < MaxItems
/\ orders' = [orders EXCEPT
![orderId].items = @ \cup {<<productId, quantity>>},
![orderId].total = @ + (quantity * 10)] \* Simplified pricing
/\ UNCHANGED <<inventory, payments, notifications>>
\* Submit order for processing
SubmitOrder(orderId) ==
/\ orderId \in DOMAIN orders
/\ orders[orderId].status = "Draft"
/\ orders[orderId].items /= {}
\* Reserve inventory
/\ \A <<p, q>> \in orders[orderId].items : inventory[p] >= q
/\ orders' = [orders EXCEPT ![orderId].status = "Submitted"]
/\ inventory' = [p \in Products |->
inventory[p] - Sum({q : <<prod, q>> \in orders[orderId].items, prod = p})]
/\ notifications' = Append(notifications,
[type |-> "OrderSubmitted", orderId |-> orderId])
/\ UNCHANGED <<payments>>
\* Process payment
ProcessPayment(orderId, amount) ==
/\ orderId \in DOMAIN orders
/\ orders[orderId].status = "Submitted"
/\ amount = orders[orderId].total
/\ payments' = payments \cup {[orderId |-> orderId, amount |-> amount, timestamp |-> 0]}
/\ orders' = [orders EXCEPT ![orderId].status = "Paid"]
/\ notifications' = Append(notifications,
[type |-> "PaymentReceived", orderId |-> orderId])
/\ UNCHANGED <<inventory>>
\* Ship order
ShipOrder(orderId) ==
/\ orderId \in DOMAIN orders
/\ orders[orderId].status = "Paid"
/\ orders' = [orders EXCEPT ![orderId].status = "Shipped"]
/\ notifications' = Append(notifications,
[type |-> "OrderShipped", orderId |-> orderId])
/\ UNCHANGED <<inventory, payments>>
\* Deliver order
DeliverOrder(orderId) ==
/\ orderId \in DOMAIN orders
/\ orders[orderId].status = "Shipped"
/\ orders' = [orders EXCEPT ![orderId].status = "Delivered"]
/\ notifications' = Append(notifications,
[type |-> "OrderDelivered", orderId |-> orderId])
/\ UNCHANGED <<inventory, payments>>
\* Cancel order (only draft or submitted)
CancelOrder(orderId) ==
/\ orderId \in DOMAIN orders
/\ orders[orderId].status \in {"Draft", "Submitted"}
/\ orders' = [orders EXCEPT ![orderId].status = "Cancelled"]
\* Return inventory if was submitted
/\ inventory' = IF orders[orderId].status = "Submitted"
THEN [p \in Products |->
inventory[p] + Sum({q : <<prod, q>> \in orders[orderId].items, prod = p})]
ELSE inventory
/\ notifications' = Append(notifications,
[type |-> "OrderCancelled", orderId |-> orderId])
/\ UNCHANGED <<payments>>
-----------------------------------------------------------------------------
\* Next State Relation
-----------------------------------------------------------------------------
Next ==
\/ \E c \in Customers, o \in 1..MaxOrders : CreateOrder(c, o)
\/ \E o \in DOMAIN orders, p \in Products, q \in 1..5 : AddItem(o, p, q)
\/ \E o \in DOMAIN orders : SubmitOrder(o)
\/ \E o \in DOMAIN orders : ProcessPayment(o, orders[o].total)
\/ \E o \in DOMAIN orders : ShipOrder(o)
\/ \E o \in DOMAIN orders : DeliverOrder(o)
\/ \E o \in DOMAIN orders : CancelOrder(o)
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
\* Safety Properties
-----------------------------------------------------------------------------
\* No negative inventory
InventoryNonNegative ==
\A p \in Products : inventory[p] >= 0
\* Order status transitions are valid
ValidStatusTransitions ==
\A o \in DOMAIN orders :
LET status == orders[o].status
IN status \in OrderStatus
\* Payment only for submitted orders
PaymentOnlyForSubmitted ==
\A p \in payments :
p.orderId \in DOMAIN orders
\* No double payments
NoDoublePayment ==
\A p1, p2 \in payments :
p1.orderId = p2.orderId => p1 = p2
-----------------------------------------------------------------------------
\* Liveness Properties
-----------------------------------------------------------------------------
\* Every submitted order eventually completes (delivered or cancelled)
EventualCompletion ==
\A o \in DOMAIN orders :
orders[o].status = "Submitted" ~>
orders[o].status \in {"Delivered", "Cancelled"}
\* If payment succeeds, order eventually ships
PaymentLeadsToShipment ==
\A o \in DOMAIN orders :
orders[o].status = "Paid" ~> orders[o].status = "Shipped"
-----------------------------------------------------------------------------
\* Helper Functions
-----------------------------------------------------------------------------
Sum(S) ==
IF S = {} THEN 0
ELSE LET x == CHOOSE x \in S : TRUE
IN x + Sum(S \ {x})
NULL == CHOOSE n : n \notin Order
=============================================================================
PlusCal
PlusCal is an algorithm language that compiles to TLA+:
PlusCal Example
--------------------------- MODULE DistributedLock ---------------------------
EXTENDS Integers, Sequences, TLC
CONSTANTS Nodes, NULL
(*--algorithm distributed_lock
variables
lock = NULL, \* Current lock holder
requests = [n \in Nodes |-> 0], \* Request timestamps
grants = [n \in Nodes |-> FALSE];
define
\* Safety: At most one node holds lock
MutualExclusion ==
\A n1, n2 \in Nodes :
grants[n1] /\ grants[n2] => n1 = n2
\* Liveness: Every request eventually granted
EventuallyGranted ==
\A n \in Nodes :
requests[n] > 0 ~> grants[n]
end define;
fair process Node \in Nodes
variables
myTimestamp = 0;
begin
Request:
myTimestamp := myTimestamp + 1;
requests[self] := myTimestamp;
WaitForLock:
await lock = NULL \/ lock = self;
lock := self;
EnterCriticalSection:
grants[self] := TRUE;
\* Critical section work here
ExitCriticalSection:
grants[self] := FALSE;
lock := NULL;
goto Request;
end process;
end algorithm; *)
\* BEGIN TRANSLATION - Auto-generated by TLA+
\* ... TLA+ translation appears here ...
\* END TRANSLATION
=============================================================================
PlusCal Constructs
variables - Global variable declarations
define - Define operators/invariants
process - Process definition (fair = fair scheduling)
procedure - Reusable procedure
begin/end - Process body
await - Wait for condition
either/or - Non-deterministic choice
while - Loop
if/then/else - Conditional
goto - Jump to label
call - Procedure call
return - Return from procedure
with - Atomic with non-deterministic selection
Common Patterns
Consensus Algorithm
--------------------------- MODULE SimpleConsensus ---------------------------
EXTENDS Integers, FiniteSets
CONSTANTS
Nodes, \* Set of participant nodes
Values, \* Possible values to agree on
Quorum \* Minimum nodes for quorum
VARIABLES
proposed, \* proposed[n] = value proposed by node n
accepted, \* accepted[n] = value accepted by node n
decided \* decided[n] = final decided value (or NULL)
vars == <<proposed, accepted, decided>>
TypeOK ==
/\ proposed \in [Nodes -> Values \cup {NULL}]
/\ accepted \in [Nodes -> Values \cup {NULL}]
/\ decided \in [Nodes -> Values \cup {NULL}]
Init ==
/\ proposed = [n \in Nodes |-> NULL]
/\ accepted = [n \in Nodes |-> NULL]
/\ decided = [n \in Nodes |-> NULL]
\* Node proposes a value
Propose(n, v) ==
/\ proposed[n] = NULL
/\ proposed' = [proposed EXCEPT ![n] = v]
/\ UNCHANGED <<accepted, decided>>
\* Node accepts a proposed value
Accept(n, v) ==
/\ \E m \in Nodes : proposed[m] = v
/\ accepted[n] = NULL
/\ accepted' = [accepted EXCEPT ![n] = v]
/\ UNCHANGED <<proposed, decided>>
\* Node decides if quorum reached
Decide(n) ==
/\ decided[n] = NULL
/\ \E v \in Values :
/\ Cardinality({m \in Nodes : accepted[m] = v}) >= Quorum
/\ decided' = [decided EXCEPT ![n] = v]
/\ UNCHANGED <<proposed, accepted>>
Next ==
\/ \E n \in Nodes, v \in Values : Propose(n, v)
\/ \E n \in Nodes, v \in Values : Accept(n, v)
\/ \E n \in Nodes : Decide(n)
Spec == Init /\ [][Next]_vars
\* Safety: Agreement - all decided values are the same
Agreement ==
\A n1, n2 \in Nodes :
decided[n1] /= NULL /\ decided[n2] /= NULL =>
decided[n1] = decided[n2]
\* Safety: Validity - decided value was proposed
Validity ==
\A n \in Nodes :
decided[n] /= NULL =>
\E m \in Nodes : proposed[m] = decided[n]
=============================================================================
Two-Phase Commit
--------------------------- MODULE TwoPhaseCommit ---------------------------
EXTENDS Integers, FiniteSets
CONSTANTS
Coordinators,
Participants
VARIABLES
coordState, \* Coordinator state
partState, \* Participant states
prepared, \* Set of prepared participants
decision \* Final decision
vars == <<coordState, partState, prepared, decision>>
CoordStates == {"init", "waiting", "committed", "aborted"}
PartStates == {"working", "prepared", "committed", "aborted"}
TypeOK ==
/\ coordState \in CoordStates
/\ partState \in [Participants -> PartStates]
/\ prepared \in SUBSET Participants
/\ decision \in {"pending", "commit", "abort"}
Init ==
/\ coordState = "init"
/\ partState = [p \in Participants |-> "working"]
/\ prepared = {}
/\ decision = "pending"
\* Coordinator sends prepare request
SendPrepare ==
/\ coordState = "init"
/\ coordState' = "waiting"
/\ UNCHANGED <<partState, prepared, decision>>
\* Participant prepares (votes yes)
Prepare(p) ==
/\ partState[p] = "working"
/\ partState' = [partState EXCEPT ![p] = "prepared"]
/\ prepared' = prepared \cup {p}
/\ UNCHANGED <<coordState, decision>>
\* Participant aborts (votes no)
Abort(p) ==
/\ partState[p] = "working"
/\ partState' = [partState EXCEPT ![p] = "aborted"]
/\ UNCHANGED <<coordState, prepared, decision>>
\* Coordinator decides commit (all prepared)
DecideCommit ==
/\ coordState = "waiting"
/\ prepared = Participants
/\ coordState' = "committed"
/\ decision' = "commit"
/\ partState' = [p \in Participants |-> "committed"]
/\ UNCHANGED <<prepared>>
\* Coordinator decides abort (any aborted)
DecideAbort ==
/\ coordState = "waiting"
/\ \E p \in Participants : partState[p] = "aborted"
/\ coordState' = "aborted"
/\ decision' = "abort"
/\ partState' = [p \in Participants |->
IF partState[p] = "prepared" THEN "aborted" ELSE partState[p]]
/\ UNCHANGED <<prepared>>
Next ==
\/ SendPrepare
\/ \E p \in Participants : Prepare(p)
\/ \E p \in Participants : Abort(p)
\/ DecideCommit
\/ DecideAbort
Spec == Init /\ [][Next]_vars
\* Safety: Atomicity - all participants reach same decision
Atomicity ==
decision /= "pending" =>
\A p \in Participants :
(decision = "commit" => partState[p] = "committed") /\
(decision = "abort" => partState[p] \in {"aborted", "working"})
=============================================================================
TLC Model Checking
Configuration File (.cfg)
SPECIFICATION Spec
\* Constants
CONSTANTS
Nodes = {n1, n2, n3}
Values = {v1, v2}
Quorum = 2
NULL = NULL
\* Invariants to check
INVARIANT TypeOK
INVARIANT Agreement
INVARIANT Validity
\* Liveness properties
PROPERTY EventuallyDecided
\* Constraints for bounded model checking
CONSTRAINT StateConstraint
\* Symmetry for optimization
SYMMETRY Symmetry
Running TLC
# Command-line TLC
java -jar tla2tools.jar -config Spec.cfg Spec.tla
# With workers for parallelism
java -jar tla2tools.jar -workers 4 -config Spec.cfg Spec.tla
# Generate trace on error
java -jar tla2tools.jar -dump dot,colorize states.dot Spec.tla
Temporal Operators
[]P - Always P (invariant)
<>P - Eventually P
P ~> Q - P leads to Q (if P then eventually Q)
[]<>P - Infinitely often P
<>[]P - Eventually always P
P /\ Q - P and Q
P \/ Q - P or Q
~P - Not P
P => Q - P implies Q
ENABLED A - Action A is enabled
[A]_v - A or v unchanged
<<A>>_v - A and v changes
WF_v(A) - Weak fairness
SF_v(A) - Strong fairness
Integration with C#
// Specification-driven design: implement to match TLA+ spec
public enum OrderStatus
{
Draft,
Submitted,
Paid,
Shipped,
Delivered,
Cancelled
}
// State machine matching TLA+ transitions
public sealed class Order
{
private static readonly Dictionary<(OrderStatus From, string Action), OrderStatus> _transitions = new()
{
// Matches TLA+ SubmitOrder action
{ (OrderStatus.Draft, "Submit"), OrderStatus.Submitted },
// Matches TLA+ ProcessPayment action
{ (OrderStatus.Submitted, "Pay"), OrderStatus.Paid },
// Matches TLA+ ShipOrder action
{ (OrderStatus.Paid, "Ship"), OrderStatus.Shipped },
// Matches TLA+ DeliverOrder action
{ (OrderStatus.Shipped, "Deliver"), OrderStatus.Delivered },
// Matches TLA+ CancelOrder action
{ (OrderStatus.Draft, "Cancel"), OrderStatus.Cancelled },
{ (OrderStatus.Submitted, "Cancel"), OrderStatus.Cancelled },
};
public OrderStatus Status { get; private set; } = OrderStatus.Draft;
public Result Transition(string action)
{
if (!_transitions.TryGetValue((Status, action), out var newStatus))
return Result.Failure($"Invalid transition: {Status} -> {action}");
Status = newStatus;
return Result.Success();
}
}
// Invariant checking in tests (matches TLA+ safety properties)
public class OrderInvariantTests
{
[Fact]
public void InventoryNonNegative_IsAlwaysTrue()
{
// Simulates TLA+ model checking for InventoryNonNegative
var inventory = new Dictionary<string, int>();
// ... run through state space
Assert.All(inventory.Values, qty => Assert.True(qty >= 0));
}
}
Workflow
When creating TLA+ specifications:
- Identify State: What variables define system state?
- Define Types: What are valid values for each variable?
- Specify Init: What is the initial state?
- Define Actions: What state transitions are possible?
- Write Invariants: What must always be true (safety)?
- Write Liveness: What must eventually happen?
- Model Check: Run TLC to verify properties
- Refine: Add detail or fix discovered bugs
Best Practices
- Start Simple: Begin with minimal spec, add complexity gradually
- Check Types First: TypeOK should pass before complex properties
- Use Constants: Parameterize for easy model size adjustment
- Add Constraints: Bound state space for tractable checking
- Symmetry: Exploit symmetry to reduce state space
- Trace Errors: Use TLC traces to understand failures
- Document Intent: Comments explain why, not what
References
For detailed guidance:
Last Updated: 2025-12-26