Milestone escrow — a contractor is paid per accepted milestone, never ahead
Freelance platforms learned this the expensive way: pay a contractor the full project fee up front and disputes become hostage negotiations. The escrow answer is milestones — but then the bug moves: releasing milestone money TWICE, or releasing more than the client funded. Here the funded balance is a slot that releases draw down (`escrowed >= 0`: the over-release is a rejected write), each milestone is released at most once, and a cancelled or completed project is terminal — the leftover balance goes back to the client exactly once.
A Soma program from the escrow_finance part of the verified corpus: 106 lines, cells MilestoneEscrow, MilestoneTests. It passes soma check with soma 3.2.4.
How it is built
The cell MilestoneEscrow declares 5 signals in its face: fund_project(id: String, amount: Int) -> Map, accept_milestone(id: String, ms: String, fee: Int) -> Map, finish_project(id: String) -> Map, cancel_project(id: String) -> Map and escrow_left(id: String) -> Int; keeps 2 memory slots: escrowed (Map<String, Int>, persistent and consistent) under the invariant escrowed >= 0 and released (Map<String, Int>, persistent and consistent) under the invariant released >= 0. Its state machine project starts in proposed and allows 3 transitions: proposed -> funded, funded -> completed and funded -> cancelled. cancelled and completed are terminal. Handlers: fund_project (line 39), accept_milestone (line 46), finish_project (line 61), cancel_project (line 68) and escrow_left (line 75).
The file also holds 1 test cell (MilestoneTests) with 17 assertions, run by soma test.
The source
milestone_escrow.cell
// ============================================================================
// MILESTONE ESCROW — a contractor is paid per accepted milestone, never ahead
// ============================================================================
//
// Freelance platforms learned this the expensive way: pay a contractor the
// full project fee up front and disputes become hostage negotiations. The
// escrow answer is milestones — but then the bug moves: releasing milestone
// money TWICE, or releasing more than the client funded. Here the funded
// balance is a slot that releases draw down (`escrowed >= 0`: the
// over-release is a rejected write), each milestone is released at most
// once, and a cancelled or completed project is terminal — the leftover
// balance goes back to the client exactly once.
// ============================================================================
cell MilestoneEscrow {
face {
signal fund_project(id: String, amount: Int) -> Map
signal accept_milestone(id: String, ms: String, fee: Int) -> Map
signal finish_project(id: String) -> Map
signal cancel_project(id: String) -> Map
signal escrow_left(id: String) -> Int
}
memory {
escrowed: Map<String, Int> [persistent, consistent]
invariant escrowed >= 0
released: Map<String, Int> [persistent, consistent]
invariant released >= 0
}
// completed and cancelled are terminal: no release after either.
state project {
initial: proposed
proposed -> funded
funded -> completed
funded -> cancelled
}
on fund_project(id: String, amount: Int) {
if amount <= 0 { return map("ok", false, "reason", "bad amount") }
transition(id, "funded")
escrowed.set(id, amount)
return map("ok", true, "escrowed", amount)
}
on accept_milestone(id: String, ms: String, fee: Int) {
if get_status(id) != "funded" {
return map("ok", false, "reason", "project is not active")
}
if fee <= 0 { return map("ok", false, "reason", "bad fee") }
let k = "{id}:{ms}"
if (released.get(k) ?? 0) > 0 {
return map("ok", false, "reason", "milestone {ms} already released")
}
let bal = escrowed.get(id) ?? 0
escrowed.set(id, bal - fee) // raises past the funded amount
released.set(k, fee)
return map("ok", true, "milestone", ms, "left", bal - fee)
}
on finish_project(id: String) {
transition(id, "completed")
let refund = escrowed.get(id) ?? 0
escrowed.set(id, 0) // unspent escrow back to client
return map("ok", true, "refund_to_client", refund)
}
on cancel_project(id: String) {
transition(id, "cancelled")
let refund = escrowed.get(id) ?? 0
escrowed.set(id, 0)
return map("ok", true, "refund_to_client", refund)
}
on escrow_left(id: String) {
return escrowed.get(id) ?? 0
}
}
cell test MilestoneTests {
rules {
assert fund_project("site", 5000).ok == true
assert accept_milestone("site", "design", 1500).ok == true
assert accept_milestone("site", "build", 2500).ok == true
assert escrow_left("site") == 1000
// THE DOUBLE RELEASE: same milestone, second payment — refused
assert accept_milestone("site", "design", 1500).ok == false
// THE OVER-RELEASE: 1,800 against 1,000 left — the write raises
assert_fails accept_milestone("site", "launch", 1800)
assert escrow_left("site") == 1000
assert_fails escrowed.set("site", -1)
// finishing returns the leftover to the client, once
assert finish_project("site").refund_to_client == 1000
assert escrow_left("site") == 0
// completed is terminal: no milestone, no cancel-refund after
assert accept_milestone("site", "extra", 100).ok == false
assert_fails transition("site", "cancelled")
assert_fails transition("site", "funded")
// the cancel path on another project, equally final
assert fund_project("logo", 800).ok == true
assert accept_milestone("logo", "draft", 300).ok == true
assert cancel_project("logo").refund_to_client == 500
assert_fails transition("logo", "completed")
}
}What the toolchain says
$ soma check milestone_escrow.cell
✓ All checks passed.$ soma test milestone_escrow.cell
test MilestoneTests ...
✓ assert fund_project("site", 5000).ok == true
✓ assert accept_milestone("site", "design", 1500).ok == true
✓ assert accept_milestone("site", "build", 2500).ok == true
✓ assert escrow_left("site") == 1000
✓ assert accept_milestone("site", "design", 1500).ok == false
✓ assert_fails accept_milestone("site", "launch", 1800) — raised memory invariant violated on 'escrowed': escrowed >= 0 — rejected write of -800 (key "site"); the slot is unchanged
✓ assert escrow_left("site") == 1000
✓ assert_fails escrowed.set("site", -1) — raised memory invariant violated on 'escrowed': escrowed >= 0 — rejected write of -1 (key "site"); the slot is unchanged
✓ assert finish_project("site").refund_to_client == 1000
✓ assert escrow_left("site") == 0
✓ assert accept_milestone("site", "extra", 100).ok == false
✓ assert_fails transition("site", "cancelled") — raised invalid transition: completed → cancelled. Current state: 'completed'. Valid targets: []
✓ assert_fails transition("site", "funded") — raised invalid transition: completed → funded. Current state: 'completed'. Valid targets: []
✓ assert fund_project("logo", 800).ok == true
✓ assert accept_milestone("logo", "draft", 300).ok == true
✓ assert cancel_project("logo").refund_to_client == 500
✓ assert_fails transition("logo", "completed") — raised invalid transition: cancelled → completed. Current state: 'cancelled'. Valid targets: []
17 tests: 17 passed, 0 failed$ soma verify milestone_escrow.cell
Verifying milestone_escrow.cell...
State machine 'project': 4 states, initial 'proposed'
States: [cancelled, completed, funded, proposed]
✓ 4 states, 3 transitions
✓ all states reachable from 'proposed'
✓ terminal states: [completed, cancelled]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `fund_project` ⟶ {funded}
✓ refinement: handler `finish_project` ⟶ {completed}
✓ refinement: handler `cancel_project` ⟶ {cancelled}
· transition sources: `fund_project`, `finish_project`, `cancel_project` call 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)
MilestoneEscrow/invariants:
✓ invariant escrowed >= 0 — writer 'cancel_project' proven (writes 0)
✓ invariant escrowed >= 0 — writer 'finish_project' proven (writes 0)
✓ invariant escrowed >= 0 — writer 'fund_project' proven by induction (writes amount)
⚠ invariant escrowed >= 0 — runtime-checked (computed values): accept_milestone → escrowed
✓ invariant released >= 0 — writer 'accept_milestone' proven by induction (writes fee)
14 passed, 1 warnings, 0 failures
Temporal properties for 'project':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK