Refinement calculus is what it's formally referred to as. As pr0n has mentioned you start with a high-level, abstract model. You then create a second model that

Refinement calculus is what it's formally referred to as. As pr0n has mentioned you start with a high-level, abstract model. You then create a second model that implies every invariant of the first while adding more detail. You proceed like this to get closer to the implementation. If you are satisfied they are one and the same you can stop. However the goal isn't often to verify every single line of code. That would be prohibitively time consuming and expensive. The ideal use for this stuff is to verify the hard parts that are critical to get right. Verifying that a critical section of code will not lead to a deadlock or resource contention might be really important and so you could start with verifying that particular system.