Which Decisions Live in the Provable Layer? Formally Verified Safety Constraints for Agentic Clinical AI, with a Whole-Person Longitudinal Benchmark

Abstract

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.