Rigor
                      ▲
                      │
    Theorem Provers   │   Coq, Isabelle/HOL, Lean
    (Full proofs)     │   ────────────────────────
                      │
    Model Checking    │   TLA+, Alloy, SPIN
    (Exhaustive)      │   ────────────────────────
                      │
    Property Testing  │   QuickCheck, Hypothesis
    (Randomized)      │   ────────────────────────
                      │
    Unit Testing      │   JUnit, pytest
    (Examples)        │
                      └──────────────────────────▶ Ease of Use

State₀ → State₁ → State₂ → State₃ → ...

---- MODULE Counter ----
VARIABLE count

Init == count = 0

Increment == count' = count + 1

Decrement == count > 0 /\ count' = count - 1

Next == Increment \/ Decrement

Spec == Init /\ [][Next]_count
====

\* Safety: Account balance never goes negative
TypeInvariant == balance >= 0

\* Liveness: Every withdrawal request eventually completes
Liveness == \A r \in requests : <>(r.completed)

┌────────────────────────────────────────────────────┐
│                  State Space                        │
│                                                     │
│    S₀ ──▶ S₁ ──▶ S₄                               │
│     │      │      │                                 │
│     ▼      ▼      ▼                                 │
│    S₂ ──▶ S₃ ──▶ S₅ ◀── Invariant violation!      │
│                  ▲                                  │
│                  │                                  │
│           Error trace provided                      │
│                                                     │
└────────────────────────────────────────────────────┘

---- MODULE TransferPlusCal ----
EXTENDS Integers, TLC

CONSTANTS Accounts, InitBalance

(*--algorithm Transfer
variables
    balance = [a \in Accounts |-> InitBalance];

define
    TotalConstant ==
        LET Sum(S) == IF S = {} THEN 0
                      ELSE LET x == CHOOSE x \in S : TRUE
                           IN balance[x] + Sum(S \ {x})
        IN Sum(Accounts) = Cardinality(Accounts) * InitBalance
end define;

process Transfer \in 1..3
variables from, to, amount;
begin
    ChooseAccounts:
        from := CHOOSE a \in Accounts : TRUE;
        to := CHOOSE a \in Accounts : a /= from;
        amount := CHOOSE n \in 1..balance[from] : TRUE;
    DoTransfer:
        if balance[from] >= amount then
            balance[from] := balance[from] - amount;
            balance[to] := balance[to] + amount;
        end if;
end process;

end algorithm; *)
====

---- MODULE TwoPhaseCommit ----
EXTENDS Integers, FiniteSets

CONSTANTS RM  \* Resource Managers

VARIABLES
    rmState,      \* State of each RM
    tmState,      \* State of Transaction Manager
    tmPrepared,   \* RMs that have prepared
    msgs          \* Messages in transit

vars == <<rmState, tmState, tmPrepared, msgs>>

Message == [type: {"Prepare", "Commit", "Abort", "Prepared", "Aborted"}]

TypeOK ==
    /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
    /\ tmState \in {"init", "preparing", "committed", "aborted"}
    /\ tmPrepared \subseteq RM
    /\ msgs \subseteq Message

Init ==
    /\ rmState = [r \in RM |-> "working"]
    /\ tmState = "init"
    /\ tmPrepared = {}
    /\ msgs = {}

\* Transaction Manager sends Prepare to all RMs
TMPrepare ==
    /\ tmState = "init"
    /\ tmState' = "preparing"
    /\ msgs' = msgs \cup {[type |-> "Prepare"]}
    /\ UNCHANGED <<rmState, tmPrepared>>

\* RM receives Prepare and responds
RMPrepare(r) ==
    /\ rmState[r] = "working"
    /\ [type |-> "Prepare"] \in msgs
    /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
    /\ msgs' = msgs \cup {[type |-> "Prepared"]}
    /\ UNCHANGED <<tmState, tmPrepared>>

\* RM can choose to abort
RMChooseAbort(r) ==
    /\ rmState[r] = "working"
    /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
    /\ msgs' = msgs \cup {[type |-> "Aborted"]}
    /\ UNCHANGED <<tmState, tmPrepared>>

\* TM receives Prepared from RM
TMRcvPrepared(r) ==
    /\ tmState = "preparing"
    /\ [type |-> "Prepared"] \in msgs
    /\ tmPrepared' = tmPrepared \cup {r}
    /\ IF tmPrepared' = RM
       THEN /\ tmState' = "committed"
            /\ msgs' = msgs \cup {[type |-> "Commit"]}
       ELSE /\ UNCHANGED tmState
            /\ UNCHANGED msgs
    /\ UNCHANGED rmState

\* TM receives Aborted and aborts transaction
TMRcvAborted ==
    /\ tmState = "preparing"
    /\ [type |-> "Aborted"] \in msgs
    /\ tmState' = "aborted"
    /\ msgs' = msgs \cup {[type |-> "Abort"]}
    /\ UNCHANGED <<rmState, tmPrepared>>

\* RM commits
RMCommit(r) ==
    /\ rmState[r] = "prepared"
    /\ [type |-> "Commit"] \in msgs
    /\ rmState' = [rmState EXCEPT ![r] = "committed"]
    /\ UNCHANGED <<tmState, tmPrepared, msgs>>

\* RM aborts
RMAbort(r) ==
    /\ rmState[r] \in {"working", "prepared"}
    /\ [type |-> "Abort"] \in msgs
    /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
    /\ UNCHANGED <<tmState, tmPrepared, msgs>>

Next ==
    \/ TMPrepare
    \/ TMRcvAborted
    \/ \E r \in RM :
        \/ RMPrepare(r)
        \/ RMChooseAbort(r)
        \/ TMRcvPrepared(r)
        \/ RMCommit(r)
        \/ RMAbort(r)

\* Safety: No RM commits if any RM aborts
Consistency ==
    \A r1, r2 \in RM :
        ~ (rmState[r1] = "committed" /\ rmState[r2] = "aborted")

Spec == Init /\ [][Next]_vars

THEOREM Spec => []Consistency
====

---- MODULE DistributedLock ----
EXTENDS Integers, Naturals

CONSTANTS
    Nodes,        \* Set of nodes
    MaxTime       \* Maximum simulation time

VARIABLES
    lock,         \* Current lock holder (or "none")
    leaseEnd,     \* When current lease expires
    time,         \* Global logical time
    requests      \* Pending lock requests

vars == <<lock, leaseEnd, time, requests>>

TypeOK ==
    /\ lock \in Nodes \cup {"none"}
    /\ leaseEnd \in 0..MaxTime
    /\ time \in 0..MaxTime
    /\ requests \subseteq Nodes

Init ==
    /\ lock = "none"
    /\ leaseEnd = 0
    /\ time = 0
    /\ requests = {}

\* Node requests the lock
Request(n) ==
    /\ n \notin requests
    /\ requests' = requests \cup {n}
    /\ UNCHANGED <<lock, leaseEnd, time>>

\* Lock is granted with a lease
Grant(n, duration) ==
    /\ n \in requests
    /\ \/ lock = "none"
       \/ time >= leaseEnd  \* Lease expired
    /\ lock' = n
    /\ leaseEnd' = time + duration
    /\ requests' = requests \ {n}
    /\ UNCHANGED time

\* Node releases lock early
Release(n) ==
    /\ lock = n
    /\ lock' = "none"
    /\ leaseEnd' = time
    /\ UNCHANGED <<time, requests>>

\* Time advances
Tick ==
    /\ time < MaxTime
    /\ time' = time + 1
    /\ UNCHANGED <<lock, leaseEnd, requests>>

\* Lease expires
Expire ==
    /\ lock /= "none"
    /\ time >= leaseEnd
    /\ lock' = "none"
    /\ UNCHANGED <<leaseEnd, time, requests>>

Next ==
    \/ \E n \in Nodes : Request(n)
    \/ \E n \in Nodes, d \in 1..5 : Grant(n, d)
    \/ \E n \in Nodes : Release(n)
    \/ Tick
    \/ Expire

\* Safety: At most one node holds the lock at any time
MutualExclusion ==
    \A n1, n2 \in Nodes :
        (lock = n1 /\ lock = n2) => n1 = n2

\* Liveness: Every request is eventually granted
EventualGrant ==
    \A n \in Nodes :
        (n \in requests) ~> (lock = n)

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
====

---- MODULE OrderedQueue ----
EXTENDS Sequences, Integers, FiniteSets

CONSTANTS
    Producers,    \* Set of producer processes
    Consumers,    \* Set of consumer processes
    MaxQueueLen   \* Maximum queue length

VARIABLES
    queue,        \* The message queue
    produced,     \* Messages produced by each producer
    consumed,     \* Messages consumed by each consumer
    nextSeq       \* Next sequence number per producer

vars == <<queue, produced, consumed, nextSeq>>

Message == [producer: Producers, seq: Nat, data: Nat]

TypeOK ==
    /\ queue \in Seq(Message)
    /\ Len(queue) <= MaxQueueLen
    /\ produced \in [Producers -> Seq(Message)]
    /\ consumed \in [Consumers -> Seq(Message)]
    /\ nextSeq \in [Producers -> Nat]

Init ==
    /\ queue = <<>>
    /\ produced = [p \in Producers |-> <<>>]
    /\ consumed = [c \in Consumers |-> <<>>]
    /\ nextSeq = [p \in Producers |-> 1]

\* Producer sends a message
Produce(p, data) ==
    /\ Len(queue) < MaxQueueLen
    /\ LET msg == [producer |-> p, seq |-> nextSeq[p], data |-> data]
       IN /\ queue' = Append(queue, msg)
          /\ produced' = [produced EXCEPT ![p] = Append(@, msg)]
          /\ nextSeq' = [nextSeq EXCEPT ![p] = @ + 1]
    /\ UNCHANGED consumed

\* Consumer receives a message (FIFO)
Consume(c) ==
    /\ Len(queue) > 0
    /\ LET msg == Head(queue)
       IN /\ queue' = Tail(queue)
          /\ consumed' = [consumed EXCEPT ![c] = Append(@, msg)]
    /\ UNCHANGED <<produced, nextSeq>>

Next ==
    \/ \E p \in Producers, d \in 1..10 : Produce(p, d)
    \/ \E c \in Consumers : Consume(c)

\* Safety: FIFO ordering is preserved per producer
FIFOOrdering ==
    \A c \in Consumers :
        \A i, j \in 1..Len(consumed[c]) :
            (i < j /\ consumed[c][i].producer = consumed[c][j].producer)
            => consumed[c][i].seq < consumed[c][j].seq

\* Safety: No message duplication
NoDuplication ==
    \A c1, c2 \in Consumers :
        \A i \in 1..Len(consumed[c1]) :
            \A j \in 1..Len(consumed[c2]) :
                (c1 /= c2 \/ i /= j) =>
                    consumed[c1][i] /= consumed[c2][j]

Spec == Init /\ [][Next]_vars

THEOREM Spec => [](FIFOOrdering /\ NoDuplication)
====

---- MODULE RaftLeaderElection ----
EXTENDS Integers, FiniteSets

CONSTANTS
    Server,       \* Set of servers
    MaxTerm       \* Maximum term for model checking

VARIABLES
    currentTerm,  \* Current term for each server
    votedFor,     \* Who this server voted for in current term
    state,        \* follower, candidate, or leader
    votesGranted  \* Votes received by candidates

vars == <<currentTerm, votedFor, state, votesGranted>>

Quorum == {Q \in SUBSET Server : Cardinality(Q) * 2 > Cardinality(Server)}

TypeOK ==
    /\ currentTerm \in [Server -> 0..MaxTerm]
    /\ votedFor \in [Server -> Server \cup {NONE}]
    /\ state \in [Server -> {"follower", "candidate", "leader"}]
    /\ votesGranted \in [Server -> SUBSET Server]

Init ==
    /\ currentTerm = [s \in Server |-> 0]
    /\ votedFor = [s \in Server |-> NONE]
    /\ state = [s \in Server |-> "follower"]
    /\ votesGranted = [s \in Server |-> {}]

\* Server times out and starts election
StartElection(s) ==
    /\ state[s] \in {"follower", "candidate"}
    /\ currentTerm[s] < MaxTerm
    /\ currentTerm' = [currentTerm EXCEPT ![s] = @ + 1]
    /\ state' = [state EXCEPT ![s] = "candidate"]
    /\ votedFor' = [votedFor EXCEPT ![s] = s]
    /\ votesGranted' = [votesGranted EXCEPT ![s] = {s}]

\* Server grants vote to candidate
RequestVote(candidate, voter) ==
    /\ state[candidate] = "candidate"
    /\ currentTerm[candidate] >= currentTerm[voter]
    /\ \/ votedFor[voter] = NONE
       \/ votedFor[voter] = candidate
    /\ currentTerm' = [currentTerm EXCEPT ![voter] = currentTerm[candidate]]
    /\ votedFor' = [votedFor EXCEPT ![voter] = candidate]
    /\ votesGranted' = [votesGranted EXCEPT ![candidate] = @ \cup {voter}]
    /\ state' = [state EXCEPT ![voter] = IF currentTerm[voter] < currentTerm[candidate]
                                          THEN "follower" ELSE @]

\* Candidate wins election
BecomeLeader(s) ==
    /\ state[s] = "candidate"
    /\ votesGranted[s] \in Quorum
    /\ state' = [state EXCEPT ![s] = "leader"]
    /\ UNCHANGED <<currentTerm, votedFor, votesGranted>>

\* Server discovers higher term
StepDown(s, term) ==
    /\ term > currentTerm[s]
    /\ currentTerm' = [currentTerm EXCEPT ![s] = term]
    /\ state' = [state EXCEPT ![s] = "follower"]
    /\ votedFor' = [votedFor EXCEPT ![s] = NONE]
    /\ UNCHANGED votesGranted

Next ==
    \/ \E s \in Server : StartElection(s)
    \/ \E c, v \in Server : RequestVote(c, v)
    \/ \E s \in Server : BecomeLeader(s)
    \/ \E s \in Server, t \in 1..MaxTerm : StepDown(s, t)

\* Safety: At most one leader per term
ElectionSafety ==
    \A s1, s2 \in Server :
        (state[s1] = "leader" /\ state[s2] = "leader" /\
         currentTerm[s1] = currentTerm[s2])
        => s1 = s2

Spec == Init /\ [][Next]_vars

THEOREM Spec => []ElectionSafety
====

# Run model checker from command line
java -jar tla2tools.jar -modelcheck YourSpec.tla

# With configuration file
java -jar tla2tools.jar -modelcheck -config YourSpec.cfg YourSpec.tla

# Distributed mode (multiple workers)
java -jar tla2tools.jar -modelcheck -workers 4 YourSpec.tla

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT Safety
PROPERTY Liveness

CONSTANT
    Nodes = {n1, n2, n3}
    MaxMessages = 5

THEOREM TypeCorrect == Spec => []TypeOK
  <1>1. Init => TypeOK
    BY DEF Init, TypeOK
  <1>2. TypeOK /\ [Next]_vars => TypeOK'
    <2>1. CASE Action1
      BY <2>1 DEF TypeOK, Action1
    <2>2. CASE Action2
      BY <2>2 DEF TypeOK, Action2
    <2>3. CASE UNCHANGED vars
      BY <2>3 DEF TypeOK
    <2>4. QED
      BY <2>1, <2>2, <2>3 DEF Next
  <1>3. QED
    BY <1>1, <1>2, PTL DEF Spec

# Type checking
apalache-mc typecheck YourSpec.tla

# Bounded model checking
apalache-mc check --length=10 YourSpec.tla

# Check specific invariant
apalache-mc check --inv=Safety YourSpec.tla

┌─────────────────────────────────────────────────────────┐
│                   Design Process                        │
│                                                         │
│  Requirements ──▶ Informal Design ──▶ TLA+ Spec         │
│       │                                   │             │
│       │                                   ▼             │
│       │                            Model Checking       │
│       │                                   │             │
│       │              ┌────────────────────┼────────┐    │
│       │              │                    │        │    │
│       │         Bug Found?           Verified      │    │
│       │              │                    │        │    │
│       │              ▼                    ▼        │    │
│       │         Fix Design          Implementation │    │
│       │              │                    │        │    │
│       │              └────────────────────┘        │    │
│       │                                            │    │
│       └────────────────────────────────────────────┘    │
│                                                         │
└─────────────────────────────────────────────────────────┘

# .github/workflows/tla-check.yml
name: TLA+ Model Checking

on:
  push:
    paths:
      - 'specs/**/*.tla'
      - 'specs/**/*.cfg'

jobs:
  model-check:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install TLA+ Tools
        run: |
          wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar

      - name: Run TLC
        run: |
          for spec in specs/*.tla; do
            java -jar tla2tools.jar -modelcheck "$spec"
          done

docs/
├── architecture.md      # High-level overview
├── protocols/
│   ├── replication.tla  # Formal spec
│   ├── replication.cfg  # Model config
│   └── replication.md   # Plain English explanation
└── decisions/
    └── ADR-001-consistency-model.md

---------------------------- MODULE UrnBalls ----------------------------
EXTENDS Naturals

CONSTANTS N, W0  \* total balls, initial white count (W0 <= N)

VARIABLES black, white

Init == /\ white = W0
        /\ black = N - W0

DrawSame == /\ (black + white) > 1
            /\ \/ /\ black >= 2          \* drew BB
                  /\ black' = black - 1  \* remove 2, add 1 black
                  /\ white' = white
               \/ /\ white >= 2          \* drew WW
                  /\ white' = white - 2  \* remove 2 white
                  /\ black' = black + 1  \* add 1 black

DrawDiff == /\ black >= 1
            /\ white >= 1
            /\ black' = black - 1  \* discard the black
            /\ white' = white      \* white survives

Next == DrawSame \/ DrawDiff

ParityInvariant == (white % 2) = (W0 % 2)

Termination == <>(black + white = 1)

LastBallColor == [](black + white = 1 =>
                    IF W0 % 2 = 1 THEN white = 1
                                  ELSE black = 1)
=====================================================================