Multisig treasury — 2-of-3 distinct approvals, proven before a cent moves
In July 2017 the Parity multisig wallet lost $30M because a code path let a single caller re-initialize ownership and drain funds alone — the "multi" in multisig was a convention, not a structure. Here the quorum IS the structure: disbursed is reachable ONLY through the quorum state, which requires two approvals from DISTINCT owners (a repeat approval does not advance the machine). `soma verify` proves the only path to disbursed passes through quorum; the vault refuses negative balances.
A Soma program from the escrow_finance part of the verified corpus: 109 lines, cells Multisig, MultisigTests. It passes soma check with soma 3.2.4.
How it is built
The cell Multisig declares 4 signals in its face: propose(id: String, amount: Int) -> Map, approve_txn(id: String, owner: String) -> Map, disburse(id: String) -> Map and vault_balance() -> Int; keeps 3 memory slots: vault (Map<String, Int>, persistent and consistent) under the invariant vault >= 0, votes (Map<String, Int>, persistent and consistent) and amounts (Map<String, Int>, persistent and consistent) under the invariant amounts >= 0. Its state machine txn starts in drafted and allows 4 transitions: drafted -> proposed, proposed -> one_approval, one_approval -> quorum and quorum -> disbursed. disbursed is terminal. Handlers: propose (line 40), approve_txn (line 51), disburse (line 70) and vault_balance (line 78).
The file also holds 1 test cell (MultisigTests) with 14 assertions, run by soma test.
The source
multisig_disburse.cell
// ============================================================================
// MULTISIG TREASURY — 2-of-3 distinct approvals, proven before a cent moves
// ============================================================================
//
// In July 2017 the Parity multisig wallet lost $30M because a code path let
// a single caller re-initialize ownership and drain funds alone — the
// "multi" in multisig was a convention, not a structure. Here the quorum IS
// the structure: disbursed is reachable ONLY through the quorum state,
// which requires two approvals from DISTINCT owners (a repeat approval
// does not advance the machine). `soma verify` proves the only path to
// disbursed passes through quorum; the vault refuses negative balances.
// ============================================================================
cell Multisig {
face {
signal propose(id: String, amount: Int) -> Map
signal approve_txn(id: String, owner: String) -> Map
signal disburse(id: String) -> Map
signal vault_balance() -> Int
}
memory {
vault: Map<String, Int> [persistent, consistent]
invariant vault >= 0
votes: Map<String, Int> [persistent, consistent]
amounts: Map<String, Int> [persistent, consistent]
invariant amounts >= 0
}
// disbursed is terminal, and its ONLY parent is quorum.
// There is no proposed -> disbursed, no one_approval -> disbursed.
state txn {
initial: drafted
drafted -> proposed
proposed -> one_approval
one_approval -> quorum
quorum -> disbursed
}
on propose(id: String, amount: Int) {
if vault.get("treasury") == () { vault.set("treasury", 100000) }
let bal = vault.get("treasury") ?? 0
if amount <= 0 || amount > bal {
return map("ok", false, "reason", "amount must be in (0, {bal}]")
}
transition(id, "proposed")
amounts.set(id, amount)
return map("ok", true, "state", get_status(id))
}
on approve_txn(id: String, owner: String) {
if owner != "alice" && owner != "bob" && owner != "carol" {
return map("ok", false, "reason", "not an owner")
}
let k = "{id}:{owner}"
if (votes.get(k) ?? 0) == 1 {
// a repeat vote by the same owner does NOT advance the machine
return map("ok", false, "reason", "{owner} already approved")
}
let st = get_status(id)
if st == "proposed" { transition(id, "one_approval") }
if st == "one_approval" { transition(id, "quorum") }
if st != "proposed" && st != "one_approval" {
return map("ok", false, "reason", "no approval needed in state {st}")
}
votes.set(k, 1)
return map("ok", true, "state", get_status(id))
}
on disburse(id: String) {
transition(id, "disbursed") // raises unless at quorum
let amt = amounts.get(id) ?? 0
let bal = vault.get("treasury") ?? 0
vault.set("treasury", bal - amt) // and the vault refuses overdraw
return map("ok", true, "paid", amt, "vault", bal - amt)
}
on vault_balance() {
return vault.get("treasury") ?? 0
}
}
cell test MultisigTests {
rules {
assert propose("t1", 40000).ok == true
// PARITY MOVE: disburse with zero approvals — the edge does not exist
assert_fails transition("t1", "disbursed")
assert approve_txn("t1", "alice").ok == true
// one signature is not quorum
assert_fails transition("t1", "disbursed")
// the SAME owner approving twice does not fake a quorum
assert approve_txn("t1", "alice").ok == false
assert_fails transition("t1", "disbursed")
// a stranger cannot vote
assert approve_txn("t1", "mallory").ok == false
// a second DISTINCT owner completes the quorum
assert approve_txn("t1", "bob").ok == true
assert disburse("t1").paid == 40000
assert vault_balance() == 60000
// disbursed is terminal: the same txn cannot pay twice
assert_fails transition("t1", "quorum")
assert_fails transition("t1", "disbursed")
// the vault itself cannot go negative
assert_fails vault.set("treasury", -1)
// a proposal larger than the vault is refused up front
assert propose("t2", 999999).ok == false
}
}What the toolchain says
$ soma check multisig_disburse.cell
✓ All checks passed.$ soma test multisig_disburse.cell
test MultisigTests ...
✓ assert propose("t1", 40000).ok == true
✓ assert_fails transition("t1", "disbursed") — raised invalid transition: proposed → disbursed. Current state: 'proposed'. Valid targets: [one_approval]
✓ assert approve_txn("t1", "alice").ok == true
✓ assert_fails transition("t1", "disbursed") — raised invalid transition: one_approval → disbursed. Current state: 'one_approval'. Valid targets: [quorum]
✓ assert approve_txn("t1", "alice").ok == false
✓ assert_fails transition("t1", "disbursed") — raised invalid transition: one_approval → disbursed. Current state: 'one_approval'. Valid targets: [quorum]
✓ assert approve_txn("t1", "mallory").ok == false
✓ assert approve_txn("t1", "bob").ok == true
✓ assert disburse("t1").paid == 40000
✓ assert vault_balance() == 60000
✓ assert_fails transition("t1", "quorum") — raised invalid transition: disbursed → quorum. Current state: 'disbursed'. Valid targets: []
✓ assert_fails transition("t1", "disbursed") — raised invalid transition: disbursed → disbursed. Current state: 'disbursed'. Valid targets: []
✓ assert_fails vault.set("treasury", -1) — raised memory invariant violated on 'vault': vault >= 0 — rejected write of -1 (key "treasury"); the slot is unchanged
✓ assert propose("t2", 999999).ok == false
14 tests: 14 passed, 0 failed$ soma verify multisig_disburse.cell
Verifying multisig_disburse.cell...
State machine 'txn': 5 states, initial 'drafted'
States: [disbursed, drafted, one_approval, proposed, quorum]
✓ 5 states, 4 transitions
✓ all states reachable from 'drafted'
✓ terminal states: [disbursed]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 4 handlers structurally terminate
✓ refinement: handler `propose` ⟶ {proposed}
✓ refinement: handler `approve_txn` ⟶ {proposed → one_approval [if st == "proposed"], one_approval → quorum [if st == "one_approval"]}
✓ refinement: handler `disburse` ⟶ {disbursed}
· transition sources: `propose`, `disburse` 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)
Multisig/invariants:
✓ invariant vault >= 0 — writer 'propose' proven (writes 100000)
⚠ invariant vault >= 0 — runtime-checked (computed values): disburse → vault
✓ invariant amounts >= 0 — writer 'propose' proven by induction (writes amount)
12 passed, 1 warnings, 0 failures
Temporal properties for 'txn':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK