Think of shadow functions as the specifications that you are building. Unlike proof assistants or Frama-C, you write specifications in C itself, and they work similarly to code. Often, the same contracts you write in these specifications can be shared by both the shadow functions and the real functions they shadow.

I take a bottom-up approach to model checking. I'll start by model checking the lowest level code, then I'll shadow this code to model check code that depends on it. In this way, I can increase the level of abstraction for model checking, focusing just on the side effects and contracts of functions I shadow, and move up the stack toward more and more general code.