Model checkers typically only explore a bounded number of states which is efficient at bug finding and often doesn't require additional annotations in the program.

Automatic (SMT-based) verifiers like Verus, Dafny, F* (and my VCC :) require you to annotate most every function and loop but give you broad guarantees about the correctness of the program.

Tools based on interactive provers (like Coq or Lean) typically require more guidance from the user but can guarantee even more complex properties.