Specifications that are formally verified can definitely cover real-time guarantees, behaviour under error returns from operations like allocation, and similar things. Hardware failures can be accounted for in hardware verification, which is much like software verification: specification + hardware design = verified design; if the spec covers it, the verification guarantees it.

Considering software alone isn't pretty useless, nor is having the guarantee that "inc x = x - 1" will always go from an Int to an Int, even if it's not "fully right" at least trying to increment a string or a complex number will be rejected at compile time. Giving up on any improvements in the correctness of code because it doesn't get you all the way to 100% correct is, IMO, defeatist.

(Giving up on it because it has diminishing returns and isn't worth the effort is reasonable, of course!)

How would that look like if you accidentally assumed you have arbitrary large integers but in practice you have 64 bits?

    Add(x,y):
       Assert( x >= 0 && y>= 0 )
        z = x + y
        Assert( z >= x && z >= y )
        return z

That’s impractical. Take binary search and the assumption the list is sorted. Verifying the list is sorted would negate the point of binary search as you would be inspecting every item in the list.