> You can prove it doesn't crash, it doesn't leak memory, it doesn't break authorization invariants, etc.

You can but nobody does. It's enough if it doesn't usually do these things.