A major chunk of storage reliability is all these weird and unexpected failure modes and edge cases which are not possible to prepare for, let alone write fixed specs for. Software correctness assumes the underlying system behaves correctly and stays fixed, which is not the case. You can't trust the hardware and the systems are too diverse - this is the worst case for formal verification.