Constant PROOF_FUEL_EXHAUSTED_MSG 

pub const PROOF_FUEL_EXHAUSTED_MSG: &str = "Aver proof fuel exhausted";

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.