Clinical artificial-intelligence systems are starting to act across a course of care, not to answer one question at a time. Their safety is checked by methods that sample the input space: a test suite tries some inputs, a language-model reviewer reads some cases, a physician panel audits some cases. A sampling check can pass a safety rule and still miss the rare input that breaks it, such as a documented obligation dropped several encounters later. This study measures that gap and releases CIV-Bench, a public benchmark of 832 clinical rule sets with safety properties across eight whole-person domains, in single-encounter and longitudinal forms, plus a computational stress tier, each with independently established ground truth. We compare formal verification, which uses a satisfiability-modulo-theories (SMT) solver to check every possible input at once, against the methods used in practice: random unit testing, language-model judges, and a blinded physician panel. Formal verification detected all 612 violations, raised no false alarm, and returned no unsound verdict; for each item it returned either a proof that the rule holds over every input or one concrete input that breaks it. A frontier language-model judge matched this detection, but it returned a pass rate over sampled cases rather than a guarantee, at three orders of magnitude more compute per item. The general open-weights judge returned unsound verdicts on the computational stress tier; the medically fine-tuned judge was unsound far more widely, collapsing on the longitudinal properties despite strong single-encounter medical detection, so medical fine-tuning did not close the gap. Unit testing and the physician panel missed the deep, cross-encounter violations that hold a course of care together. Formal verification is set apart not by a higher detection rate but by the kind of evidence it returns: a proof over the whole input space, a replayable counterexample, or an explicit statement that it cannot decide. The guarantee holds for the decisions placed in this layer, and it depends on the safety rule being specified correctly.
Studies of artificial intelligence tools used in patient triage have largely involved academic medical center cohorts, scripted patient-actor scenarios, or knowledge benchmarks. Populations that may rely on such tools due to constrained access to in-person care, including Medicaid patients, have been less fully evaluated.
To compare combinations of safety guardrails added to artificial intelligence tools for triage of patient-initiated text messages in a multi-state Medicaid population.
Retrospective evaluation of 2000 messages from Medicaid patients across three U.S. states (Virginia, Washington, Ohio) during January 2023 through November 2025. Three physicians independently adjudicated each message under blinded review; disagreements were resolved by majority and a senior-physician arbiter. Tools included a deployed decision support system with a Conservative Q-Learning controller, supervised baselines (XGBoost+sentence-BERT, logistic regression, rule-based guardrails), and frontier large language models (Claude Opus 4.7, GPT-5.5, Gemini 3.1 Pro, each with and without retrieval-augmented generation). Combinations spanned single tools, ensembles, cascades, multi-model consensus rules, and four-component guardrail compositions identified by a structured literature review. Thresholds and Platt calibration were fit on a held-out validation split and frozen before the test pass. Two pre-specified targets: an autonomous (physician-unassisted) triage benchmark of sensitivity and specificity both 0.80 or higher; and a sensitivity-floor target of 0.80 to 0.95 with clinician review of flagged messages.
Real-world messages had lower reading level (grade 4.6 versus 5.8) and more colloquialisms (59.1% versus 19.5%) than physician-scripted scenarios. Hazard prevalence on blinded physician review was 8.2% (165 of 2000). Two configurations met the sensitivity-floor target: a high-recall first-stage screen (sensitivity 0.855; 12.0 missed hazards and 729 alerts per 1,000 messages) and a disagreement-stratified clinician-review workflow (sensitivity 0.939; 5.0 missed hazards and 878 alerts per 1,000 messages). No configuration met the autonomous benchmark; sensitivity and specificity reached 0.594 and 0.592 for the best balanced single tool, 0.685 and 0.575 for the best balanced ensemble, and 0.297 and 0.874 for the highest-specificity cascade.
No evaluated tool or combination was sufficiently accurate to enable physician-unassisted triage in this setting. Two configurations met the pre-specified sensitivity-floor target under clinician review of flagged messages, following the classical clinical-screening pattern.
Sanjay Basu, Sadiq Y. Patel, Parth Sheth et al.· BMC Medical Informatics and...· 0 citations