Term limits — the third term is not forbidden, it is unrepresentable
In 2008, New York's City Council — at Mayor Bloomberg's urging — voted 29-22 to extend its own term limits so the sitting mayor could run again, overriding two public referenda in which New Yorkers had twice voted for a two-term cap. It was legal precisely because the limit lived in an ordinary statute the limited officials themselves could amend. The U.S. answer to FDR's four terms was different: the 22nd Amendment put the cap somewhere no incumbent can reach. This module is the 22nd-Amendment version. The terms ledger carries `invariant terms <= 2` — certifying a third term for the same person is a WRITE THE MEMORY REFUSES, and there is no handler anywhere that can loosen an invariant at runtime. Each term also walks a machine whose `vacated` state is terminal: an ended term cannot be revived as a sneaky continuation of itself.
A Soma program from the governance part of the verified corpus: 128 lines, cells TermRegistry, TermLimitTests. It passes soma check with soma 3.2.4.
How it is built
The cell TermRegistry declares 5 signals in its face: nominate(person: String, term_id: String) -> Map, certify_win(person: String, term_id: String) -> Map, inaugurate(term_id: String) -> Map, vacate(term_id: String) -> Map and terms_served(person: String) -> Int; keeps 2 memory slots: terms (Map<String, Int>, persistent and consistent) under the invariant terms >= 0 && terms <= 2 and winners (Map<String, String>, persistent and consistent). Its state machine term starts in open_seat and allows 5 transitions: open_seat -> nominated, nominated -> won, won -> sworn_in, sworn_in -> vacated and nominated -> lost. lost and vacated are terminal. Handlers: nominate (line 50), certify_win (line 60), inaugurate (line 77), vacate (line 83) and terms_served (line 89).
The file also holds 1 test cell (TermLimitTests) with 17 assertions, run by soma test.
The source
term_limits.cell
// ============================================================================
// TERM LIMITS — the third term is not forbidden, it is unrepresentable
// ============================================================================
//
// In 2008, New York's City Council — at Mayor Bloomberg's urging —
// voted 29-22 to extend its own term limits so the sitting mayor could
// run again, overriding two public referenda in which New Yorkers had
// twice voted for a two-term cap. It was legal precisely because the
// limit lived in an ordinary statute the limited officials themselves
// could amend. The U.S. answer to FDR's four terms was different: the
// 22nd Amendment put the cap somewhere no incumbent can reach.
//
// This module is the 22nd-Amendment version. The terms ledger carries
// `invariant terms <= 2` — certifying a third term for the same person
// is a WRITE THE MEMORY REFUSES, and there is no handler anywhere that
// can loosen an invariant at runtime. Each term also walks a machine
// whose `vacated` state is terminal: an ended term cannot be revived
// as a sneaky continuation of itself.
// ============================================================================
cell TermRegistry {
face {
signal nominate(person: String, term_id: String) -> Map
signal certify_win(person: String, term_id: String) -> Map
signal inaugurate(term_id: String) -> Map
signal vacate(term_id: String) -> Map
signal terms_served(person: String) -> Int
}
memory {
// person -> terms certified, lifetime. 3 does not exist.
terms: Map<String, Int> [persistent, consistent]
invariant terms >= 0 && terms <= 2
winners: Map<String, String> [persistent, consistent]
}
// nominated -> won -> sworn_in -> vacated (TERMINAL).
// The office is re-filled only through a NEW term id — a new
// nomination, a new election, a fresh certification against the cap.
state term {
initial: open_seat
open_seat -> nominated
nominated -> won
won -> sworn_in
sworn_in -> vacated
nominated -> lost
}
on nominate(person: String, term_id: String) {
// the ballot gate: someone already at the cap cannot even run
if (terms.get(person) ?? 0) >= 2 {
return map("ok", false, "reason", "{person} has served 2 terms; the ballot is closed")
}
let r = try { transition(term_id, "nominated") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "candidate", person)
}
on certify_win(person: String, term_id: String) {
if get_status(term_id) != "nominated" {
let s = get_status(term_id)
return map("ok", false, "reason", "nothing to certify from {s}")
}
// THE WALL: even if the ballot gate above were repealed by a
// friendly council, the third certification is a write of 3 —
// and the ledger refuses it.
let w = try { terms.set(person, (terms.get(person) ?? 0) + 1) }
if w.error != () {
return map("ok", false, "reason", "22nd Amendment: no third term for {person}")
}
transition(term_id, "won")
winners.set(term_id, person)
return map("ok", true, "person", person, "terms", terms.get(person))
}
on inaugurate(term_id: String) {
let r = try { transition(term_id, "sworn_in") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "holder", winners.get(term_id))
}
on vacate(term_id: String) {
let r = try { transition(term_id, "vacated") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "vacated")
}
on terms_served(person: String) {
return terms.get(person) ?? 0
}
}
cell test TermLimitTests {
rules {
// term one: nominate, win, swear in, and eventually vacate
assert nominate("bloomberg", "t2002").ok == true
assert certify_win("bloomberg", "t2002").terms == 1
assert inaugurate("t2002").holder == "bloomberg"
assert vacate("t2002").ok == true
// a vacated term is dead — no continuation-in-place
assert_fails transition("t2002", "sworn_in")
assert_fails transition("t2002", "won")
// term two, through a brand-new term id
assert nominate("bloomberg", "t2005").ok == true
assert certify_win("bloomberg", "t2005").terms == 2
assert inaugurate("t2005").ok == true
assert vacate("t2005").ok == true
// THE 2008 MOVE: the third run. The ballot gate refuses —
// and even a "council override" of that gate hits the memory.
assert nominate("bloomberg", "t2009").ok == false
assert_fails terms.set("bloomberg", 3)
assert terms_served("bloomberg") == 2
// a rigged certification with no election behind it also dies:
// t2009 was never nominated, so there is nothing to certify
assert certify_win("bloomberg", "t2009").ok == false
assert_fails transition("t2009", "won")
// the office itself stays alive — for somebody else
assert nominate("thompson", "t2009").ok == true
assert certify_win("thompson", "t2009").terms == 1
}
}What the toolchain says
$ soma check term_limits.cell
✓ All checks passed.$ soma test term_limits.cell
test TermLimitTests ...
✓ assert nominate("bloomberg", "t2002").ok == true
✓ assert certify_win("bloomberg", "t2002").terms == 1
✓ assert inaugurate("t2002").holder == "bloomberg"
✓ assert vacate("t2002").ok == true
✓ assert_fails transition("t2002", "sworn_in") — raised invalid transition: vacated → sworn_in. Current state: 'vacated'. Valid targets: []
✓ assert_fails transition("t2002", "won") — raised invalid transition: vacated → won. Current state: 'vacated'. Valid targets: []
✓ assert nominate("bloomberg", "t2005").ok == true
✓ assert certify_win("bloomberg", "t2005").terms == 2
✓ assert inaugurate("t2005").ok == true
✓ assert vacate("t2005").ok == true
✓ assert nominate("bloomberg", "t2009").ok == false
✓ assert_fails terms.set("bloomberg", 3) — raised memory invariant violated on 'terms': terms >= 0 && terms <= 2 — rejected write of 3 (key "bloomberg"); the slot is unchanged
✓ assert terms_served("bloomberg") == 2
✓ assert certify_win("bloomberg", "t2009").ok == false
✓ assert_fails transition("t2009", "won") — raised invalid transition: open_seat → won. Current state: 'open_seat'. Valid targets: [nominated]
✓ assert nominate("thompson", "t2009").ok == true
✓ assert certify_win("thompson", "t2009").terms == 1
17 tests: 17 passed, 0 failed$ soma verify term_limits.cell
Verifying term_limits.cell...
State machine 'term': 6 states, initial 'open_seat'
States: [lost, nominated, open_seat, sworn_in, vacated, won]
✓ 6 states, 5 transitions
✓ all states reachable from 'open_seat'
✓ terminal states: [vacated, lost]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
⚠ refinement: declared transition `nominated → lost` is never reached by any handler — spec may be aspirational or stale
✓ refinement: handler `nominate` ⟶ {nominated}
✓ refinement: handler `certify_win` ⟶ {nominated → won}
✓ refinement: handler `inaugurate` ⟶ {sworn_in}
✓ refinement: handler `vacate` ⟶ {vacated}
· transition sources: `nominate`, `inaugurate`, `vacate` 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)
TermRegistry/invariants:
✓ invariant terms >= 0 — writer 'certify_win' proven by induction (writes (terms.get(person) ?? 0) + 1)
⚠ invariant terms >= 0 && terms <= 2 — runtime-checked (computed values): certify_win → terms [terms <= 2] because `terms` has no known range
12 passed, 2 warnings, 0 failures
Temporal properties for 'term':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK