soma.cell

Medication administration — the "five rights" enforced by barcode, no scan no dose Wrong-patient and wrong-drug medication errors are among the most common causes of inpatient harm

The defense that actually moved the numbers is Barcode Medication Administration (BCMA): the nurse scans their badge, the patient's wristband, and the drug — and the system confirms the five rights (right patient, drug, dose, route, time) BEFORE the dose is recorded as administered_done. Workarounds (charting without scanning) are exactly how the errors slip back in. Here an administration is a state machine that physically cannot reach `administered_done` without passing through `patient_verified` and `drug_verified`. A mismatch at either scan sends it to the TERMINAL `aborted` state — the dose is never administered_done and the attempt can't be silently retried into success. `soma verify` proves `administered_done` is unreachable from `aborted`.

A Soma program from the medical part of the verified corpus: 135 lines, cells BCMA, BCMATests. It passes soma check with soma 3.2.4.

How it is built

The cell BCMA declares 6 signals in its face: start(admin: String) -> Map, scan_patient(admin: String, scanned: String, ordered: String) -> Map, scan_drug(admin: String, scanned: String, ordered: String) -> Map, administer(admin: String) -> Map, admin_state(admin: String) -> String and demo() -> String. Its state machine administration starts in opened and allows 5 transitions: opened -> patient_verified, patient_verified -> drug_verified, drug_verified -> administered_done, opened -> aborted and patient_verified -> aborted. aborted and administered_done are terminal. Handlers: start (line 47), scan_patient (line 53), scan_drug (line 66), administer (line 82), admin_state (line 90) and demo (line 92).

The file also holds 1 test cell (BCMATests) with 15 assertions, run by soma test.

Generated from soma describe on this file.

The source

med_administration.cell

// ============================================================================
// MEDICATION ADMINISTRATION — the "five rights" enforced by barcode, no
// scan no dose
// ============================================================================
//
// Wrong-patient and wrong-drug medication errors are among the most common
// causes of inpatient harm. The defense that actually moved the numbers is
// Barcode Medication Administration (BCMA): the nurse scans their badge,
// the patient's wristband, and the drug — and the system confirms the five
// rights (right patient, drug, dose, route, time) BEFORE the dose is
// recorded as administered_done. Workarounds (charting without scanning) are exactly
// how the errors slip back in.
//
// Here an administration is a state machine that physically cannot reach
// `administered_done` without passing through `patient_verified` and `drug_verified`.
// A mismatch at either scan sends it to the TERMINAL `aborted` state — the
// dose is never administered_done and the attempt can't be silently retried into
// success. `soma verify` proves `administered_done` is unreachable from `aborted`.
//
//   soma verify examples/corpus/medical/med_administration.cell
//   soma test   examples/corpus/medical/med_administration.cell
//   soma run    examples/corpus/medical/med_administration.cell demo
// ============================================================================

cell BCMA {
    face {
        signal start(admin: String) -> Map
        signal scan_patient(admin: String, scanned: String, ordered: String) -> Map
        signal scan_drug(admin: String, scanned: String, ordered: String) -> Map
        signal administer(admin: String) -> Map
        signal admin_state(admin: String) -> String
        signal demo() -> String
    }

    // `administered_done` is reachable ONLY through both verifications. `aborted` is
    // TERMINAL — a mismatched scan ends the attempt for good. verify
    // proves there is no aborted -> administered_done path.
    state administration {
        initial: opened
        opened           -> patient_verified
        patient_verified -> drug_verified
        drug_verified    -> administered_done             // terminal: dose charted
        opened           -> aborted           // bad patient scan
        patient_verified -> aborted           // bad drug scan
    }

    on start(admin: String) {
        return map("ok", true, "state", get_status(admin))
    }

    // Right patient: the scanned wristband must match the order. A
    // mismatch aborts — terminally.
    on scan_patient(admin: String, scanned: String, ordered: String) {
        if scanned != ordered {
            transition(admin, "aborted")
            return map("ok", false, "reason",
                "WRONG PATIENT: scanned {scanned}, order for {ordered}",
                "state", get_status(admin))
        }
        let r = try { transition(admin, "patient_verified") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", get_status(admin))
    }

    // Right drug: scanned barcode must match the ordered drug.
    on scan_drug(admin: String, scanned: String, ordered: String) {
        let st = get_status(admin)
        if st != "patient_verified" {
            return map("ok", false, "reason", "scan patient first (state {st})")
        }
        if scanned != ordered {
            transition(admin, "aborted")
            return map("ok", false, "reason",
                "WRONG DRUG: scanned {scanned}, ordered {ordered}",
                "state", get_status(admin))
        }
        transition(admin, "drug_verified")
        return map("ok", true, "state", get_status(admin))
    }

    // Charting a dose as administered_done is possible ONLY from drug_verified.
    on administer(admin: String) {
        let r = try { transition(admin, "administered_done") }
        if r.error != () {
            return map("ok", false, "reason", "not verified — dose blocked: {r.error}")
        }
        return map("ok", true, "state", get_status(admin))
    }

    on admin_state(admin: String) { return get_status(admin) }

    on demo() {
        start("a1")
        scan_patient("a1", "band-123", "band-123")
        scan_drug("a1", "ndc-warfarin", "ndc-warfarin")
        let ok = administer("a1")

        // a wrong-patient scan: aborts, and the dose can never be administered_done
        start("a2")
        let bad = scan_patient("a2", "band-999", "band-123")
        let blocked = administer("a2")
        print("clean dose:   {ok}")
        print("wrong patient: {bad}")
        print("blocked dose:  {blocked}")
        return "demo done"
    }
}

cell test BCMATests {
    rules {
        // clean path: scan patient, scan drug, administer
        assert start("x").ok == true
        assert scan_patient("x", "b1", "b1").ok == true
        assert scan_drug("x", "d1", "d1").ok == true
        assert administer("x").ok == true
        assert admin_state("x") == "administered_done"

        // administered_done is terminal — no double-charting the same dose
        assert_fails transition("x", "drug_verified")

        // cannot administer without scanning — no scan, no dose
        assert start("y").ok == true
        assert_fails transition("y", "administered_done")
        assert administer("y").ok == false

        // wrong patient aborts terminally; the dose is unreachable
        assert start("z").ok == true
        assert scan_patient("z", "wrong", "right").ok == false
        assert admin_state("z") == "aborted"
        assert_fails transition("z", "patient_verified")
        assert_fails transition("z", "administered_done")
        assert administer("z").ok == false
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check med_administration.cell
✓ All checks passed.
$ soma test med_administration.cell
test BCMATests ...
  ✓ assert start("x").ok == true
  ✓ assert scan_patient("x", "b1", "b1").ok == true
  ✓ assert scan_drug("x", "d1", "d1").ok == true
  ✓ assert administer("x").ok == true
  ✓ assert admin_state("x") == "administered_done"
  ✓ assert_fails transition("x", "drug_verified") — raised invalid transition: administered_done → drug_verified. Current state: 'administered_done'. Valid targets: []
  ✓ assert start("y").ok == true
  ✓ assert_fails transition("y", "administered_done") — raised invalid transition: opened → administered_done. Current state: 'opened'. Valid targets: [patient_verified, aborted]
  ✓ assert administer("y").ok == false
  ✓ assert start("z").ok == true
  ✓ assert scan_patient("z", "wrong", "right").ok == false
  ✓ assert admin_state("z") == "aborted"
  ✓ assert_fails transition("z", "patient_verified") — raised invalid transition: aborted → patient_verified. Current state: 'aborted'. Valid targets: []
  ✓ assert_fails transition("z", "administered_done") — raised invalid transition: aborted → administered_done. Current state: 'aborted'. Valid targets: []
  ✓ assert administer("z").ok == false

15 tests: 15 passed, 0 failed
$ soma verify med_administration.cell
Verifying med_administration.cell...

State machine 'administration': 5 states, initial 'opened'
  States: [aborted, administered_done, drug_verified, opened, patient_verified]

  ✓ 5 states, 5 transitions
  ✓ all states reachable from 'opened'
  ✓ terminal states: [administered_done, aborted]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 5 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `scan_patient` ⟶ {aborted [if scanned != ordered], patient_verified}
  ✓ refinement: handler `scan_drug` ⟶ {patient_verified → aborted [if scanned != ordered], patient_verified → drug_verified}
  ✓ refinement: handler `administer` ⟶ {administered_done}
  · transition sources: `scan_patient`, `administer` 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)

10 passed, 0 warnings, 0 failures

  Temporal properties for 'administration':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK
$ soma run med_administration.cell demo
clean dose:   {"ok": true, "state": "administered_done"}
wrong patient: {"ok": false, "reason": "WRONG PATIENT: scanned band-999, order for band-123", "state": "aborted"}
blocked dose:  {"ok": false, "reason": "not verified — dose blocked: invalid transition: aborted → administered_done. Current state: 'aborted'. Valid targets: []"}
demo done

Builtins used

get_status, map, print, transition

Source file: /corpus/medical/med_administration.cell · examples/corpus/medical/med_administration.cell