Procurement — sealed bids stay sealed, and the unsealing ends the auction
Classic bid-rigging (a DOJ antitrust staple): a procurement officer leaks the standing low bid to a favored vendor, who then "submits" a bid one dollar under it — possible because the system can read bids before close and accept bids after. Both capabilities are removed here, structurally: bid amounts are unreadable until the tender leaves `accepting`, the unsealing transition is the same event that closes submissions forever, and one bid per vendor is a memory invariant — there is no "revised bid" after a peek. `awarded` is terminal: the contract cannot be quietly re-tendered for a do-over.
A Soma program from the civic part of the verified corpus: 112 lines, cells SealedTender, TenderTests. It passes soma check with soma 3.2.4.
How it is built
The cell SealedTender declares 5 signals in its face: submit_bid(vendor: String, amount: Int) -> Map, peek_bids() -> Map, unseal() -> Map, award_contract() -> Map and phase() -> String; keeps 2 memory slots: bid_count (Map<String, Int>, persistent and consistent) under the invariant bid_count >= 0 && bid_count <= 1 and sealed (Map<String, Int>, persistent and consistent) under the invariant sealed >= 1. Its state machine tender starts in accepting and allows 2 transitions: accepting -> unsealed and unsealed -> awarded. awarded is terminal. Handlers: phase (line 42), submit_bid (line 44), peek_bids (line 61), unseal (line 71) and award_contract (line 77).
The file also holds 1 test cell (TenderTests) with 14 assertions, run by soma test.
The source
procurement.cell
// ============================================================================
// PROCUREMENT — sealed bids stay sealed, and the unsealing ends the auction
// ============================================================================
// Classic bid-rigging (a DOJ antitrust staple): a procurement officer leaks
// the standing low bid to a favored vendor, who then "submits" a bid one
// dollar under it — possible because the system can read bids before close
// and accept bids after. Both capabilities are removed here, structurally:
// bid amounts are unreadable until the tender leaves `accepting`, the
// unsealing transition is the same event that closes submissions forever,
// and one bid per vendor is a memory invariant — there is no "revised bid"
// after a peek. `awarded` is terminal: the contract cannot be quietly
// re-tendered for a do-over.
// ============================================================================
cell SealedTender {
face {
signal submit_bid(vendor: String, amount: Int) -> Map
signal peek_bids() -> Map
signal unseal() -> Map
signal award_contract() -> Map
signal phase() -> String
}
memory {
// vendor -> bids submitted. A second (revised) bid is unrepresentable.
bid_count: Map<String, Int> [persistent, consistent]
invariant bid_count >= 0 && bid_count <= 1
// amounts must be positive — a $0 placeholder bid is refused.
sealed: Map<String, Int> [persistent, consistent]
invariant sealed >= 1
}
// One arrow forward only: unsealing closes submissions, awarding
// closes the tender. No state re-opens the box.
state tender {
initial: accepting
accepting -> unsealed
unsealed -> awarded
}
on phase() { return get_status("tender") }
on submit_bid(vendor: String, amount: Int) {
if phase() != "accepting" {
return map("ok", false, "reason", "tender is {phase()}")
}
let prior = bid_count.get(vendor) ?? 0
let c = try { bid_count.set(vendor, prior + 1) }
if c.error != () {
return map("ok", false, "reason", "{vendor} already bid — no revisions")
}
let w = try { sealed.set(vendor, amount) }
if w.error != () {
return map("ok", false, "reason", "bid must be at least 1")
}
return map("ok", true, "vendor", vendor)
}
// The leak, refused: while accepting, amounts are not readable.
on peek_bids() {
if phase() == "accepting" {
return map("ok", false, "reason", "bids are sealed until opening")
}
let names = sealed.keys()
let out = map()
for v in names { out[v] = sealed.get(v) ?? 0 }
return map("ok", true, "bids", out)
}
on unseal() {
let r = try { transition("tender", "unsealed") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "bidders", len(sealed.keys()))
}
on award_contract() {
let r = try { transition("tender", "awarded") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
let names = sealed.keys()
let best = ""
let low = 0
for v in names {
let amt = sealed.get(v) ?? 0
if best == "" || amt < low {
best = v
low = amt
}
}
return map("ok", true, "winner", best, "amount", low)
}
}
cell test TenderTests {
rules {
assert submit_bid("acme", 100).ok == true
assert submit_bid("rival", 90).ok == true
assert peek_bids().ok == false // sealed means sealed
assert submit_bid("acme", 89).ok == false // no revised bid
assert_fails bid_count.set("acme", 2) // unrepresentable
assert_fails sealed.set("ghost", 0) // no placeholder bids
assert award_contract().ok == false // can't award sealed bids
assert unseal().ok == true
assert submit_bid("late", 1).ok == false // unsealing closed the door
assert peek_bids().ok == true
assert award_contract().winner == "rival"
assert phase() == "awarded"
assert_fails transition("tender", "accepting") // no re-tender
assert_fails transition("tender", "unsealed")
}
}What the toolchain says
$ soma check procurement.cell
✓ All checks passed.$ soma test procurement.cell
test TenderTests ...
✓ assert submit_bid("acme", 100).ok == true
✓ assert submit_bid("rival", 90).ok == true
✓ assert peek_bids().ok == false
✓ assert submit_bid("acme", 89).ok == false
✓ assert_fails bid_count.set("acme", 2) — raised memory invariant violated on 'bid_count': bid_count >= 0 && bid_count <= 1 — rejected write of 2 (key "acme"); the slot is unchanged
✓ assert_fails sealed.set("ghost", 0) — raised memory invariant violated on 'sealed': sealed >= 1 — rejected write of 0 (key "ghost"); the slot is unchanged
✓ assert award_contract().ok == false
✓ assert unseal().ok == true
✓ assert submit_bid("late", 1).ok == false
✓ assert peek_bids().ok == true
✓ assert award_contract().winner == "rival"
✓ assert phase() == "awarded"
✓ assert_fails transition("tender", "accepting") — raised invalid transition: awarded → accepting. Current state: 'awarded'. Valid targets: []
✓ assert_fails transition("tender", "unsealed") — raised invalid transition: awarded → unsealed. Current state: 'awarded'. Valid targets: []
14 tests: 14 passed, 0 failed$ soma verify procurement.cell
Verifying procurement.cell...
State machine 'tender': 3 states, initial 'accepting'
States: [accepting, awarded, unsealed]
✓ 3 states, 2 transitions
✓ all states reachable from 'accepting'
✓ terminal states: [awarded]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 2 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `unseal` ⟶ {unsealed}
✓ refinement: handler `award_contract` ⟶ {awarded}
· transition sources: `unseal`, `award_contract` 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)
SealedTender/invariants:
✓ invariant bid_count >= 0 — writer 'submit_bid' proven by induction (writes prior + 1)
⚠ invariant bid_count >= 0 && bid_count <= 1 — runtime-checked (computed values): submit_bid → bid_count [bid_count <= 1] because `prior + 1` is only known to lie in [1, 2] — narrow it: `require (prior + 1) <= 1 else …`
⚠ invariant sealed >= 1 — runtime-checked (computed values): submit_bid → sealed because `amount` is a parameter (narrow it: `require amount >= 1 else …`)
10 passed, 2 warnings, 0 failures
Temporal properties for 'tender':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK