| Autopilot authority — Aeroflot 593: the half-disconnected autopilot | 108 | a state machine, a memory invariant, try / catch |
| Cabin pressurization — Helios 522: the manual-mode takeoff, unrepresentable | 106 | a state machine, a memory invariant, try / catch |
| Cargo door — Turkish Airlines 981: "indicated locked" is not LOCKED | 116 | a state machine, a memory invariant, try / catch |
| Docking approach — Progress / Mir 1997: abort means ABORT | 116 | a state machine, a memory invariant, try / catch |
| Engine fire bottle — one-shot suppression, fuel off FIRST | 117 | a state machine, a memory invariant, try / catch |
| Fuel crossfeed — Air Transat 236: never feed a leak from the good tank | 118 | a state machine, a memory invariant, try / catch |
| Landing gear — weight-on-wheels interlock, made unrepresentable | 99 | a state machine, a memory invariant, try / catch |
| Launch commit criteria — Challenger: no waiver path to ignition | 127 | a state machine, a memory invariant, try / catch |
| Cryo tank heater — Apollo 13: the thermostat that welded shut | 110 | a state machine, a memory invariant, try / catch |
| Parachute sequence — Genesis: the drogue that never fired | 105 | a state machine, a memory invariant, try / catch |
| Range safety — the flight termination system's three one-way doors | 114 | a state machine, a memory invariant, try / catch |
| Stage separation — the ascent sequence as a proven order | 90 | a state machine, a memory invariant, try / catch |
| Tcas resolution advisory — Überlingen: the opposite maneuver is no state | 121 | a state machine, a memory invariant, try / catch |
| Thrust reverser — Lauda Air 004: in-flight deployment, made structural | 100 | a state machine, a memory invariant, try / catch |
| Unreliable airspeed — AF447: the autopilot never flies on bad data | 105 | a state machine, a memory invariant, try / catch |
| Agent with preconditions and a memory invariant — refuses bad input | 59 | a state machine, a memory invariant, an agent cell, require / fail |
| Campaign finance — the contribution limit lives in the ledger, not the law | 106 | a state machine, a memory invariant, try / catch |
| Census — after certification, the count is history, not a database row | 106 | a state machine, a memory invariant, try / catch |
| Disaster aid — one emergency grant per household, however many times asked | 116 | a state machine, a memory invariant, try / catch |
| Election audit — a risk-limiting audit that cannot count a ballot twice | 117 | a state machine, a memory invariant, try / catch |
| Foia — the statutory clock cannot be silently ignored | 99 | a state machine, a memory invariant, try / catch |
| Grants — budget conservation: the fund cannot award money it does not have | 107 | a state machine, a memory invariant, try / catch |
| Jury — strikes are counted by the bench, not by the honor system | 118 | a state machine, a memory invariant, try / catch |
| Land registry — a parcel cannot be sold to two buyers at once | 110 | a state machine, a memory invariant, try / catch |
| Lottery — committed entries, a published seed, and a draw that closes forever | 96 | a state machine, a memory invariant, try / catch |
| Permit — a building permit that cannot skip a review | 118 | a state machine, a memory invariant, try / catch |
| Petition — one signature per citizen, a wall in memory, not a clerk's eye | 100 | a state machine, a memory invariant, try / catch |
| Procurement — sealed bids stay sealed, and the unsealing ends the auction | 112 | a state machine, a memory invariant, try / catch |
| Sunshine — a council cannot vote on what the public never got to discuss | 135 | a state machine, a memory invariant, try / catch |
| Vital records — a person dies at most once, and benefits know it instantly | 107 | a state machine, a memory invariant, try / catch |
| Backup retention — the floor you cannot prune through | 102 | a state machine, a memory invariant, try / catch |
| Blue/green cutover — there is no state where nobody serves traffic | 114 | a state machine, a memory invariant, try / catch |
| Cert rotation — expiry is an escalation ladder, not a surprise | 108 | a state machine, a memory invariant, try / catch |
| Db migration — applied migrations are immutable history | 104 | a state machine, a memory invariant, try / catch |
| Deploy canary — the staged rollout you cannot skip | 102 | a state machine, a memory invariant, try / catch |
| Dns change control — no record goes live without passing validation | 102 | a state machine, a memory invariant, try / catch |
| Kill switch — a dead flag stays dead | 105 | a state machine, a memory invariant, try / catch |
| Fleet sync — no activation until every node runs the same code | 100 | a state machine, a memory invariant, try / catch |
| Image promotion — nothing unscanned, unsigned, or vulnerable ships | 105 | a state machine, a memory invariant, try / catch |
| Incident ladder — severity only climbs, and closure needs a postmortem | 118 | a state machine, a memory invariant, try / catch |
| Pager escalation — no page resolves without a human acknowledging it | 110 | a state machine, a memory invariant, try / catch |
| Rate limiter — admission control with a quota the memory enforces | 119 | a state machine, a memory invariant, try / catch |
| Secret rotation — a revoked credential never logs in again | 115 | a state machine, a memory invariant, try / catch |
| State lock — two concurrent applies can never both hold the lock | 114 | a state machine, a memory invariant, try / catch |
| Anti-islanding — a solar inverter must never energize a "dead" line | 107 | a state machine, a memory invariant, try / catch |
| Battery dispatch — the charge window is a wall, not a setpoint | 83 | a memory invariant, try / catch |
| Black start — you cannot boot a power plant from a dead grid out of order | 118 | a state machine, a memory invariant, try / catch |
| Recloser — a trip is permanent until a human walks the line | 94 | a state machine, a memory invariant, try / catch |
| Demand response — no payment before measurement, and settlement is final | 124 | a state machine, a memory invariant, try / catch |
| Ev charging — no current before the handshake, no session past the cap | 124 | a state machine, a memory invariant, try / catch |
| Gas turbine light-off — purge before every ignition attempt, no exceptions | 134 | a state machine, a memory invariant, try / catch |
| Generator paralleling — sync-check before the breaker, always | 137 | a state machine, a memory invariant, try / catch |
| Load shedding — the transformer's nameplate is a wall, hospitals shed last | 112 | a memory invariant, try / catch |
| Meter billing — you are billed exactly what the meter read, once | 115 | a state machine, a memory invariant, match, try / catch |
| Spillway gates — a dam may never lose its last release path | 121 | a state machine, a memory invariant, try / catch |
| Spinning reserve — every megawatt you sell must claim real iron | 109 | a memory invariant, try / catch |
| Lockout-tagout — test before touch, and nobody re-energizes over a lock | 137 | a state machine, a memory invariant, try / catch |
| Transformer emergency loading — overload only with every fan running | 134 | a state machine, a memory invariant, try / catch |
| Wind turbine overspeed — after an emergency brake, inspection or nothing | 136 | a state machine, a memory invariant, try / catch |
| Chargeback window — disputes die at day 120, reversals happen exactly once | 109 | a state machine, a memory invariant |
| Client money segregation — the firm can only ever touch its own excess | 100 | a memory invariant |
| All-or-nothing crowdfunding — miss the goal, every backer gets refunded | 120 | a state machine, a memory invariant |
| Dividend distribution — payments can never exceed the declared pool | 96 | a state machine, a memory invariant |
| Delivery-versus-payment — no securities leave before the cash arrives | 111 | a state machine, a memory invariant |
| Invoice factoring — no advance on unverified paper, no double-selling | 108 | a state machine, a memory invariant |
| Letter of credit — the bank pays against verified documents, never trust | 116 | a state machine, a memory invariant |
| Loan amortization — principal never goes negative, never grows back | 100 | a state machine, a memory invariant |
| Milestone escrow — a contractor is paid per accepted milestone, never ahead | 106 | a state machine, a memory invariant |
| Multisig treasury — 2-of-3 distinct approvals, proven before a cent moves | 109 | a state machine, a memory invariant |
| Payroll run — the payslips must sum EXACTLY to the approved total | 100 | a state machine, a memory invariant |
| Security deposit — deductions can never exceed what the tenant paid | 99 | a state machine, a memory invariant |
| Two-party escrow — funds move only when BOTH sides say so, and never leak | 117 | a state machine, a memory invariant |
| Vesting schedule — cliff then linear, and over-vesting is unwritable | 118 | a state machine, a memory invariant |
| Wire dual control — the maker can never be the checker | 98 | a state machine, a memory invariant |
| Monthly budget tracker with a spend cap invariant | 54 | a memory invariant, try / catch |
| Chip/cash ledger with a non-negative balance invariant | 54 | a memory invariant, try / catch |
| FX converter with a rate table in memory and a non-negative rate invariant | 60 | a memory invariant, try / catch |
| Position-limit risk gate. Each symbol's net position must stay within | 59 | a memory invariant, try / catch |
| Auction house — escrowed bids, gold that cannot be printed | 124 | a state machine, a memory invariant, try / catch |
| Battle pass — every tier reward claimed exactly once | 92 | a state machine, a memory invariant, try / catch |
| Battle turns — nobody acts twice, and the dead stay dead | 89 | a state machine, a memory invariant |
| Crafting forge — ingredients consumed exactly once | 98 | a state machine, a memory invariant, try / catch |
| Daily chest — one claim per day, clock tricks be damned | 57 | a state machine, a memory invariant, try / catch |
| Gem store — a purchase receipt credits exactly once | 101 | a state machine, a memory invariant, try / catch |
| Guild bank — the heist needs a key an expelled member cannot hold | 102 | a state machine, a memory invariant, try / catch |
| Harvest node — one vein, one yield per respawn cycle | 79 | a state machine, a memory invariant, try / catch |
| Loot roll — one roll per raider, one award per drop | 84 | a state machine, a memory invariant, try / catch |
| Loot trade — an item exists in exactly one inventory, ever | 101 | a state machine, a memory invariant, try / catch |
| Pity banner — the 90-pull guarantee that cannot be skipped | 73 | a memory invariant |
| Seasonal ladder — decay you cannot dodge, ratings that cannot underflow | 98 | a state machine, a memory invariant, try / catch |
| Stamina — the energy bar that cannot be overfilled or driven negative | 68 | a memory invariant, try / catch |
| Veterancy ranks — promotion is earned and can never be rolled back | 92 | a state machine, a memory invariant, try / catch |
| Wager duel — staked gold that exactly one fighter can win | 122 | a state machine, a memory invariant, match, try / catch |
| Amendment — supermajority ratification, and a "yes" that cannot be unsaid | 129 | a state machine, a memory invariant, try / catch |
| Anti-deficiency — no obligation of funds Congress never appropriated | 126 | a state machine, a memory invariant, try / catch |
| Auditor independence — one firm, one client, ONE role | 117 | a state machine, a memory invariant, try / catch |
| Board motion — Robert's Rules where "no quorum, no vote" is structural | 155 | a state machine, a memory invariant, try / catch |
| Emergency sunset — extraordinary powers that cannot become ordinary | 136 | a state machine, a memory invariant, try / catch |
| Four-eyes approval — the maker cannot be the checker, by construction | 115 | a state machine, a memory invariant, try / catch |
| Grant milestones — money moves only behind verified work, and only once | 148 | a state machine, a memory invariant, try / catch |
| Judicial recusal — a conflicted judge cannot sit, and cases aren't shopped | 121 | a state machine, a memory invariant, try / catch |
| Minutes adoption — the corporate record cannot be edited after the fact | 115 | a state machine, a memory invariant, try / catch |
| Open meetings — no public decision without public notice, structurally | 118 | a state machine, a memory invariant, try / catch |
| Peer review — double-blind where the blind cannot be lifted early | 132 | a state machine, a memory invariant, try / catch |
| Release pipeline — "tests pass before deploy" as a theorem, not a habit | 133 | a state machine, a memory invariant, try / catch |
| Sealed bids — the envelope opens once, for everyone, after the deadline | 131 | a state machine, a memory invariant, try / catch |
| Term limits — the third term is not forbidden, it is unrepresentable | 128 | a state machine, a memory invariant, try / catch |
| Three readings — an ordinance cannot be law the night it is introduced | 145 | a state machine, a memory invariant, try / catch, require / fail |
| Whistleblower shield — retaliation against a reporter is unrepresentable | 119 | a state machine, a memory invariant, try / catch |
| Bonded warehouse — no duty, no exit | 125 | a state machine, a memory invariant, try / catch |
| Cold-chain custody — a warm vaccine never gets cold again | 105 | a state machine, a memory invariant, try / catch |
| Container seal — a broken seal cannot be quietly replaced | 108 | a state machine, a memory invariant, match, try / catch |
| Container weight — the misdeclared box that breaks the ship | 97 | a state machine, a memory invariant, try / catch |
| Customs clearance — no release without an examination verdict | 112 | a state machine, a memory invariant, try / catch |
| Gate appointments — a dock door cannot be double-booked | 100 | a memory invariant |
| Hazmat bay segregation — Beirut, as a state that cannot exist | 120 | a state machine, a memory invariant, try / catch |
| Inventory conservation — stock never teleports, never goes negative | 92 | a memory invariant, pipes (|>), try / catch, lambdas |
| Package tracking — delivered is FOREVER | 84 | a state machine, a memory invariant, try / catch |
| Rack slot capacity — the pallet that brings down the aisle | 85 | a memory invariant, try / catch |
| Recall quarantine — the recalled lot that ships anyway | 110 | a state machine, a memory invariant, try / catch |
| Reefer setpoint — the typo that thaws forty tonnes of tuna | 111 | a state machine, a memory invariant, try / catch |
| Uld loadmaster — National Airlines 102, refused at the manifest | 111 | a state machine, a memory invariant, try / catch |
| Blood bank — an ABO-incompatible transfusion is unrepresentable, and | 129 | a memory invariant, match, try / catch, lambdas |
| Vaccine cold-chain — a temperature breach is PERMANENT, not "probably fine" | 126 | a state machine, a memory invariant, try / catch, lambdas |
| Controlled substance cabinet — the narcotic count must reconcile, always | 133 | a memory invariant, try / catch |
| Dialysis — fluid removal is capped, and a session always ends with the | 148 | a state machine, a memory invariant, try / catch |
| Infusion pump — the programmed rate can never exceed the drug's hard limit ("guardrails") A nurse programming an IV pump types the rate by hand | 113 | a memory invariant, try / catch, lambdas |
| Isolation precautions — a contagious patient cannot be discharged to a | 155 | a state machine, a memory invariant, try / catch |
| Prescription interaction lockout — a lethal drug combination is refused | 142 | a memory invariant, try / catch, lambdas |
| Sepsis bundle — antibiotics never go in before the blood cultures are | 147 | a state machine, a memory invariant, try / catch |
| Autoclave sterilization — a failed cycle can never release instruments | 159 | a state machine, a memory invariant, try / catch, lambdas |
| Surgical safety checklist — no incision before time-out, and the count | 146 | a state machine, a memory invariant, match, try / catch |
| Emergency triage — the sickest patient is seen first, by construction | 123 | a memory invariant, try / catch |
| Autoclave door — a quick-opening door never unlocks under pressure | 96 | a state machine, a memory invariant, try / catch |
| Blast furnace top — never open a door against live CO gas | 83 | a state machine, a memory invariant, try / catch |
| Chlorine dosing — no chemical feed without proven water flow | 88 | a state machine, a memory invariant, try / catch |
| Grain conveyor pull-cord — a latched trip, and a broken safety circuit that stays broken | 88 | a state machine, a memory invariant, try / catch |
| Crane load moment — the tipping write is refused by the ledger | 90 | a state machine, a memory invariant, try / catch |
| Drawbridge — the span never moves while the deck is open to traffic | 85 | a state machine, a memory invariant, try / catch |
| Gas burner ignition — purge before spark, lockout is forever | 82 | a state machine, a memory invariant, try / catch |
| Lockout/tagout — a machine with a personal lock on it cannot start | 91 | a state machine, a memory invariant, try / catch |
| Mine hoist — no motion with the gate open, and a trip is forever | 86 | a state machine, a memory invariant, try / catch |
| Pipeline pig trap — the closure never opens against trapped pressure | 99 | a state machine, a memory invariant, try / catch |
| Pressure relief valve — a live vessel can never lose its relief path | 88 | a state machine, a memory invariant, try / catch |
| Railway block signaling — two trains never share a block | 80 | a state machine, a memory invariant, try / catch |
| Robot cell gate — full-speed automation only behind a closed gate | 84 | a state machine, a memory invariant, try / catch, guard blocks |
| Two-hand press control — anti-tie-down, anti-repeat, structural | 78 | a state machine, a memory invariant, try / catch |
| Payments approval — a whole service in one file: a ledger that cannot overdraw, a payment lifecycle the verifier proves, an HTTP API that maps error kinds to status codes, and tests that run offline | 165 | a state machine, a memory invariant, HTTP routes, match, try / catch, require / fail, several cells, a whole verified service |
| Refund agent — an LLM decides, the language decides what it may do | 162 | a state machine, a memory invariant, an agent cell, a sum type, LLM calls (think), match, try / catch, guard blocks, require / fail, a cost bound, tools |
| Warehouse reservations — two cells: a stock ledger with hard bounds and a reservation lifecycle with a supervisor guard, behind one HTTP router | 187 | a state machine, a memory invariant, HTTP routes, match, try / catch, guard blocks, require / fail, several cells, a whole verified service |
| Review with holes — a design that is proven before it is finished | 90 | a state machine, a memory invariant, require / fail, a skeleton |
| Stock and orders — two skeletons, and what one may ask of the other | 133 | a state machine, a memory invariant, require / fail, a skeleton, several cells |
| Ticket desk — one cell written skeleton-first | 122 | a state machine, a memory invariant, require / fail, a skeleton |
| Triage agent — an LLM inside a frame | 98 | a state machine, a memory invariant, LLM calls (think), a skeleton |
| Turnstile — a signal that may take any edge, and says so | 84 | a state machine, a memory invariant, match, require / fail, a skeleton |
| 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 |
| Subscription billing state machine | 93 | a state machine, a memory invariant |
| 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 |