Actually, formal verification could help massively with four of those problems — all but the first (UI/UX) and fifth (requirements will always be hard).

A change in the API of a dependency should be detected immediately and handled silently.

Reliance on unspecified behavior shouldn't happen in the first place; the client's verification would fail.

Detecting breakage caused by library changes should be where verification really shines; when you get the update, you try to re-run your verification, and if that fails, it tells you what the problem is.

As for interconnected systems, again, that's pretty much the whole point. Obviously, achieving this dream will require formalizing pretty much everything, which is well beyond our capabilities now. But eventually, with advances in AI, I think it will be possible. It will take something fundamentally better than today's LLMs, though.