This is very cool work but the author is labouring under a false premise about how axiomatic systems work:

> Every Lean proof assumes the runtime is correct.

No. Every valid Lean proof assumes that if the runtime/mathlib etc is correct, then it too is correct.

Tangentially also, most lean proofs are not dependent on whether or not the runtime has things like buffer overflows or denial of service against lean itself at all, because if I prove some result in Lean (without attacking the runtime) then a bug in the runtime doesn’t affect the validity of the result in general. It does mean however that it’s not ok to blindly trust a proof just because it only relies on standard axioms and has no “sorry”s. You also need to check that the proof doesn’t exploit lean itself.