> Anything affected by the physical implementation of the computer still needs to be tested, for example. That includes corruption safety for databases I think

> Anything affected by the physical implementation of the computer still needs to be tested, for example. That includes corruption safety for databases I think that comes under "taken far enough". If you can model the corruption in your proof, you're good. I'm less confident about timings. But you're right that testing is still useful for bugs on other levels. After all, going high enough, humans can have buggy requirements, and no proof will catch that. Tests might.