We report on the formalisation and correctness proof of a model checker for the modal &mgr;-calculus in Coq's constructive type theory. Using Coq's extraction mechanism we obtain an executable Caml program, which is added as a safe decision procedure to the system. We thereby avoid the generation of large proof objects while preserving the high reliability of the proof environment. An example illustrates the combination of model checking with deductive techniques.