I prefer to "visualize" my code as manipulating a set of logical assertions that characterize the state of the computation, ultimately reaching the point where the state of the computation's properties satisfy the requirements. Somewhat like that explained in [Gries1987] and [Dijkstra1976]. Visual tools are just too coarse to capture the details necessary to ensure correctness or real-life requirements.
While UML diagrams sometimes help to make sense of a complex set of OO Class relationships, this is far from how I normally work with the meaning of code in my head while programming.
Programs absolutely can be proven to be correct. Lousy programs are hard to prove. To do it even reasonably well, you have to evolve the program and proof hand-in-hand.
You can't automate the proof because of the halting problem. You can, however, manually prove the post-conditions and preconditions of any arbitrary statement, or sequence of statements.
You must read Dijsktra's A Discipline of Programming.
Then, you must read Gries' The Science of Programming.
Then you'll know how to prove programs correct.