Comment by throw-qqqqq

Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it.

I’d wager a million gazillion bucks that this is not the case.