data Negative control 1: replacing a real proof body with an incomplete proof in an otherwise-passing artifact caused failure by two independent mechanisms, the compiler flag (exit code 1, 'declaration uses sorry') and the probe (reporting the offending declaration and the incomplete-proof axiom). Negative control 2: a theorem proved by compiled-evaluator reflection was correctly reported as depending on a non-kernel axiom, demonstrating the trusted-base claim can also fail. A passing check that cannot fail is worse than no check.