Grant milestones — money moves only behind verified work, and only once
Milestone-based disbursement is how funders stop the oldest grant fraud there is: draw the full award up front, deliver a report nobody reads, dissolve the entity. GAO audits of federal grant programs keep finding the same two failure modes — funds released ahead of the work, and the same milestone paid twice under slightly different paperwork. Clawing money back after the fact almost never works; the only cheap control is at the moment of disbursement. So that moment is where the walls are. The grant walks a machine — each milestone must be verified before the next opens, soma verify proves there is no path around the order. The escrow balance carries `invariant >= 0` (you cannot disburse money that is not there) and each milestone pays AT MOST ONCE: the duplicate-invoice write is refused by the ledger itself.
A Soma program from the governance part of the verified corpus: 148 lines, cells GrantEscrow, EscrowTests. It passes soma check with soma 3.2.4.
How it is built
The cell GrantEscrow declares 5 signals in its face: fund(grant: String, amount: Int) -> Map, verify_milestone(grant: String) -> Map, disburse(grant: String, milestone: Int, amount: Int) -> Map, escrow_left(grant: String) -> Int and paid_for(grant: String, milestone: Int) -> Int; keeps 3 memory slots: escrow (Map<String, Int>, persistent and consistent) under the invariant escrow >= 0, payouts (Map<String, Int>, persistent and consistent) under the invariant payouts >= 0 && payouts <= 1 and amounts (Map<String, Int>, persistent and consistent) under the invariant amounts >= 1. Its state machine grant starts in awarded and allows 4 transitions: awarded -> funded, funded -> m1_verified, m1_verified -> m2_verified and m2_verified -> closed. closed is terminal. Handlers: fund (line 54), verify_milestone (line 62), disburse (line 75), escrow_left (line 107) and paid_for (line 111).
The file also holds 1 test cell (EscrowTests) with 19 assertions, run by soma test.
The source
grant_milestones.cell
// ============================================================================
// GRANT MILESTONES — money moves only behind verified work, and only once
// ============================================================================
//
// Milestone-based disbursement is how funders stop the oldest grant
// fraud there is: draw the full award up front, deliver a report nobody
// reads, dissolve the entity. GAO audits of federal grant programs keep
// finding the same two failure modes — funds released ahead of the work,
// and the same milestone paid twice under slightly different paperwork.
// Clawing money back after the fact almost never works; the only cheap
// control is at the moment of disbursement.
//
// So that moment is where the walls are. The grant walks a machine —
// each milestone must be verified before the next opens, soma verify
// proves there is no path around the order. The escrow balance carries
// `invariant >= 0` (you cannot disburse money that is not there) and
// each milestone pays AT MOST ONCE: the duplicate-invoice write is
// refused by the ledger itself.
// ============================================================================
cell GrantEscrow {
face {
signal fund(grant: String, amount: Int) -> Map
signal verify_milestone(grant: String) -> Map
signal disburse(grant: String, milestone: Int, amount: Int) -> Map
signal escrow_left(grant: String) -> Int
signal paid_for(grant: String, milestone: Int) -> Int
}
memory {
// what remains in escrow — can never go below zero
escrow: Map<String, Int> [persistent, consistent]
invariant escrow >= 0
// grant:milestone -> payments made. ONE. The duplicate invoice
// for already-paid work is unrepresentable.
payouts: Map<String, Int> [persistent, consistent]
invariant payouts >= 0 && payouts <= 1
amounts: Map<String, Int> [persistent, consistent]
invariant amounts >= 1
}
// funded -> m1_verified -> m2_verified -> closed (TERMINAL).
// Verification is the only way forward; closed grants pay nobody.
state grant {
initial: awarded
awarded -> funded
funded -> m1_verified
m1_verified -> m2_verified
m2_verified -> closed
}
on fund(grant: String, amount: Int) {
if amount <= 0 { return map("ok", false, "reason", "funding must be positive") }
let r = try { transition(grant, "funded") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
escrow.set(grant, amount)
return map("ok", true, "grant", grant, "escrow", amount)
}
on verify_milestone(grant: String) {
let s = get_status(grant)
let target = ""
if s == "funded" { target = "m1_verified" }
if s == "m1_verified" { target = "m2_verified" }
if s == "m2_verified" { target = "closed" }
if target == "" {
return map("ok", false, "reason", "nothing verifiable from state {s}")
}
transition(grant, target)
return map("ok", true, "state", target)
}
on disburse(grant: String, milestone: Int, amount: Int) {
let s = get_status(grant)
// money follows verified work: milestone N pays only once the
// machine has actually passed mN_verified (and the grant is open)
let earned = false
if milestone == 1 && (s == "m1_verified" || s == "m2_verified") { earned = true }
if milestone == 2 && s == "m2_verified" { earned = true }
if !earned {
return map("ok", false, "reason",
"milestone {milestone} is not verified-and-payable from state {s}")
}
if amount <= 0 { return map("ok", false, "reason", "disbursements are positive") }
let left = escrow.get(grant) ?? 0
if left < amount {
return map("ok", false, "reason", "escrow has {left}; {amount} refused")
}
// WALL 1: pay each milestone once
let k = "{grant}:m{milestone}"
let w = try { payouts.set(k, (payouts.get(k) ?? 0) + 1) }
if w.error != () {
return map("ok", false, "reason", "milestone {milestone} was already paid")
}
// WALL 2: even if the check above were deleted, the escrow slot
// refuses to go negative
let e = try { escrow.set(grant, left - amount) }
if e.error != () {
return map("ok", false, "reason", "escrow write refused: {e.error}")
}
amounts.set(k, amount)
return map("ok", true, "milestone", milestone, "paid", amount, "left", left - amount)
}
on escrow_left(grant: String) {
return escrow.get(grant) ?? 0
}
on paid_for(grant: String, milestone: Int) {
return amounts.get("{grant}:m{milestone}") ?? 0
}
}
cell test EscrowTests {
rules {
// the classic fraud: draw everything before any work is verified
assert fund("G-77", 1000).ok == true
assert disburse("G-77", 1, 500).ok == false
assert disburse("G-77", 2, 500).ok == false
assert_fails transition("G-77", "m2_verified") // no skipping milestone 1
assert_fails transition("G-77", "closed")
// milestone 1 verified — milestone 1 money flows, milestone 2 stays shut
assert verify_milestone("G-77").state == "m1_verified"
assert disburse("G-77", 2, 500).ok == false
assert disburse("G-77", 1, 400).left == 600
// the duplicate invoice: a second payment for m1 is refused
assert disburse("G-77", 1, 400).ok == false
assert_fails payouts.set("G-77:m1", 2)
assert paid_for("G-77", 1) == 400
// milestone 2: cannot draw more than the escrow holds
assert verify_milestone("G-77").state == "m2_verified"
assert disburse("G-77", 2, 900).ok == false // 900 > 600
assert_fails escrow.set("G-77", -300)
assert disburse("G-77", 2, 600).left == 0
// closed is terminal — a finished grant pays nothing, ever again
assert verify_milestone("G-77").state == "closed"
assert_fails transition("G-77", "funded")
assert disburse("G-77", 1, 1).ok == false
assert escrow_left("G-77") == 0
}
}What the toolchain says
$ soma check grant_milestones.cell
✓ All checks passed.$ soma test grant_milestones.cell
test EscrowTests ...
✓ assert fund("G-77", 1000).ok == true
✓ assert disburse("G-77", 1, 500).ok == false
✓ assert disburse("G-77", 2, 500).ok == false
✓ assert_fails transition("G-77", "m2_verified") — raised invalid transition: funded → m2_verified. Current state: 'funded'. Valid targets: [m1_verified]
✓ assert_fails transition("G-77", "closed") — raised invalid transition: funded → closed. Current state: 'funded'. Valid targets: [m1_verified]
✓ assert verify_milestone("G-77").state == "m1_verified"
✓ assert disburse("G-77", 2, 500).ok == false
✓ assert disburse("G-77", 1, 400).left == 600
✓ assert disburse("G-77", 1, 400).ok == false
✓ assert_fails payouts.set("G-77:m1", 2) — raised memory invariant violated on 'payouts': payouts >= 0 && payouts <= 1 — rejected write of 2 (key "G-77:m1"); the slot is unchanged
✓ assert paid_for("G-77", 1) == 400
✓ assert verify_milestone("G-77").state == "m2_verified"
✓ assert disburse("G-77", 2, 900).ok == false
✓ assert_fails escrow.set("G-77", -300) — raised memory invariant violated on 'escrow': escrow >= 0 — rejected write of -300 (key "G-77"); the slot is unchanged
✓ assert disburse("G-77", 2, 600).left == 0
✓ assert verify_milestone("G-77").state == "closed"
✓ assert_fails transition("G-77", "funded") — raised invalid transition: closed → funded. Current state: 'closed'. Valid targets: []
✓ assert disburse("G-77", 1, 1).ok == false
✓ assert escrow_left("G-77") == 0
19 tests: 19 passed, 0 failed$ soma verify grant_milestones.cell
Verifying grant_milestones.cell...
State machine 'grant': 5 states, initial 'awarded'
States: [awarded, closed, funded, m1_verified, m2_verified]
✓ 5 states, 4 transitions
✓ all states reachable from 'awarded'
✓ terminal states: [closed]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
⚠ dynamic transition targets: handler `verify_milestone` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
✓ termination: all 5 handlers structurally terminate
⚠ refinement (partial — dynamic targets fall back to runtime check): handler `verify_milestone` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
✓ refinement (partial — dynamic targets fall back to runtime check): handler `fund` ⟶ {funded}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `verify_milestone` ⟶ <dynamic>
· transition sources: `fund` calls transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)
GrantEscrow/invariants:
✓ invariant escrow >= 0 — writer 'disburse' proven by induction (writes left - amount)
✓ invariant escrow >= 0 — writer 'fund' proven by induction (writes amount)
✓ invariant payouts >= 0 — writer 'disburse' proven by induction (writes (payouts.get(k) ?? 0) + 1)
⚠ invariant payouts >= 0 && payouts <= 1 — runtime-checked (computed values): disburse → payouts [payouts <= 1] because `k` = "{grant}:m{milestone}" — not bounded; `payouts` has no known range
✓ invariant amounts >= 1 — writer 'disburse' proven by induction (writes amount)
12 passed, 3 warnings, 0 failures
Temporal properties for 'grant':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK