Customs clearance — no release without an examination verdict
The 2019 Philadelphia seizure of 17.5 tonnes of cocaine aboard the MSC Gayane worked because the containers were HELD at the port until CBP finished examining them. The failure mode customs agencies fear is the opposite: a "port runner" — cargo that leaves the terminal while its entry is still under review, or after a seizure order. Once goods are on a truck, the border has already failed. This lifecycle makes the run impossible in the record system: `released` is reachable ONLY from `cleared`, an exam hold must return a verdict before anything moves, and `seized` is TERMINAL — a seizure order can never be walked back to circulation. soma verify proves all three.
A Soma program from the logistics part of the verified corpus: 112 lines, cells Customs, NoPortRunners. It passes soma check with soma 3.2.4.
How it is built
The cell Customs declares 6 signals in its face: file_entry(entry: String, duty_cents: Int) -> Map, flag_for_exam(entry: String) -> Map, exam_verdict(entry: String, verdict: String) -> Map, clear_entry(entry: String) -> Map, release_cargo(entry: String) -> Map and entry_status(entry: String) -> String; keeps 1 memory slot: duty (Map<String, Int>, persistent and consistent) under the invariant duty >= 0. Its state machine entry_flow starts in filed and allows 6 transitions: filed -> under_review, under_review -> cleared, under_review -> exam_hold, exam_hold -> cleared, exam_hold -> seized and cleared -> released. released and seized are terminal. Handlers: file_entry (line 45), flag_for_exam (line 53), exam_verdict (line 59), clear_entry (line 68), release_cargo (line 74) and entry_status (line 80).
The file also holds 1 test cell (NoPortRunners) with 16 assertions, run by soma test.
The source
customs_clearance.cell
// ============================================================================
// CUSTOMS CLEARANCE — no release without an examination verdict
// ============================================================================
//
// The 2019 Philadelphia seizure of 17.5 tonnes of cocaine aboard the MSC
// Gayane worked because the containers were HELD at the port until CBP
// finished examining them. The failure mode customs agencies fear is the
// opposite: a "port runner" — cargo that leaves the terminal while its
// entry is still under review, or after a seizure order. Once goods are
// on a truck, the border has already failed.
//
// This lifecycle makes the run impossible in the record system: `released`
// is reachable ONLY from `cleared`, an exam hold must return a verdict
// before anything moves, and `seized` is TERMINAL — a seizure order can
// never be walked back to circulation. soma verify proves all three.
// ============================================================================
cell Customs {
face {
signal file_entry(entry: String, duty_cents: Int) -> Map
signal flag_for_exam(entry: String) -> Map
signal exam_verdict(entry: String, verdict: String) -> Map
signal clear_entry(entry: String) -> Map
signal release_cargo(entry: String) -> Map
signal entry_status(entry: String) -> String
}
memory {
// assessed duty per entry, in cents — never negative
duty: Map<String, Int> [persistent, consistent]
invariant duty >= 0
}
// released and seized are terminal: gone is gone, seized is seized.
state entry_flow {
initial: filed
filed -> under_review
under_review -> cleared
under_review -> exam_hold
exam_hold -> cleared
exam_hold -> seized
cleared -> released
}
on file_entry(entry: String, duty_cents: Int) {
let w = try { duty.set(entry, duty_cents) }
if w.error != () { return map("ok", false, "reason", "duty cannot be negative") }
let r = try { transition(entry, "under_review") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "entry", entry, "duty_cents", duty_cents)
}
on flag_for_exam(entry: String) {
let r = try { transition(entry, "exam_hold") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "exam_hold")
}
on exam_verdict(entry: String, verdict: String) {
if verdict != "cleared" && verdict != "seized" {
return map("ok", false, "reason", "verdict must be cleared or seized")
}
let r = try { transition(entry, verdict) }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", verdict)
}
on clear_entry(entry: String) {
let r = try { transition(entry, "cleared") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "state", "cleared")
}
on release_cargo(entry: String) {
let r = try { transition(entry, "released") }
if r.error != () { return map("ok", false, "reason", "not cleared: {r.error}") }
return map("ok", true, "state", "released")
}
on entry_status(entry: String) { return get_status(entry) }
}
cell test NoPortRunners {
rules {
// THE PORT RUN: release straight from review. No such edge.
assert file_entry("E-100", 250000).ok == true
assert release_cargo("E-100").ok == false
assert_fails transition("E-100", "released")
// a clean entry clears, then releases
assert clear_entry("E-100").ok == true
assert release_cargo("E-100").ok == true
assert entry_status("E-100") == "released"
// the Gayane: flagged, examined, SEIZED — terminal forever
assert file_entry("E-666", 90000).ok == true
assert flag_for_exam("E-666").ok == true
assert exam_verdict("E-666", "seized").ok == true
assert_fails transition("E-666", "cleared")
assert_fails transition("E-666", "released")
assert entry_status("E-666") == "seized"
// an exam hold cannot be released without a verdict
assert file_entry("E-7", 100).ok == true
assert flag_for_exam("E-7").ok == true
assert_fails transition("E-7", "released")
// negative duty assessments are refused by the memory
assert_fails duty.set("E-7", -500)
}
}What the toolchain says
$ soma check customs_clearance.cell
✓ All checks passed.$ soma test customs_clearance.cell
test NoPortRunners ...
✓ assert file_entry("E-100", 250000).ok == true
✓ assert release_cargo("E-100").ok == false
✓ assert_fails transition("E-100", "released") — raised invalid transition: under_review → released. Current state: 'under_review'. Valid targets: [cleared, exam_hold]
✓ assert clear_entry("E-100").ok == true
✓ assert release_cargo("E-100").ok == true
✓ assert entry_status("E-100") == "released"
✓ assert file_entry("E-666", 90000).ok == true
✓ assert flag_for_exam("E-666").ok == true
✓ assert exam_verdict("E-666", "seized").ok == true
✓ assert_fails transition("E-666", "cleared") — raised invalid transition: seized → cleared. Current state: 'seized'. Valid targets: []
✓ assert_fails transition("E-666", "released") — raised invalid transition: seized → released. Current state: 'seized'. Valid targets: []
✓ assert entry_status("E-666") == "seized"
✓ assert file_entry("E-7", 100).ok == true
✓ assert flag_for_exam("E-7").ok == true
✓ assert_fails transition("E-7", "released") — raised invalid transition: exam_hold → released. Current state: 'exam_hold'. Valid targets: [cleared, seized]
✓ assert_fails duty.set("E-7", -500) — raised memory invariant violated on 'duty': duty >= 0 — rejected write of -500 (key "E-7"); the slot is unchanged
16 tests: 16 passed, 0 failed$ soma verify customs_clearance.cell
Verifying customs_clearance.cell...
State machine 'entry_flow': 6 states, initial 'filed'
States: [cleared, exam_hold, filed, released, seized, under_review]
✓ 6 states, 6 transitions
✓ all states reachable from 'filed'
✓ terminal states: [seized, released]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
⚠ dynamic transition targets: handler `exam_verdict` 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 `exam_verdict` 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 `file_entry` ⟶ {under_review}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `flag_for_exam` ⟶ {exam_hold}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `exam_verdict` ⟶ <dynamic>
✓ refinement (partial — dynamic targets fall back to runtime check): handler `clear_entry` ⟶ {cleared}
✓ refinement (partial — dynamic targets fall back to runtime check): handler `release_cargo` ⟶ {released}
· transition sources: `file_entry`, `flag_for_exam`, `clear_entry`, `release_cargo` 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)
Customs/invariants:
⚠ invariant duty >= 0 — runtime-checked (computed values): file_entry → duty because `duty_cents` is a parameter (narrow it: `require duty_cents >= 0 else …`)
11 passed, 3 warnings, 0 failures
Temporal properties for 'entry_flow':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK