You take hardware properties as axioms (for instance, ARMv6 cache coherency is specified in detail as part of the lengthy spec, even though you have no guarantees that the hardware actually is faithful to the spec)

You can certainly verify the soundness of what is within your control, the compiler code, which is what is being suggested above.

You can formally verify that the algorithm has the desired properties, though. If the hardware requires additional properties for soundness, then that would only be an error in the properties, not in the proof. (Of course, that would no longer prove soundness on that hardware.)