2. A model checker most certainly provides 100% guarantees. This is why it's called a model-checker: it checks that a system's Kripke structure is a model[1] (i.e. a satisfying assignment) for a formula. It's just that model checkers often fail to check infinite state spaces and so people often check a finite instance of a specification. While model checkers have occasionally found errors in (informal but peer-reviewed) "proofs", I am not aware of any cases to the converse (obviously, when a finite instance was used for an infinite-state system). Both model checkers and deductive proofs have limitations and are generally complementary, but currently model checkers are considered to be much more scalable.
Also, model checkers don't "simulate a model some number of times." (the model-checking algorithm for temporal logic won the Turing award for its inventors). Even in finite state cases, model checkers check temporal formulas on infinite behaviors (e.g. that every request is eventually matched by a response).