The marker every Lean runtime panic prints into captured build output.
Empirically pinned against real lake build transcripts (both panic
sites below produce it):
Panic message baked into every fuel wrapper’s exhaustion arm. This is a
SOUNDNESS marker, not just a diagnostic: Lean’s panic! does NOT abort
evaluation — it prints PANIC at … <this message> and returns the type’s
default value, so under native_decide an exhausted-fuel sample reduces
both sides of a model-vs-model equation to default and the kernel
certifies a vacuous (possibly FALSE) equality with lake still exiting 0.
aver proof --check therefore scans captured lake output for panic lines
(crate::codegen::lean::count_model_panic_lines) and treats any hit as
a hard check failure. The scan keys on Lean’s generic PANIC at line
marker — every prelude panic! site shares the vacuity vector, not just
this one — so this constant is purely the emission message; changing it
cannot blind the gate.