soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/escrow_finance/multisig_disburse.cell · examples/corpus/escrow_finance/multisig_disburse.cell