Some model checkers like CBMC annotate C code directly. Others can generate piles of tests. But usually just knowing your requirements are consistent and exactly how the algorithm has to behave to work as intended goes a long way!