Verified programs
327 Soma programs, each re-checked by soma 3.2.4 when this page was built. A program the toolchain rejects is withheld, never published.
New to Soma? Start with the basic examples: 97 small programs, commented line by line.
aerospace
15 programs: Autopilot authority — Aeroflot 593: the half-disconnected autopilot; Cabin pressurization — Helios 522: the manual-mode takeoff, unrepresentable; Cargo door — Turkish Airlines 981: "indicated locked" is not LOCKED…
agents
17 programs: Human-in-the-loop approval gate guarding an irreversible action; Bounded-retry agent — the verified-termination poster child; Token-budget enforcement, made testable…
algorithms
18 programs: Breadth-first search on a small directed graph represented as an adjacency; Binary search over a sorted List<Int> — returns the index or -1; Bubble sort over a list, with the classic early-exit optimization…
civic
14 programs: Campaign finance — the contribution limit lives in the ledger, not the law; Census — after certification, the count is history, not a database row; Disaster aid — one emergency grant per household, however many times asked…
data
17 programs: A/B test rollup: per-variant conversions and lift over control; Market-basket analysis: transactions of (order, product) lines; Cohort analysis: bucket users by signup month, then measure how many were still active in a later month…
devops
14 programs: Backup retention — the floor you cannot prune through; Blue/green cutover — there is no state where nobody serves traffic; Cert rotation — expiry is an escalation ladder, not a surprise…
energy
15 programs: Anti-islanding — a solar inverter must never energize a "dead" line; Battery dispatch — the charge window is a wall, not a setpoint; Black start — you cannot boot a power plant from a dead grid out of order…
escrow_finance
15 programs: Chargeback window — disputes die at day 120, reversals happen exactly once; Client money segregation — the firm can only ever touch its own excess; All-or-nothing crowdfunding — miss the goal, every backer gets refunded…
finance
17 programs: Fixed-coupon bond pricing: present value of coupons plus redemption, current yield, and a par/premium/discount classifier; Monthly budget tracker with a spend cap invariant; Chip/cash ledger with a non-negative balance invariant…
games
19 programs: Blackjack — hand scoring with soft/hard aces and bust detection hand_value() sums card ranks, counting each Ace as 11 then demoting to 1 while the total busts; Card deck — build, deterministic Fisher-Yates shuffle, and deal; Connect Four — drop a disc and detect four-in-a-row…
games_economy
16 programs: Auction house — escrowed bids, gold that cannot be printed; Battle pass — every tier reward claimed exactly once; Battle turns — nobody acts twice, and the dead stay dead…
governance
16 programs: Amendment — supermajority ratification, and a "yes" that cannot be unsaid; Anti-deficiency — no obligation of funds Congress never appropriated; Auditor independence — one firm, one client, ONE role…
logistics
15 programs: Bonded warehouse — no duty, no exit; Cold-chain custody — a warm vaccine never gets cold again; Container seal — a broken seal cannot be quietly replaced…
math
17 programs: Bisection — bracket a root of a continuous function and halve; Combinatorics — factorial, permutations, combinations factorial folds product over range(1, n+1); Complex numbers — records carrying real and imaginary parts…
medical
14 programs: Blood bank — an ABO-incompatible transfusion is unrepresentable, and; 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 it; Vaccine cold-chain — a temperature breach is PERMANENT, not "probably fine"…
records
17 programs: Address book: Contact records stored in a Map slot, round-tripped through storage, and queried; Bank accounts as Account records kept in a persistent Map slot, with deposit/withdraw that read, mutate, and write the record back; Binary search tree built from Node records with nested `left`/`right` children…
safety_interlocks
14 programs: Autoclave door — a quick-opening door never unlocks under pressure; Blast furnace top — never open a door against live CO gas; Chlorine dosing — no chemical feed without proven water flow…
services
3 programs: 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; Refund agent — an LLM decides, the language decides what it may do; Warehouse reservations — two cells: a stock ledger with hard bounds and a reservation lifecycle with a supervisor guard, behind one HTTP router…
skeleton
5 programs: Review with holes — a design that is proven before it is finished; Stock and orders — two skeletons, and what one may ask of the other; Ticket desk — one cell written skeleton-first…
state_machines
15 programs: Document editorial workflow with a typed (sum-type) state machine; An elevator door + motion interlock; Multi-step expense-approval workflow with guarded transitions…
text
18 programs: Acronym / initials — first letter of each word, uppercased; Anagram check — same multiset of letters; Caesar cipher — shift letters using an alphabet lookup…
web
16 programs: Mini blog API with tag filtering. Posts carry a list of tags;; Form handler with server-side validation; Counter API: a persistent integer counter exposed over HTTP…
316 complete Soma programs across 20 domains — every one passing soma check and soma test (and soma verify where a state machine exists) on the current binary, independently re-verified before commit. Generated as LLM training data: idiomatic, diverse, self-verifying, and (wave 2) story-driven — each safety program names the real-world failure it makes unrepresentable (Therac-25, Lauda Air 004, Helios 522, Überlingen, Apollo 13, Ladbroke Grove, ...).
| Domain | Programs |
|---|---|
| aerospace | 15 |
| agents | 15 |
| algorithms | 18 |
| civic | 14 |
| data | 17 |
| devops | 14 |
| energy | 15 |
| escrow_finance | 15 |
| finance | 17 |
| games | 19 |
| games_economy | 16 |
| governance | 16 |
| logistics | 15 |
| math | 17 |
| medical | 14 |
| records | 17 |
| skeleton | 5 |
| safety_interlocks | 14 |
| state_machines | 14 |
| text | 18 |
| web | 16 |
Verify the whole corpus:
for f in examples/corpus/*/*.cell; do soma check "$f" && soma test "$f"; done