Unlike what UML is trying to simulate, which is an architectural blueprint, a UML model of a system cannot be verified for correctness. But a blueprint can be verified; You can tell "that proposed bridge" will hold "so much traffic and wind" by studying the blueprint.
Most code is verified for correctness by human eyeballs. I think many of us underestimate how important the 'diff' is with respect to incremental reasoning, which we do more often than not to keep the costs down. Once in a while we 'audit' the system, considering the model as a whole, but more often than not we are thinking in terms of deltas versus previous expectations.
Whoever actually solves the visual diff problem, I would be happy to see nominated for a Turing award. It's that big of a hill to climb.