When the Specification Is the Risk: Applying Formal Verification to Clinical Decision Rules

Medicine has begun turning treatment guidelines into machine-checkable code. A guideline, however, mixes two kinds of sentence. One kind is a per-patient obligation, decidable by a program from the fields of a single case. The other is a population claim about survival or risk, which a proof can only assume. Both can appear as formal declarations, but a passing build alone does not reveal which are checked and which are assumed. “Verified” then means far less than it sounds. In compiler engineering the specification is the more trusted side; in medicine—as with AI-generated specifications—the specification itself is the risk. We propose making the unit of a clinical verification claim a single declaration, not a build. Each claim must report its axiom footprint: every assumption used by its proof, directly or through other results. It must also prove what its executable checker actually decides, a binding between checker and rule. A versioned envelope records the pair together with the risks left uncovered. Because the footprint belongs to the declaration itself, a scoped claim stays meaningful even inside broken surroundings. We apply this to our own working, hand-written Lean 4 oncology guideline library, which passes every ordinary signal. It compiles, contains no sorry, and its tests pass. Of its 32 rules, 29 are provably false one at a time, most from a single misplaced quantifier. An intended “the treatment given to this patient must be a tyrosine kinase inhibitor (TKI)” was written as “every treatment is a TKI”. Meanwhile 21 of its 25 checkers decide exactly the per-patient form of their own rule, and one accepts what its rule forbids, invisible to its tests. We also implemented and tested the pipeline end to end on synthetic cases. Nothing here establishes clinical correctness.