| Document editorial workflow with a typed (sum-type) state machine | 59 | a state machine, a sum type |
| An elevator door + motion interlock | 60 | a state machine |
| Multi-step expense-approval workflow with guarded transitions | 81 | a state machine, a memory invariant, require / fail |
| Online game-match lifecycle | 81 | a state machine, a memory invariant, match |
| A media-player transport state machine | 57 | a state machine, a sum type |
| Order lifecycle as a typed state machine | 58 | a state machine, a sum type |
| Parcel shipment tracking with a delivery-exception loop | 67 | a state machine |
| Subscription billing state machine | 93 | a state machine, a memory invariant |
| Support-ticket lifecycle with a reopen path | 60 | a state machine |
| A simplified TCP connection state machine (active-open path) | 58 | a state machine, a sum type |
| An HVAC thermostat control loop | 75 | a state machine, require / fail |
| A two-road traffic-light interlock proven safe by construction | 62 | a state machine, match |
| A coin-operated turnstile — the textbook two-state machine, plus an out-of-service state reachable only via maintenance | 77 | a state machine |
| A vending machine state machine | 89 | a state machine, a memory invariant, require / fail |
| Wildcard failure — `* -> failed` with an `eventually` property | 68 | a state machine, a memory invariant, guard blocks, require / fail |