Lab chain of custody — a sample whose custody broke can never be reported, by construction A forensic toxicology or pathology result is only as trustworthy as the unbroken chain of custody behind it
If a sample is left unsealed, or its identity can't be accounted for at any handoff, the result is inadmissible and clinically worthless — but the dangerous version is the lab that reports it anyway, and a treatment (or a conviction) rests on a possibly-swapped tube. Here a specimen walks collected → sealed → in_transit → received → analyzed → reported. The one terminal failure state is `compromised`: any custody break sends the sample there and it can NEVER reach `reported`. `soma verify` proves reported is unreachable from compromised, and that compromised is itself terminal — no "re-seal and pretend" path exists.
A Soma program from the medical part of the verified corpus: 125 lines, cells ChainOfCustody, CustodyTests. It passes soma check with soma 3.2.4.
How it is built
The cell ChainOfCustody declares 6 signals in its face: collect(sample: String) -> Map, handoff(sample: String, step: String) -> Map, breach(sample: String) -> Map, report(sample: String) -> Map, sample_state(sample: String) -> String and demo() -> String. Its state machine specimen starts in collected and allows 10 transitions: collected -> sealed, sealed -> in_transit, in_transit -> received, received -> analyzed, analyzed -> reported, collected -> compromised, sealed -> compromised, in_transit -> compromised, received -> compromised and analyzed -> compromised. compromised and reported are terminal. Handlers: collect (line 53), handoff (line 59), breach (line 67), report (line 75), sample_state (line 83) and demo (line 87).
The file also holds 1 test cell (CustodyTests) with 16 assertions, run by soma test.
The source
chain_of_custody.cell
// ============================================================================
// LAB CHAIN OF CUSTODY — a sample whose custody broke can never be
// reported, by construction
// ============================================================================
//
// A forensic toxicology or pathology result is only as trustworthy as the
// unbroken chain of custody behind it. If a sample is left unsealed, or
// its identity can't be accounted for at any handoff, the result is
// inadmissible and clinically worthless — but the dangerous version is the
// lab that reports it anyway, and a treatment (or a conviction) rests on a
// possibly-swapped tube.
//
// Here a specimen walks collected → sealed → in_transit → received →
// analyzed → reported. The one terminal failure state is `compromised`:
// any custody break sends the sample there and it can NEVER reach
// `reported`. `soma verify` proves reported is unreachable from
// compromised, and that compromised is itself terminal — no "re-seal and
// pretend" path exists.
//
// soma verify examples/corpus/medical/chain_of_custody.cell
// soma test examples/corpus/medical/chain_of_custody.cell
// soma run examples/corpus/medical/chain_of_custody.cell demo
// ============================================================================
cell ChainOfCustody {
face {
signal collect(sample: String) -> Map
signal handoff(sample: String, step: String) -> Map
signal breach(sample: String) -> Map
signal report(sample: String) -> Map
signal sample_state(sample: String) -> String
signal demo() -> String
}
// `reportable` order: collected -> sealed -> in_transit -> received ->
// analyzed -> reported. `compromised` is the TERMINAL trap: every
// custody-bearing state can fall into it, none escape. verify proves
// reported is unreachable once compromised.
state specimen {
initial: collected
collected -> sealed
sealed -> in_transit
in_transit -> received
received -> analyzed
analyzed -> reported
collected -> compromised
sealed -> compromised
in_transit -> compromised
received -> compromised
analyzed -> compromised
}
on collect(sample: String) {
return map("ok", true, "state", get_status(sample))
}
// A legitimate handoff is the next step in the chain; the machine
// rejects skipping a step (e.g. shipping an unsealed tube).
on handoff(sample: String, step: String) {
let r = try { transition(sample, step) }
if r.error != () {
return map("ok", false, "reason", "custody violation: {r.error}")
}
return map("ok", true, "state", get_status(sample))
}
on breach(sample: String) {
let r = try { transition(sample, "compromised") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", get_status(sample))
}
// Reporting is only reachable through an unbroken chain. A compromised
// sample cannot transition to reported — the proof, not a policy memo.
on report(sample: String) {
let r = try { transition(sample, "reported") }
if r.error != () {
return map("ok", false, "reason", "cannot report: {r.error}")
}
return map("ok", true, "state", get_status(sample))
}
on sample_state(sample: String) {
return get_status(sample)
}
on demo() {
collect("tube-A")
handoff("tube-A", "sealed")
handoff("tube-A", "in_transit")
breach("tube-A") // seal found broken at the dock
let r = report("tube-A") // REFUSED — chain is broken
let st = sample_state("tube-A")
print("after breach: report = {r}")
print("final state: {st}")
return "demo done"
}
}
cell test CustodyTests {
rules {
// an unbroken chain reaches reported
assert collect("s1").ok == true
assert handoff("s1", "sealed").ok == true
assert handoff("s1", "in_transit").ok == true
assert handoff("s1", "received").ok == true
assert handoff("s1", "analyzed").ok == true
assert report("s1").ok == true
assert sample_state("s1") == "reported"
// you cannot skip sealing — shipping a raw tube is rejected
assert collect("s2").ok == true
assert_fails transition("s2", "in_transit")
// a breach is terminal and blocks reporting forever
assert collect("s3").ok == true
assert handoff("s3", "sealed").ok == true
assert breach("s3").ok == true
assert sample_state("s3") == "compromised"
assert_fails transition("s3", "reported")
assert_fails transition("s3", "sealed")
assert report("s3").ok == false
}
}What the toolchain says
$ soma check chain_of_custody.cell
✓ All checks passed.$ soma test chain_of_custody.cell
test CustodyTests ...
✓ assert collect("s1").ok == true
✓ assert handoff("s1", "sealed").ok == true
✓ assert handoff("s1", "in_transit").ok == true
✓ assert handoff("s1", "received").ok == true
✓ assert handoff("s1", "analyzed").ok == true
✓ assert report("s1").ok == true
✓ assert sample_state("s1") == "reported"
✓ assert collect("s2").ok == true
✓ assert_fails transition("s2", "in_transit") — raised invalid transition: collected → in_transit. Current state: 'collected'. Valid targets: [sealed, compromised]
✓ assert collect("s3").ok == true
✓ assert handoff("s3", "sealed").ok == true
✓ assert breach("s3").ok == true
✓ assert sample_state("s3") == "compromised"
✓ assert_fails transition("s3", "reported") — raised invalid transition: compromised → reported. Current state: 'compromised'. Valid targets: []
✓ assert_fails transition("s3", "sealed") — raised invalid transition: compromised → sealed. Current state: 'compromised'. Valid targets: []
✓ assert report("s3").ok == false
16 tests: 16 passed, 0 failed$ soma verify chain_of_custody.cell
Verifying chain_of_custody.cell...
State machine 'specimen': 7 states, initial 'collected'
States: [analyzed, collected, compromised, in_transit, received, reported, sealed]
✓ 7 states, 10 transitions
✓ all states reachable from 'collected'
✓ terminal states: [reported, compromised]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
⚠ dynamic transition targets: handler `handoff` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
✓ termination: all 6 handlers structurally terminate
⚠ refinement (partial — dynamic targets fall back to runtime check): handler `handoff` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
✓ refinement (partial — dynamic targets fall back to runtime check): handler `handoff` ⟶ <dynamic>
✓ refinement (partial — dynamic targets fall back to runtime check): handler `breach` ⟶ {compromised}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `report` ⟶ {reported}
· transition sources: `breach`, `report` 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)
9 passed, 2 warnings, 0 failures
Temporal properties for 'specimen':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK$ soma run chain_of_custody.cell demo
after breach: report = {"ok": false, "reason": "cannot report: invalid transition: compromised → reported. Current state: 'compromised'. Valid targets: []"}
final state: compromised
demo done