Programs using require / fail
16 verified Soma programs that use require / fail. Start from one of these when you write a program that needs it.
| Program | Lines | Uses |
|---|---|---|
| Agent with preconditions and a memory invariant — refuses bad input | 59 | a state machine, a memory invariant, an agent cell, require / fail |
| A horde: one [task] agent per document, a bounded pool, a hard token budget, each verdict stored exactly once, a summary at the end | 58 | an agent cell, LLM calls (think), pipes (|>), lambdas, require / fail, several cells |
| Planning agent: decompose a goal into ordered subtasks, then execute | 64 | a state machine, an agent cell, require / fail |
| Turn-bounded conversation agent — proves a chat loop terminates | 61 | a state machine, an agent cell, LLM calls (think), try / catch, require / fail |
| Three readings — an ordinance cannot be law the night it is introduced | 145 | a state machine, a memory invariant, try / catch, require / fail |
| 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 |
| 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 |
| An HVAC thermostat control loop | 75 | a state machine, require / fail |
| 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 |