Peer review — double-blind where the blind cannot be lifted early
Double-blind review exists because the data says it must: when reviewers see author names, papers from famous labs are accepted at measurably higher rates (the NeurIPS 2014 and 2021 consistency experiments put numbers on how noisy and biased single-blind judging is). The whole mechanism collapses on two failure modes: an author reviewing their own paper under a conflict, and the author's identity leaking to the reviewer BEFORE the decision is locked. Both are structural here. A reviewer/author pair can hold at most one role on a paper — self-review is a write the memory refuses. And `unmasked` is reachable ONLY from `decided`: there is no edge from any pre-decision state to the unmasked world. soma verify proves it.
A Soma program from the governance part of the verified corpus: 132 lines, cells ReviewDesk, BlindTests. It passes soma check with soma 3.2.4.
How it is built
The cell ReviewDesk declares 6 signals in its face: submit_paper(paper: String, author: String) -> Map, assign_reviewer(paper: String, reviewer: String) -> Map, decide(paper: String, accept: Bool) -> Map, lift_blind(paper: String) -> Map, author_of(paper: String) -> String and verdict_of(paper: String) -> String; keeps 3 memory slots: blind_roles (Map<String, Int>, persistent and consistent) under the invariant blind_roles >= 0 && blind_roles <= 1, authors (Map<String, String>, persistent and consistent) and verdicts (Map<String, String>, persistent and consistent). Its state machine blind starts in sealed and allows 3 transitions: sealed -> in_review, in_review -> decided and decided -> unmasked. unmasked is terminal. Handlers: submit_paper (line 49), assign_reviewer (line 58), decide (line 73), lift_blind (line 81), author_of (line 88) and verdict_of (line 95).
The file also holds 1 test cell (BlindTests) with 18 assertions, run by soma test.
The source
peer_review.cell
// ============================================================================
// PEER REVIEW — double-blind where the blind cannot be lifted early
// ============================================================================
//
// Double-blind review exists because the data says it must: when
// reviewers see author names, papers from famous labs are accepted at
// measurably higher rates (the NeurIPS 2014 and 2021 consistency
// experiments put numbers on how noisy and biased single-blind judging
// is). The whole mechanism collapses on two failure modes: an author
// reviewing their own paper under a conflict, and the author's identity
// leaking to the reviewer BEFORE the decision is locked.
//
// Both are structural here. A reviewer/author pair can hold at most one
// role on a paper — self-review is a write the memory refuses. And
// `unmasked` is reachable ONLY from `decided`: there is no edge from any
// pre-decision state to the unmasked world. soma verify proves it.
// ============================================================================
cell ReviewDesk {
face {
signal submit_paper(paper: String, author: String) -> Map
signal assign_reviewer(paper: String, reviewer: String) -> Map
signal decide(paper: String, accept: Bool) -> Map
signal lift_blind(paper: String) -> Map
signal author_of(paper: String) -> String
signal verdict_of(paper: String) -> String
}
memory {
// paper:person -> roles held (author or reviewer). A 2 — the
// same person on both sides of the blind — is unrepresentable.
blind_roles: Map<String, Int> [persistent, consistent]
invariant blind_roles >= 0 && blind_roles <= 1
authors: Map<String, String> [persistent, consistent]
verdicts: Map<String, String> [persistent, consistent]
}
// The blind is a place in the machine, not a flag. There is NO edge
// from sealed/in_review to unmasked: identity stays behind the
// decision. unmasked is terminal — once lifted, the record is final.
state blind {
initial: sealed
sealed -> in_review
in_review -> decided
decided -> unmasked
}
on submit_paper(paper: String, author: String) {
if authors.get(paper) != () {
return map("ok", false, "reason", "paper {paper} already submitted")
}
authors.set(paper, author)
blind_roles.set("{paper}:{author}", 1)
return map("ok", true, "paper", paper)
}
on assign_reviewer(paper: String, reviewer: String) {
if get_status(paper) != "sealed" {
let s = get_status(paper)
return map("ok", false, "reason", "cannot assign in state {s}")
}
// THE WALL: if the reviewer wrote the paper, this write is a 2
let k = "{paper}:{reviewer}"
let w = try { blind_roles.set(k, (blind_roles.get(k) ?? 0) + 1) }
if w.error != () {
return map("ok", false, "reason", "conflict: {reviewer} cannot review their own paper")
}
transition(paper, "in_review")
return map("ok", true, "reviewer", reviewer)
}
on decide(paper: String, accept: Bool) {
let r = try { transition(paper, "decided") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
if accept { verdicts.set(paper, "accept") }
if !accept { verdicts.set(paper, "reject") }
return map("ok", true, "verdict", verdicts.get(paper))
}
on lift_blind(paper: String) {
let r = try { transition(paper, "unmasked") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "author", authors.get(paper))
}
// identity is served ONLY past the decision — the machine is the gate
on author_of(paper: String) {
if get_status(paper) != "unmasked" {
return "[REDACTED]"
}
return authors.get(paper) ?? "[unknown]"
}
on verdict_of(paper: String) {
return verdicts.get(paper) ?? "pending"
}
}
cell test BlindTests {
rules {
assert submit_paper("P7", "prof_x").ok == true
assert submit_paper("P7", "prof_x").ok == false // no resubmission
// self-review: the role ledger cannot hold the 2
assert assign_reviewer("P7", "prof_x").ok == false
assert_fails blind_roles.set("P7:prof_x", 2)
assert get_status("P7") == "sealed"
// the blind cannot be lifted before a decision — no such edge
assert_fails transition("P7", "unmasked")
assert author_of("P7") == "[REDACTED]"
// an honest reviewer goes through; identity still sealed
assert assign_reviewer("P7", "dr_y").ok == true
assert_fails transition("P7", "unmasked") // mid-review leak: no edge
assert author_of("P7") == "[REDACTED]"
assert lift_blind("P7").ok == false
// decision locks the verdict; only THEN may the blind lift
assert decide("P7", true).verdict == "accept"
assert author_of("P7") == "[REDACTED]" // decided != unmasked yet
assert lift_blind("P7").ok == true
assert author_of("P7") == "prof_x"
// unmasked is terminal: the record cannot re-enter review
assert_fails transition("P7", "in_review")
assert_fails transition("P7", "sealed")
assert verdict_of("P7") == "accept"
}
}What the toolchain says
$ soma check peer_review.cell
✓ All checks passed.$ soma test peer_review.cell
test BlindTests ...
✓ assert submit_paper("P7", "prof_x").ok == true
✓ assert submit_paper("P7", "prof_x").ok == false
✓ assert assign_reviewer("P7", "prof_x").ok == false
✓ assert_fails blind_roles.set("P7:prof_x", 2) — raised memory invariant violated on 'blind_roles': blind_roles >= 0 && blind_roles <= 1 — rejected write of 2 (key "P7:prof_x"); the slot is unchanged
✓ assert get_status("P7") == "sealed"
✓ assert_fails transition("P7", "unmasked") — raised invalid transition: sealed → unmasked. Current state: 'sealed'. Valid targets: [in_review]
✓ assert author_of("P7") == "[REDACTED]"
✓ assert assign_reviewer("P7", "dr_y").ok == true
✓ assert_fails transition("P7", "unmasked") — raised invalid transition: in_review → unmasked. Current state: 'in_review'. Valid targets: [decided]
✓ assert author_of("P7") == "[REDACTED]"
✓ assert lift_blind("P7").ok == false
✓ assert decide("P7", true).verdict == "accept"
✓ assert author_of("P7") == "[REDACTED]"
✓ assert lift_blind("P7").ok == true
✓ assert author_of("P7") == "prof_x"
✓ assert_fails transition("P7", "in_review") — raised invalid transition: unmasked → in_review. Current state: 'unmasked'. Valid targets: []
✓ assert_fails transition("P7", "sealed") — raised invalid transition: unmasked → sealed. Current state: 'unmasked'. Valid targets: []
✓ assert verdict_of("P7") == "accept"
18 tests: 18 passed, 0 failed$ soma verify peer_review.cell
Verifying peer_review.cell...
State machine 'blind': 4 states, initial 'sealed'
States: [decided, in_review, sealed, unmasked]
✓ 4 states, 3 transitions
✓ all states reachable from 'sealed'
✓ terminal states: [unmasked]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `assign_reviewer` ⟶ {sealed → in_review}
✓ refinement: handler `decide` ⟶ {decided}
✓ refinement: handler `lift_blind` ⟶ {unmasked}
· transition sources: `decide`, `lift_blind` 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)
ReviewDesk/invariants:
✓ invariant blind_roles >= 0 — writer 'assign_reviewer' proven by induction (writes (blind_roles.get(k) ?? 0) + 1)
✓ invariant blind_roles >= 0 && blind_roles <= 1 — writer 'submit_paper' proven (writes 1)
⚠ invariant blind_roles >= 0 && blind_roles <= 1 — runtime-checked (computed values): assign_reviewer → blind_roles [blind_roles <= 1] because `blind_roles` has no known range; `k` = "{paper}:{reviewer}" — not bounded
12 passed, 1 warnings, 0 failures
Temporal properties for 'blind':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK