The Recommendation Explained Itself. Did Anything Check the Explanation?

Compile-Time Intelligence, Part 7

Turning clinical guidelines into executable rules could make their thresholds, exceptions and qualifications easier to apply when a clinician needs them. A recommendation could arrive with the relevant guidance, the patient facts it used and an explanation of how the rule reached its answer.

That would be more useful than a bare recommendation. But the explanation creates a question of its own.

Suppose a system recommends starting a medication. Its explanation correctly reports the patient’s age, risk factors and estimated risk. Every supporting fact it mentions is true. Yet it never mentions an exclusion that changes the decision.

Checking everything an explanation says is different from checking everything the recommendation requires.

Oleg Mürk’s discussion of proof-carrying actions offers a useful starting point: an agent supplies a justification for a consequential action, and a separate monitor checks it, using formal proofs where feasible. His earlier essay on AI control explicitly keeps the specification and verification machinery among the things the system still has to trust. [1] [2]

Clinical decision support offers a more bounded setting in which to examine that idea. When a recommendation is supposed to follow a defined rule, the system can record the inputs and condition results, then check whether they establish the proposed outcome. The challenge is to make missing evidence visible as well as incorrect evidence.

Part 4 examined what must remain connected to a compiled rule. Part 5 asked what its checks enforce. Part 6 examined whether the specification captures the guideline’s meaning. [3] [4] [5]

Part 7 moves from approving the rule to checking each use of it: does this recommendation follow from that rule and the evidence about this patient?

The producer supplies the evidence. The receiver sets the requirements.

An older idea makes that division of responsibility concrete.

In proof-carrying code, a software producer supplies a program together with a mathematical proof that it obeys a specified safety policy. The receiving system checks the proof before accepting the code. George Necula described this approach in 1997, following earlier work with Peter Lee on safe operating-system extensions. [6] [7]

The producer does the difficult work of constructing the proof. A smaller checking component validates it. In Necula and Lee’s prototype, the proof validator was about five pages of C code. The aim was to keep the component that must be trusted much smaller than the software it examines. [7]

Crucially, the receiving system determines what must be proved. The producer cannot substitute an easier property and call the result safe. A proof that a program never crashes, for example, would not establish that it returns the correct answer. [6] [7]

A clinical recommendation could borrow that arrangement. Its producer supplies evidence, while an approved rule, reviewed and authorized for a defined clinical purpose, determines what the checker must establish.

The evidence need not be a formal proof. It could be a structured record of patient inputs and calculations that another program can recompute. The useful principle is the same: the party proposing the result does not get to decide which requirements count.

One patient, one omitted exclusion

Consider an illustrative pathway for initiating a statin, a cholesterol-lowering drug, to help prevent a first cardiovascular event.

The 2022 US Preventive Services Task Force recommendation supports prescribing a statin to adults aged 40 to 75 with at least one specified cardiovascular risk factor and an estimated ten-year cardiovascular risk of 10% or more. Its listed risk factors are dyslipidemia, diabetes, hypertension and smoking. Dyslipidemia means abnormal blood lipid levels. The recommendation has additional population and implementation qualifications, but no dialysis exclusion. [8]

KDIGO, the kidney-guideline organization, addresses dialysis separately. Its lipid guideline suggests not initiating statins in adults with chronic kidney disease requiring dialysis, while suggesting continuation when treatment was already in place before dialysis began. [9]

Combining those sources requires an explicit clinical interpretation. For this software example, suppose a clinical team has approved a simplified pathway in which dialysis prevents a positive initiation recommendation. This is an illustrative combination, not a complete prescribing protocol or an absolute prohibition on treatment.

Within the example’s assumed scope, a positive recommendation requires all five conditions: age 40 to 75, at least one listed risk factor, estimated ten-year risk of at least 10%, no dialysis dependence, and no current statin treatment. The last condition keeps the task focused on starting treatment.

Now consider a hypothetical 63-year-old patient with hypertension and dyslipidemia, a recorded risk estimate of 12.4%, and no current statin. The record also documents hemodialysis three times a week. For this comparison, assume these inputs have been confirmed as current.

Four conditions support initiation. The dialysis exclusion changes the pathway’s answer.

My colleague Chen Li used an omitted dialysis exclusion in the fictional example in When the Checker Becomes the Reward. A generated program could receive full credit because its tests never included the patient who would expose the omission. [10] Here, the question moves to an individual recommendation: would its accompanying evidence reveal the mistake?

Keep the evidence that produced the recommendation

A useful justification would connect three parts of the decision.

The rule: its identifier and approved version, linked to the source passages and the interpretation recorded during review. The checker retrieves the rule authorized for this task instead of accepting whatever rule the producer supplies.

The patient evidence: the values used, their sources and dates, and whether each fact is established, uncertain or not documented. A blank field is not evidence that a condition is absent.

The evaluation: the conditions applied, the results of evaluating them, and the proposed recommendation. This is an execution trace, a record of the steps taken when the rule ran.

Chen’s What Has to Survive Extraction From a Clinical Note explains why the evidence needs more than a value. A claim should retain whether it was affirmed or negated, its certainty, when it applied, whom it concerns, its information source and supporting text. [11]

The proposal is to preserve this information during evaluation, rather than ask a model to invent a plausible explanation afterward. The result gives another component something concrete to check.

But what should that checker do when the producer leaves a condition out?

Two checkers, two different questions

Consider two checkers evaluating the same three submissions. Both can compare supplied facts with the confirmed patient inputs and recompute the condition results they examine.

Checker A checks the submitted argument. It verifies the facts and conditions listed in the justification, then checks whether the proposed output agrees with those listed results. It does not check whether the list is complete.

Checker B checks the approved rule’s requirements. It retrieves the required conditions from the authorized rule. For a positive initiation recommendation in this example, it needs evidence establishing all five. A missing condition remains unresolved.

The middle row is the important one. All the supporting facts it reports are true. The recommendation is nevertheless inconsistent with the approved rule.

Checker A is deliberately a weaker check, not a sound proof verifier for that rule. It establishes consistency with a selected subset of conditions. Checker B catches the omission because it knows what the proposed outcome requires.

This is the explanation-level counterpart of weakening a specification by dropping a requirement. [12] The justification cannot be allowed to define its own standard of completeness.

Completeness does not always require evaluating every branch. A confirmed exclusion might settle the result immediately. The obligation is to provide the evidence the approved decision procedure requires for the particular outcome.

The surrounding system also has to enforce the check. The result must be tied to the same patient, rule version, evidence snapshot and recommendation that will be displayed. An unchecked revision cannot inherit an earlier approval. Missing evidence should produce a visible request for clarification or review, not silently become a positive or negative clinical answer.

Independence means more than a second opinion

Checker B works in the example because the rule and patient inputs have already been established. That assumption identifies the next problem: where do those inputs come from?

Some checks are mechanical. A program can confirm a rule version, compare values with designated records, apply explicit recency requirements and recalculate the outcome.

Other checks involve interpretation. Finding the words “hemodialysis three times a week” proves that a passage contains those words. It does not establish that they describe the patient rather than a relative, remain current, or are uncontradicted elsewhere. Likewise, no medication entry is not automatically confirmation that the patient takes no statin.

The patient-evidence layer may therefore require extraction models, conflict-handling rules or clinical review. The rule checker can then verify how accepted inputs were used. Correct calculation does not remove uncertainty in the underlying evidence.

This is why two components can agree without providing independent assurance. No collusion is necessary if both rely on the same incomplete summary. Giving a reviewer a different name, prompt or model does not by itself give it the missing fact.

In the proposed arrangement, the checker obtains its obligations from the approved rule and its evidence through defined sources it can inspect, not only through the producer’s narrative. Those sources, the rule and the checker remain part of what must be trusted and evaluated.

Approval is not infallibility. If the approved rule itself omits dialysis, complete execution of that rule will not discover the omission. That returns us to Part 6’s question about the specification. This article addresses the next link: whether a particular recommendation follows it.

A “valid” answer still needs a defined scope

The same distinction appears in systems that check answers against written policies.

Amazon Bedrock Guardrails’ Automated Reasoning checks turn written policies into formal rules, then check whether claims translated into logic follow from those rules and supplied facts. AWS explicitly states that a VALID finding does not validate untranslated claims or content outside the formal policy’s scope. Checking what follows from assumed facts does not establish that those facts are true. [13]

The associated research, by Chenyang An, Sam Bayless and colleagues including Byron Cook, Ferhat Erata and Aman Goel, explores making several translations and checking their agreement in meaning. In one conservative configuration, 169 approvals were correct and 10 incorrect. It recognized only 169 of the 1,131 valid cases in that evaluation. [14]

That tradeoff matters. A checker needs evaluation on both what it accepts and what it leaves unresolved. In healthcare, excessive rejection can also create review burdens or delays; rejection needs a defined destination, not just a reassuring label.

Beyond Solver Verdicts, by Vikash Singh, Debargha Ganguly and colleagues including Aman Goel, Ali Torkamani and Ferhat Erata, examines a related limit. A solver answers a formal logical question, such as whether a set of constraints can all hold. Two different translations can receive the same verdict while imposing different constraints. On the paper’s matched examples, reading that identical verdict alone cannot distinguish the translations. [15]

The connection to our example is about information, not identical architecture. A checker cannot detect a distinction through a result that contains no information about it. Checking the recommendation requires access to the relevant conditions and evidence, not merely agreement with an earlier pass.

Make explanations easier to check, then audit what passes

Could another model simply read the explanation and judge whether it is convincing?

Research by Miles Turpin, Julian Michael, Ethan Perez and Samuel Bowman shows why that is insufficient. In their experiments, chain-of-thought explanations, the written reasoning accompanying an answer, could rationalize answers influenced by irrelevant cues without acknowledging those cues. Plausible reasoning was not necessarily a faithful account of what influenced the model. [16]

For a compiled rule, the goal can be more concrete than reconstructing a model’s internal reasoning: establish that the displayed recommendation follows from the approved conditions and supported inputs. A readable explanation can be generated from the checked record rather than treated as the evidence itself.

Models may also learn to make their answers easier to examine. Prover-verifier games pair a prover that supplies an answer and supporting reasoning with a verifier that judges it. Cem Anil, Guodong Zhang, Yuhuai Wu and Roger Grosse introduced a learning framework built around those roles. [17]

Jan Hendrik Kirchner and colleagues studied a related approach on grade-school mathematics, training helpful provers to produce correct solutions verifiers could recognize and adversarial provers to expose weaknesses. Training for checkability also improved time-constrained human evaluation of the helpful solutions. These are empirical results on the studied tasks, not formal guarantees of safety. [18]

This creates a useful possibility: train systems to supply evidence that helps a checker do its job. It also recreates the concern in Chen’s reward-loop article: getting better at satisfying a checker is not automatically getting better at the intended task. [10]

An evaluation could therefore include justifications with accurate supporting claims but deliberately omitted conditions. It could test false claims, stale facts and contradictions separately. A clinical audit could examine accepted recommendations against the relevant guideline and patient record, rather than review only the submitted explanation. Unresolved and rejected cases also need inspection for missed recommendations and delays.

Show what passed, not just a green tick

For the illustrative patient, the system could show:

This pathway does not recommend statin initiation. The dialysis exclusion applies. Current dialysis is documented in the patient evidence. View the evidence, the approved rule and the source passages supporting this condition.

When dialysis status is unknown, the message should be different:

This pathway cannot establish an initiation recommendation. Dialysis status is unresolved. Additional information or clinical review is needed.

The first reports a rule outcome supported by evidence. The second reports that a required basis for a positive recommendation is missing. Neither is a complete treatment decision.

That inspectability has a regulatory counterpart. FDA’s January 2026 guidance discusses enabling clinicians to independently review the basis for recommendations, including inputs, relevant knowns and unknowns, and how the logic applies to the patient. Such review is one of several conditions relevant to whether certain clinical decision-support functions fall outside the medical-device definition. A checked record could support review; it does not establish a product’s classification or clinical safety. [19]

HL7’s CDS Hooks standard provides a way to display decision support inside an electronic health record as cards. Cards require a source and can include detail and links, which could expose this evidence. Those presentation fields do not themselves verify it. [20]

The scope must remain visible. In Seven Ways Clinical AI Fails, and the Control Each Requires, Chen describes an accurate answer about ibuprofen that misses a potentially urgent symptom in the patient’s question. Correct drug information does not make the overall response adequate. [21]

Likewise, a complete justification for a statin pathway is not a complete assessment of the patient. Other clinical concerns still require other controls and judgment.

The opportunity is a recommendation whose basis can be examined

The useful shift is from asking an AI to explain itself to asking what evidence would establish the proposed result.

The producer supplies that evidence. The approved rule sets the requirements. The checker evaluates the connection. Unresolved questions remain visible, and the clinical reviewer can inspect both what passed and what was outside the check.

This does not eliminate trust. It makes the places where trust is required more explicit, while creating a route for machines to take on more of the routine checking.

A convincing explanation tells a story about the answer. A checked justification shows which requirements the answer has actually satisfied.

Part 8 turns to rules that unfold over time, where individually checked decisions can still miss a problem in the sequence of care.

Sources

1. Mürk O. LLM-Based Firewalls and Proof-Carrying Actions. X, October 30, 2026. Proposal for independently checked justifications, including formal proofs where feasible.
2. Mürk O. Alignment Is Dead (for now), Long Live Control! X, September 17, 2026. Explicitly retains the specification and verification stack within the trusted base.
3. Bressler D. The Guideline Compiled Cleanly. Where Did the Interpretation Go? Eventum AI, October 22, 2026. Part 4.
4. Bressler D. The Output Matched the Schema. What Did the Schema Guarantee? Eventum AI, October 27, 2026. Part 5.
5. Bressler D. The Proof Checked. Does the Spec Say What the Guideline Says? Eventum AI, October 28, 2026. Part 6.
6. Necula GC. Proof-Carrying Code. POPL 1997, 106-119.
7. Necula GC, Lee P. Safe Kernel Extensions Without Run-Time Checking. OSDI 1996. The proof-validation section describes the approximately five-page prototype validator. This is not a size estimate for a clinical checker.
8. US Preventive Services Task Force. Statin Use for the Primary Prevention of Cardiovascular Disease in Adults: Preventive Medication. 2022. JAMA 328(8), 746-753. The example is not the complete recommendation and does not validate a cardiovascular-risk estimator for dialysis patients. Population restrictions and patient preferences remain relevant to actual care.
9. KDIGO Lipid Work Group. Clinical Practice Guideline for Lipid Management in Chronic Kidney Disease. 2013. Recommendations 2.3.1 and 2.3.2 distinguish initiation from continuation. See also the guideline group’s 2014 summary, p. 1306. The initiation recommendation is a suggestion, not an absolute prohibition.
10. Li C. When the Checker Becomes the Reward. Eventum AI, October 20, 2026. Its statin rule is fictional and differs from this article’s illustrative pathway.
11. Li C. What Has to Survive Extraction From a Clinical Note. Eventum AI, October 21, 2026.
12. Mürk O. Commentary on specifications and generated patches. X, October 23, 2026. Discusses removing functionality to satisfy a specification.
13. Amazon Web Services. Automated Reasoning checks and concepts. Scope of validation, untranslated material and application-level handling of findings.
14. An C, Bayless S, Buliani S, Cassel D, Cook B, et al. A Neurosymbolic Approach to Natural Language Formalization and Verification. Version 2, July 13, 2026, Table 1. The cited three-of-three configuration used 563 instances evaluated three times: 169 true approvals, 10 false approvals, 548 true rejections and 962 false rejections. Approval precision is 94.4%; recall is 14.9%. The reported 99.4% soundness measure subtracts incorrect approvals divided by all 1,689 decisions from one. These are experimental results, not universal production guarantees.
15. Singh V, Ganguly D, Goel A, Torkamani A, Han X, Lilien J, Erata F, Chaudhary V. Beyond Solver Verdicts: Generative Reward Models for Autoformalization. Version 2, September 11, 2026. The indistinguishability result concerns verdict-only scoring on matched pairs; the learned target is equivalence to a designated formal reference.
16. Turpin M, Michael J, Perez E, Bowman SR. Language Models Don’t Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting. NeurIPS 2023.
17. Anil C, Zhang G, Wu Y, Grosse R. Learning to Give Checkable Answers with Prover-Verifier Games. 2021.
18. Kirchner JH, Chen Y, Edwards H, Leike J, McAleese N, Burda Y. Prover-Verifier Games Improve Legibility of LLM Outputs. 2024. Evaluation on grade-school mathematics, including time-constrained human assessment.
19. US Food and Drug Administration. Clinical Decision Support Software. Guidance issued January 29, 2026, especially criterion 4, pp. 14-15. No product-classification conclusion is drawn here.
20. HL7 International. CDS Hooks, version 2.0.1. Card source, detail and link attributes.
21. Li C. Seven Ways Clinical AI Fails, and the Control Each Requires. Eventum AI, October 22, 2026.