soma.cell

Programs using a state machine

176 verified Soma programs that use a state machine. Start from one of these when you write a program that needs it.

ProgramLinesUses
Autopilot authority — Aeroflot 593: the half-disconnected autopilot108a state machine, a memory invariant, try / catch
Cabin pressurization — Helios 522: the manual-mode takeoff, unrepresentable106a state machine, a memory invariant, try / catch
Cargo door — Turkish Airlines 981: "indicated locked" is not LOCKED116a state machine, a memory invariant, try / catch
Docking approach — Progress / Mir 1997: abort means ABORT116a state machine, a memory invariant, try / catch
Engine fire bottle — one-shot suppression, fuel off FIRST117a state machine, a memory invariant, try / catch
Fuel crossfeed — Air Transat 236: never feed a leak from the good tank118a state machine, a memory invariant, try / catch
Landing gear — weight-on-wheels interlock, made unrepresentable99a state machine, a memory invariant, try / catch
Launch commit criteria — Challenger: no waiver path to ignition127a state machine, a memory invariant, try / catch
Cryo tank heater — Apollo 13: the thermostat that welded shut110a state machine, a memory invariant, try / catch
Parachute sequence — Genesis: the drogue that never fired105a state machine, a memory invariant, try / catch
Range safety — the flight termination system's three one-way doors114a state machine, a memory invariant, try / catch
Stage separation — the ascent sequence as a proven order90a state machine, a memory invariant, try / catch
Tcas resolution advisory — Überlingen: the opposite maneuver is no state121a state machine, a memory invariant, try / catch
Thrust reverser — Lauda Air 004: in-flight deployment, made structural100a state machine, a memory invariant, try / catch
Unreliable airspeed — AF447: the autopilot never flies on bad data105a state machine, a memory invariant, try / catch
Human-in-the-loop approval gate guarding an irreversible action70a state machine, an agent cell
Bounded-retry agent — the verified-termination poster child60a state machine, an agent cell
Token-budget enforcement, made testable52a state machine, an agent cell, LLM calls (think), try / catch
Agent with preconditions and a memory invariant — refuses bad input59a state machine, a memory invariant, an agent cell, require / fail
Agent with persistent memory via remember()/recall()61a state machine, an agent cell, LLM calls (think), try / catch
Multi-agent content pipeline with verified handoffs70a state machine, an agent cell, several cells
Planning agent: decompose a goal into ordered subtasks, then execute64a state machine, an agent cell, require / fail
A ReAct-style agent whose tools are real, deterministic computations63a state machine, an agent cell, LLM calls (think), pipes (|>), try / catch, lambdas, tools
Sentiment-routing agent: classify a message, route by polarity67a state machine, an agent cell, LLM calls (think), match, tools
Reflective tool-dispatch agent: routes a named action to the right tool77a state machine, an agent cell, LLM calls (think), match, try / catch, tools
Self-auditing agent: it inspects its own execution trace59a state machine, an agent cell, LLM calls (think), try / catch, tools
Support-ticket triage agent65a state machine, an agent cell, LLM calls (think), tools
Turn-bounded conversation agent — proves a chat loop terminates61a state machine, an agent cell, LLM calls (think), try / catch, require / fail
Agent lifecycle typed against a sum type — typos become compile errors57a state machine, an agent cell, a sum type, match
The killer feature: an agent whose termination is PROVEN by soma verify52a state machine, an agent cell, LLM calls (think), try / catch
Campaign finance — the contribution limit lives in the ledger, not the law106a state machine, a memory invariant, try / catch
Census — after certification, the count is history, not a database row106a state machine, a memory invariant, try / catch
Disaster aid — one emergency grant per household, however many times asked116a state machine, a memory invariant, try / catch
Election audit — a risk-limiting audit that cannot count a ballot twice117a state machine, a memory invariant, try / catch
Foia — the statutory clock cannot be silently ignored99a state machine, a memory invariant, try / catch
Grants — budget conservation: the fund cannot award money it does not have107a state machine, a memory invariant, try / catch
Jury — strikes are counted by the bench, not by the honor system118a state machine, a memory invariant, try / catch
Land registry — a parcel cannot be sold to two buyers at once110a state machine, a memory invariant, try / catch
Lottery — committed entries, a published seed, and a draw that closes forever96a state machine, a memory invariant, try / catch
Permit — a building permit that cannot skip a review118a state machine, a memory invariant, try / catch
Petition — one signature per citizen, a wall in memory, not a clerk's eye100a state machine, a memory invariant, try / catch
Procurement — sealed bids stay sealed, and the unsealing ends the auction112a state machine, a memory invariant, try / catch
Sunshine — a council cannot vote on what the public never got to discuss135a state machine, a memory invariant, try / catch
Vital records — a person dies at most once, and benefits know it instantly107a state machine, a memory invariant, try / catch
Backup retention — the floor you cannot prune through102a state machine, a memory invariant, try / catch
Blue/green cutover — there is no state where nobody serves traffic114a state machine, a memory invariant, try / catch
Cert rotation — expiry is an escalation ladder, not a surprise108a state machine, a memory invariant, try / catch
Db migration — applied migrations are immutable history104a state machine, a memory invariant, try / catch
Deploy canary — the staged rollout you cannot skip102a state machine, a memory invariant, try / catch
Dns change control — no record goes live without passing validation102a state machine, a memory invariant, try / catch
Kill switch — a dead flag stays dead105a state machine, a memory invariant, try / catch
Fleet sync — no activation until every node runs the same code100a state machine, a memory invariant, try / catch
Image promotion — nothing unscanned, unsigned, or vulnerable ships105a state machine, a memory invariant, try / catch
Incident ladder — severity only climbs, and closure needs a postmortem118a state machine, a memory invariant, try / catch
Pager escalation — no page resolves without a human acknowledging it110a state machine, a memory invariant, try / catch
Rate limiter — admission control with a quota the memory enforces119a state machine, a memory invariant, try / catch
Secret rotation — a revoked credential never logs in again115a state machine, a memory invariant, try / catch
State lock — two concurrent applies can never both hold the lock114a state machine, a memory invariant, try / catch
Anti-islanding — a solar inverter must never energize a "dead" line107a state machine, a memory invariant, try / catch
Black start — you cannot boot a power plant from a dead grid out of order118a state machine, a memory invariant, try / catch
Recloser — a trip is permanent until a human walks the line94a state machine, a memory invariant, try / catch
Demand response — no payment before measurement, and settlement is final124a state machine, a memory invariant, try / catch
Ev charging — no current before the handshake, no session past the cap124a state machine, a memory invariant, try / catch
Gas turbine light-off — purge before every ignition attempt, no exceptions134a state machine, a memory invariant, try / catch
Generator paralleling — sync-check before the breaker, always137a state machine, a memory invariant, try / catch
Meter billing — you are billed exactly what the meter read, once115a state machine, a memory invariant, match, try / catch
Spillway gates — a dam may never lose its last release path121a state machine, a memory invariant, try / catch
Lockout-tagout — test before touch, and nobody re-energizes over a lock137a state machine, a memory invariant, try / catch
Transformer emergency loading — overload only with every fan running134a state machine, a memory invariant, try / catch
Wind turbine overspeed — after an emergency brake, inspection or nothing136a state machine, a memory invariant, try / catch
Chargeback window — disputes die at day 120, reversals happen exactly once109a state machine, a memory invariant
All-or-nothing crowdfunding — miss the goal, every backer gets refunded120a state machine, a memory invariant
Dividend distribution — payments can never exceed the declared pool96a state machine, a memory invariant
Delivery-versus-payment — no securities leave before the cash arrives111a state machine, a memory invariant
Invoice factoring — no advance on unverified paper, no double-selling108a state machine, a memory invariant
Letter of credit — the bank pays against verified documents, never trust116a state machine, a memory invariant
Loan amortization — principal never goes negative, never grows back100a state machine, a memory invariant
Milestone escrow — a contractor is paid per accepted milestone, never ahead106a state machine, a memory invariant
Multisig treasury — 2-of-3 distinct approvals, proven before a cent moves109a state machine, a memory invariant
Payroll run — the payslips must sum EXACTLY to the approved total100a state machine, a memory invariant
Security deposit — deductions can never exceed what the tenant paid99a state machine, a memory invariant
Two-party escrow — funds move only when BOTH sides say so, and never leak117a state machine, a memory invariant
Vesting schedule — cliff then linear, and over-vesting is unwritable118a state machine, a memory invariant
Wire dual control — the maker can never be the checker98a state machine, a memory invariant
Order lifecycle as a verified state machine: an order flows from new to filled or rejected, and a fill settles63a state machine, guard blocks
Turn tracker — round/phase state machine with player rotation71a state machine
Auction house — escrowed bids, gold that cannot be printed124a state machine, a memory invariant, try / catch
Battle pass — every tier reward claimed exactly once92a state machine, a memory invariant, try / catch
Battle turns — nobody acts twice, and the dead stay dead89a state machine, a memory invariant
Crafting forge — ingredients consumed exactly once98a state machine, a memory invariant, try / catch
Daily chest — one claim per day, clock tricks be damned57a state machine, a memory invariant, try / catch
Gem store — a purchase receipt credits exactly once101a state machine, a memory invariant, try / catch
Guild bank — the heist needs a key an expelled member cannot hold102a state machine, a memory invariant, try / catch
Harvest node — one vein, one yield per respawn cycle79a state machine, a memory invariant, try / catch
Loot roll — one roll per raider, one award per drop84a state machine, a memory invariant, try / catch
Loot trade — an item exists in exactly one inventory, ever101a state machine, a memory invariant, try / catch
Seasonal ladder — decay you cannot dodge, ratings that cannot underflow98a state machine, a memory invariant, try / catch
Tournament bracket — eliminated means eliminated73a state machine, match, try / catch
Veterancy ranks — promotion is earned and can never be rolled back92a state machine, a memory invariant, try / catch
Wager duel — staked gold that exactly one fighter can win122a state machine, a memory invariant, match, try / catch
Amendment — supermajority ratification, and a "yes" that cannot be unsaid129a state machine, a memory invariant, try / catch
Anti-deficiency — no obligation of funds Congress never appropriated126a state machine, a memory invariant, try / catch
Auditor independence — one firm, one client, ONE role117a state machine, a memory invariant, try / catch
Board motion — Robert's Rules where "no quorum, no vote" is structural155a state machine, a memory invariant, try / catch
Emergency sunset — extraordinary powers that cannot become ordinary136a state machine, a memory invariant, try / catch
Four-eyes approval — the maker cannot be the checker, by construction115a state machine, a memory invariant, try / catch
Grant milestones — money moves only behind verified work, and only once148a state machine, a memory invariant, try / catch
Judicial recusal — a conflicted judge cannot sit, and cases aren't shopped121a state machine, a memory invariant, try / catch
Minutes adoption — the corporate record cannot be edited after the fact115a state machine, a memory invariant, try / catch
Open meetings — no public decision without public notice, structurally118a state machine, a memory invariant, try / catch
Peer review — double-blind where the blind cannot be lifted early132a state machine, a memory invariant, try / catch
Release pipeline — "tests pass before deploy" as a theorem, not a habit133a state machine, a memory invariant, try / catch
Sealed bids — the envelope opens once, for everyone, after the deadline131a state machine, a memory invariant, try / catch
Term limits — the third term is not forbidden, it is unrepresentable128a state machine, a memory invariant, try / catch
Three readings — an ordinance cannot be law the night it is introduced145a state machine, a memory invariant, try / catch, require / fail
Whistleblower shield — retaliation against a reporter is unrepresentable119a state machine, a memory invariant, try / catch
Bonded warehouse — no duty, no exit125a state machine, a memory invariant, try / catch
Cold-chain custody — a warm vaccine never gets cold again105a state machine, a memory invariant, try / catch
Container seal — a broken seal cannot be quietly replaced108a state machine, a memory invariant, match, try / catch
Container weight — the misdeclared box that breaks the ship97a state machine, a memory invariant, try / catch
Customs clearance — no release without an examination verdict112a state machine, a memory invariant, try / catch
Dock door interlock — the trailer that drives off with the forklift86a state machine, try / catch
Hazmat bay segregation — Beirut, as a state that cannot exist120a state machine, a memory invariant, try / catch
Package tracking — delivered is FOREVER84a state machine, a memory invariant, try / catch
Proof of delivery — no signature, no "delivered"105a state machine, try / catch
Recall quarantine — the recalled lot that ships anyway110a state machine, a memory invariant, try / catch
Reefer setpoint — the typo that thaws forty tonnes of tuna111a state machine, a memory invariant, try / catch
Uld loadmaster — National Airlines 102, refused at the manifest111a state machine, a memory invariant, try / catch
Lab chain of custody — a sample whose custody broke can never be reported, by construction A forensic toxicology or pathology result is only as trustworthy as the unbroken chain of custody behind it125a state machine, try / catch
Vaccine cold-chain — a temperature breach is PERMANENT, not "probably fine"126a state machine, a memory invariant, try / catch, lambdas
Dialysis — fluid removal is capped, and a session always ends with the148a state machine, a memory invariant, try / catch
Isolation precautions — a contagious patient cannot be discharged to a155a state machine, a memory invariant, try / catch
Medication administration — the "five rights" enforced by barcode, no scan no dose Wrong-patient and wrong-drug medication errors are among the most common causes of inpatient harm135a state machine, match, try / catch
Sepsis bundle — antibiotics never go in before the blood cultures are147a state machine, a memory invariant, try / catch
Autoclave sterilization — a failed cycle can never release instruments159a state machine, a memory invariant, try / catch, lambdas
Surgical safety checklist — no incision before time-out, and the count146a state machine, a memory invariant, match, try / catch
Organ allocation — one organ, one recipient, and no taking it back once145a state machine, try / catch
Order records with nested line-items, computed totals, and a state machine over the order lifecycle58a state machine, a sum type, pipes (|>), lambdas
Autoclave door — a quick-opening door never unlocks under pressure96a state machine, a memory invariant, try / catch
Blast furnace top — never open a door against live CO gas83a state machine, a memory invariant, try / catch
Chlorine dosing — no chemical feed without proven water flow88a state machine, a memory invariant, try / catch
Grain conveyor pull-cord — a latched trip, and a broken safety circuit that stays broken88a state machine, a memory invariant, try / catch
Crane load moment — the tipping write is refused by the ledger90a state machine, a memory invariant, try / catch
Drawbridge — the span never moves while the deck is open to traffic85a state machine, a memory invariant, try / catch
Gas burner ignition — purge before spark, lockout is forever82a state machine, a memory invariant, try / catch
Lockout/tagout — a machine with a personal lock on it cannot start91a state machine, a memory invariant, try / catch
Mine hoist — no motion with the gate open, and a trip is forever86a state machine, a memory invariant, try / catch
Pipeline pig trap — the closure never opens against trapped pressure99a state machine, a memory invariant, try / catch
Pressure relief valve — a live vessel can never lose its relief path88a state machine, a memory invariant, try / catch
Railway block signaling — two trains never share a block80a state machine, a memory invariant, try / catch
Robot cell gate — full-speed automation only behind a closed gate84a state machine, a memory invariant, try / catch, guard blocks
Two-hand press control — anti-tie-down, anti-repeat, structural78a 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 offline165a 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 do162a 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 router187a 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 finished90a state machine, a memory invariant, require / fail, a skeleton
Stock and orders — two skeletons, and what one may ask of the other133a state machine, a memory invariant, require / fail, a skeleton, several cells
Ticket desk — one cell written skeleton-first122a state machine, a memory invariant, require / fail, a skeleton
Triage agent — an LLM inside a frame98a state machine, a memory invariant, LLM calls (think), a skeleton
Turnstile — a signal that may take any edge, and says so84a state machine, a memory invariant, match, require / fail, a skeleton
Document editorial workflow with a typed (sum-type) state machine59a state machine, a sum type
An elevator door + motion interlock60a state machine
Multi-step expense-approval workflow with guarded transitions81a state machine, a memory invariant, require / fail
Online game-match lifecycle81a state machine, a memory invariant, match
A media-player transport state machine57a state machine, a sum type
Order lifecycle as a typed state machine58a state machine, a sum type
Parcel shipment tracking with a delivery-exception loop67a state machine
Subscription billing state machine93a state machine, a memory invariant
Support-ticket lifecycle with a reopen path60a state machine
A simplified TCP connection state machine (active-open path)58a state machine, a sum type
An HVAC thermostat control loop75a state machine, require / fail
A two-road traffic-light interlock proven safe by construction62a state machine, match
A coin-operated turnstile — the textbook two-state machine, plus an out-of-service state reachable only via maintenance77a state machine
A vending machine state machine89a state machine, a memory invariant, require / fail
Wildcard failure — `* -> failed` with an `eventually` property68a state machine, a memory invariant, guard blocks, require / fail
Todo service backed by a typed state machine (sum type TodoStatus)82a state machine, a sum type, HTTP routes, match