tla-specification

What this skill does

# 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:

1. **Invoke `docs-management` skill** for formal methods patterns
2. **Verify TLA+ syntax** via MCP servers (perplexity for latest practices)
3. **Base all guidance on Leslie Lamport's TLA+ documentation**

## Why TLA+?

TLA+ enables:

1. **Precise Design**: Mathematical precision in system design
2. **Early Bug Detection**: Find concurrency bugs before coding
3. **Model Checking**: Exhaustive verification with TLC
4. **Documentation**: Executable specifications that document intent
5. **Industry Adoption**: Used by Amazon (AWS), Microsoft, MongoDB, etc.

## TLA+ Structure

### Basic Module Template

```tla
--------------------------- 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,