There is nothing preventing modeling the contextual environment within static analysis. Static analysis/type systems help the programmer draw the line between the known and the unknown. Some conditions are just not practical or efficient to check for. However for the context you use it within you can make certain guarantees about the code. This is still incredibly useful even though it doesn't guarantee an error can never take place.

You say it "is" leaky in the presence of memory corruption. However that is not necessarily true. One could model software memory verification within a type system. Meaning, you could guarantee at compile time that each time a variable is read it is verified via checksum against its last written value. This would not be particularly efficient, but the point stands that type systems can be used (and should be used) to model hardware failures.

This is no different than network link failures, etc...