Minutes adoption — the corporate record cannot be edited after the fact
The stock-option backdating scandals of 2006 (over 130 companies under SEC investigation, CEOs of Brocade and Comverse criminally charged) ran on one quiet mechanic: board paperwork written or "fixed" AFTER the fact, dressed up as the record of an earlier date. Minutes are evidence — Delaware courts treat adopted minutes as the authoritative memory of what a board decided. Their value collapses the moment they can be revised after adoption. So adoption here is a one-way door. Amendments append to a numbered revision trail only while the draft circulates; `adopted` is a terminal state soma verify proves, and the adoption ledger holds at most one adoption per document — a second "corrected" adoption of the same minutes is a write the memory refuses.
A Soma program from the governance part of the verified corpus: 115 lines, cells MinuteBook, MinuteBookTests. It passes soma check with soma 3.2.4.
How it is built
The cell MinuteBook declares 5 signals in its face: circulate(doc: String) -> Map, amend(doc: String, change: String) -> Map, adopt(doc: String) -> Map, revision_count(doc: String) -> Int and adopted_once(doc: String) -> Bool; keeps 3 memory slots: adoptions (Map<String, Int>, persistent and consistent) under the invariant adoptions >= 0 && adoptions <= 1, revisions (Map<String, Int>, persistent and consistent) under the invariant revisions >= 0 and edit_log (Map<String, String>, persistent and consistent). Its state machine minutes starts in drafted and allows 2 transitions: drafted -> circulated and circulated -> adopted. adopted is terminal. Handlers: circulate (line 48), amend (line 55), adopt (line 66), revision_count (line 80) and adopted_once (line 84).
The file also holds 1 test cell (MinuteBookTests) with 14 assertions, run by soma test.
The source
minutes_adoption.cell
// ============================================================================
// MINUTES ADOPTION — the corporate record cannot be edited after the fact
// ============================================================================
//
// The stock-option backdating scandals of 2006 (over 130 companies under
// SEC investigation, CEOs of Brocade and Comverse criminally charged)
// ran on one quiet mechanic: board paperwork written or "fixed" AFTER
// the fact, dressed up as the record of an earlier date. Minutes are
// evidence — Delaware courts treat adopted minutes as the authoritative
// memory of what a board decided. Their value collapses the moment they
// can be revised after adoption.
//
// So adoption here is a one-way door. Amendments append to a numbered
// revision trail only while the draft circulates; `adopted` is a
// terminal state soma verify proves, and the adoption ledger holds at
// most one adoption per document — a second "corrected" adoption of the
// same minutes is a write the memory refuses.
// ============================================================================
cell MinuteBook {
face {
signal circulate(doc: String) -> Map
signal amend(doc: String, change: String) -> Map
signal adopt(doc: String) -> Map
signal revision_count(doc: String) -> Int
signal adopted_once(doc: String) -> Bool
}
memory {
// doc -> adoptions. AT MOST ONE: "re-adopting corrected minutes"
// over the originals is unrepresentable.
adoptions: Map<String, Int> [persistent, consistent]
invariant adoptions >= 0 && adoptions <= 1
revisions: Map<String, Int> [persistent, consistent]
invariant revisions >= 0
edit_log: Map<String, String> [persistent, consistent]
}
// drafted -> circulated (amendable, may loop) -> adopted (TERMINAL).
state minutes {
initial: drafted
drafted -> circulated
circulated -> adopted
}
on circulate(doc: String) {
let r = try { transition(doc, "circulated") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "circulated")
}
// amendments are welcome — while the board is still looking at a draft
on amend(doc: String, change: String) {
if get_status(doc) != "circulated" {
let s = get_status(doc)
return map("ok", false, "reason", "minutes are {s}; the record does not bend")
}
let n = (revisions.get(doc) ?? 0) + 1
revisions.set(doc, n)
edit_log.set("{doc}:r{n}", change)
return map("ok", true, "doc", doc, "revision", n)
}
on adopt(doc: String) {
if get_status(doc) != "circulated" {
let s = get_status(doc)
return map("ok", false, "reason", "cannot adopt from {s}")
}
// THE WALL: one adoption, ever
let w = try { adoptions.set(doc, (adoptions.get(doc) ?? 0) + 1) }
if w.error != () {
return map("ok", false, "reason", "{doc} was already adopted; the record stands")
}
transition(doc, "adopted")
return map("ok", true, "state", "adopted", "revisions", revisions.get(doc) ?? 0)
}
on revision_count(doc: String) {
return revisions.get(doc) ?? 0
}
on adopted_once(doc: String) {
return (adoptions.get(doc) ?? 0) == 1
}
}
cell test MinuteBookTests {
rules {
// nothing is amendable before circulation, nothing adoptable from draft
assert amend("jan-meeting", "fix attendee list").ok == false
assert adopt("jan-meeting").ok == false
assert_fails transition("jan-meeting", "adopted")
// circulate; the board marks up the draft freely
assert circulate("jan-meeting").ok == true
assert amend("jan-meeting", "fix attendee list").revision == 1
assert amend("jan-meeting", "correct vote tally on item 4").revision == 2
assert revision_count("jan-meeting") == 2
// adoption closes the book
assert adopt("jan-meeting").ok == true
assert adopted_once("jan-meeting") == true
// THE BACKDATER'S MOVE: edit after adoption. No state to do it in,
// no path back, and a second adoption is a write the memory refuses.
assert amend("jan-meeting", "option grant was 'always' dated June 1").ok == false
assert_fails transition("jan-meeting", "circulated")
assert_fails transition("jan-meeting", "drafted")
assert_fails adoptions.set("jan-meeting", 2)
assert revision_count("jan-meeting") == 2 // the trail is intact
}
}What the toolchain says
$ soma check minutes_adoption.cell
✓ All checks passed.$ soma test minutes_adoption.cell
test MinuteBookTests ...
✓ assert amend("jan-meeting", "fix attendee list").ok == false
✓ assert adopt("jan-meeting").ok == false
✓ assert_fails transition("jan-meeting", "adopted") — raised invalid transition: drafted → adopted. Current state: 'drafted'. Valid targets: [circulated]
✓ assert circulate("jan-meeting").ok == true
✓ assert amend("jan-meeting", "fix attendee list").revision == 1
✓ assert amend("jan-meeting", "correct vote tally on item 4").revision == 2
✓ assert revision_count("jan-meeting") == 2
✓ assert adopt("jan-meeting").ok == true
✓ assert adopted_once("jan-meeting") == true
✓ assert amend("jan-meeting", "option grant was 'always' dated June 1").ok == false
✓ assert_fails transition("jan-meeting", "circulated") — raised invalid transition: adopted → circulated. Current state: 'adopted'. Valid targets: []
✓ assert_fails transition("jan-meeting", "drafted") — raised invalid transition: adopted → drafted. Current state: 'adopted'. Valid targets: []
✓ assert_fails adoptions.set("jan-meeting", 2) — raised memory invariant violated on 'adoptions': adoptions >= 0 && adoptions <= 1 — rejected write of 2 (key "jan-meeting"); the slot is unchanged
✓ assert revision_count("jan-meeting") == 2
14 tests: 14 passed, 0 failed$ soma verify minutes_adoption.cell
Verifying minutes_adoption.cell...
State machine 'minutes': 3 states, initial 'drafted'
States: [adopted, circulated, drafted]
✓ 3 states, 2 transitions
✓ all states reachable from 'drafted'
✓ terminal states: [adopted]
✓ 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 `circulate` ⟶ {circulated}
✓ refinement: handler `adopt` ⟶ {circulated → adopted}
· transition sources: `circulate` calls 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)
MinuteBook/invariants:
✓ invariant adoptions >= 0 — writer 'adopt' proven by induction (writes (adoptions.get(doc) ?? 0) + 1)
⚠ invariant adoptions >= 0 && adoptions <= 1 — runtime-checked (computed values): adopt → adoptions [adoptions <= 1] because `adoptions` has no known range
✓ invariant revisions >= 0 — writer 'amend' proven by induction (writes n)
11 passed, 1 warnings, 0 failures
Temporal properties for 'minutes':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK