Invoice factoring — no advance on unverified paper, no double-selling
Greensill Capital collapsed in 2021 holding billions in "invoices" that were never verified — some for trade that hadn't happened, some financed twice through different vehicles. The two frauds are structural here: an invoice can only be SOLD from the verified state (the issued -> sold edge does not exist), and sold has no edge back to itself or to verified, so the same invoice cannot be advanced twice. The advance ledger caps the cash at 90% of face value and refuses negative writes.
A Soma program from the escrow_finance part of the verified corpus: 108 lines, cells Factoring, FactoringTests. It passes soma check with soma 3.2.4.
How it is built
The cell Factoring declares 6 signals in its face: issue_invoice(id: String, face_value: Int) -> Map, verify_delivery(id: String) -> Map, sell_invoice(id: String, advance: Int) -> Map, collect(id: String) -> Map, write_off(id: String) -> Map and advance_paid(id: String) -> Int; keeps 2 memory slots: advanced (Map<String, Int>, persistent and consistent) under the invariant advanced >= 0 and face_val (Map<String, Int>, persistent and consistent) under the invariant face_val >= 0. Its state machine invoice starts in drafted and allows 5 transitions: drafted -> issued, issued -> verified, verified -> sold, sold -> collected and sold -> defaulted. collected and defaulted are terminal. Handlers: issue_invoice (line 42), verify_delivery (line 50), sell_invoice (line 55), collect (line 65), write_off (line 72) and advance_paid (line 77).
The file also holds 1 test cell (FactoringTests) with 16 assertions, run by soma test.
The source
invoice_factoring.cell
// ============================================================================
// INVOICE FACTORING — no advance on unverified paper, no double-selling
// ============================================================================
//
// Greensill Capital collapsed in 2021 holding billions in "invoices" that
// were never verified — some for trade that hadn't happened, some financed
// twice through different vehicles. The two frauds are structural here:
// an invoice can only be SOLD from the verified state (the issued -> sold
// edge does not exist), and sold has no edge back to itself or to verified,
// so the same invoice cannot be advanced twice. The advance ledger caps
// the cash at 90% of face value and refuses negative writes.
// ============================================================================
cell Factoring {
face {
signal issue_invoice(id: String, face_value: Int) -> Map
signal verify_delivery(id: String) -> Map
signal sell_invoice(id: String, advance: Int) -> Map
signal collect(id: String) -> Map
signal write_off(id: String) -> Map
signal advance_paid(id: String) -> Int
}
memory {
advanced: Map<String, Int> [persistent, consistent]
invariant advanced >= 0
face_val: Map<String, Int> [persistent, consistent]
invariant face_val >= 0
}
// collected and defaulted are terminal. The fraud edges are ABSENT:
// no issued -> sold (unverified paper), no sold -> sold (double-sale).
state invoice {
initial: drafted
drafted -> issued
issued -> verified
verified -> sold
sold -> collected
sold -> defaulted
}
on issue_invoice(id: String, face_value: Int) {
if face_value <= 0 { return map("ok", false, "reason", "bad face value") }
transition(id, "issued")
face_val.set(id, face_value)
advanced.set(id, 0)
return map("ok", true, "state", get_status(id))
}
on verify_delivery(id: String) {
transition(id, "verified") // raises unless invoice was issued
return map("ok", true, "state", get_status(id))
}
on sell_invoice(id: String, advance: Int) {
let fv = face_val.get(id) ?? 0
if advance <= 0 || advance * 10 > fv * 9 {
return map("ok", false, "reason", "advance must be in (0, 90% of {fv}]")
}
transition(id, "sold") // raises unless verified — and only once
advanced.set(id, advance)
return map("ok", true, "advance", advance, "face", fv)
}
on collect(id: String) {
transition(id, "collected")
let fv = face_val.get(id) ?? 0
let adv = advanced.get(id) ?? 0
return map("ok", true, "rebate_to_seller", fv - adv)
}
on write_off(id: String) {
transition(id, "defaulted")
return map("ok", true, "loss", advanced.get(id) ?? 0)
}
on advance_paid(id: String) {
return advanced.get(id) ?? 0
}
}
cell test FactoringTests {
rules {
assert issue_invoice("inv1", 10000).ok == true
// GREENSILL MOVE 1: advance cash on unverified paper — edge absent
assert_fails transition("inv1", "sold")
assert verify_delivery("inv1").ok == true
// advance capped at 90% of face
assert sell_invoice("inv1", 9500).ok == false
assert sell_invoice("inv1", 9000).ok == true
assert advance_paid("inv1") == 9000
// GREENSILL MOVE 2: sell the same invoice again — no sold -> sold
assert_fails transition("inv1", "sold")
assert_fails transition("inv1", "verified")
// the ledger refuses a negative advance outright
assert_fails advanced.set("inv1", -1)
// collection is terminal; a collected invoice cannot default too
assert collect("inv1").rebate_to_seller == 1000
assert_fails transition("inv1", "defaulted")
// default path on a second invoice, equally final
assert issue_invoice("inv2", 5000).ok == true
assert verify_delivery("inv2").ok == true
assert sell_invoice("inv2", 4000).ok == true
assert write_off("inv2").loss == 4000
assert_fails transition("inv2", "collected")
}
}What the toolchain says
$ soma check invoice_factoring.cell
✓ All checks passed.$ soma test invoice_factoring.cell
test FactoringTests ...
✓ assert issue_invoice("inv1", 10000).ok == true
✓ assert_fails transition("inv1", "sold") — raised invalid transition: issued → sold. Current state: 'issued'. Valid targets: [verified]
✓ assert verify_delivery("inv1").ok == true
✓ assert sell_invoice("inv1", 9500).ok == false
✓ assert sell_invoice("inv1", 9000).ok == true
✓ assert advance_paid("inv1") == 9000
✓ assert_fails transition("inv1", "sold") — raised invalid transition: sold → sold. Current state: 'sold'. Valid targets: [collected, defaulted]
✓ assert_fails transition("inv1", "verified") — raised invalid transition: sold → verified. Current state: 'sold'. Valid targets: [collected, defaulted]
✓ assert_fails advanced.set("inv1", -1) — raised memory invariant violated on 'advanced': advanced >= 0 — rejected write of -1 (key "inv1"); the slot is unchanged
✓ assert collect("inv1").rebate_to_seller == 1000
✓ assert_fails transition("inv1", "defaulted") — raised invalid transition: collected → defaulted. Current state: 'collected'. Valid targets: []
✓ assert issue_invoice("inv2", 5000).ok == true
✓ assert verify_delivery("inv2").ok == true
✓ assert sell_invoice("inv2", 4000).ok == true
✓ assert write_off("inv2").loss == 4000
✓ assert_fails transition("inv2", "collected") — raised invalid transition: defaulted → collected. Current state: 'defaulted'. Valid targets: []
16 tests: 16 passed, 0 failed$ soma verify invoice_factoring.cell
Verifying invoice_factoring.cell...
State machine 'invoice': 6 states, initial 'drafted'
States: [collected, defaulted, drafted, issued, sold, verified]
✓ 6 states, 5 transitions
✓ all states reachable from 'drafted'
✓ terminal states: [collected, defaulted]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 5 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `issue_invoice` ⟶ {issued}
✓ refinement: handler `verify_delivery` ⟶ {verified}
✓ refinement: handler `sell_invoice` ⟶ {sold}
✓ refinement: handler `collect` ⟶ {collected}
✓ refinement: handler `write_off` ⟶ {defaulted}
· transition sources: `issue_invoice`, `verify_delivery`, `sell_invoice`, `collect`, `write_off` 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)
Factoring/invariants:
✓ invariant advanced >= 0 — writer 'issue_invoice' proven (writes 0)
✓ invariant advanced >= 0 — writer 'sell_invoice' proven by induction (writes advance)
✓ invariant face_val >= 0 — writer 'issue_invoice' proven by induction (writes face_value)
15 passed, 0 warnings, 0 failures
Temporal properties for 'invoice':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK