As the title says, can Coq be used as a model checker? Can I mix model checking with Coq proving? Is this usual? Google talks about a "µ-calculus", does anyone have experience with this or something similar? Is it advised to use Coq in this way, or should I look for another tool?
A proof assistant like Coq will verify that your proof is sound and that any theorems you propose can (or cannot) be derived using axioms and previously proven results. It will also provide you with support in proposing proof steps to reduce the effort you have to make to discharging the proofs.
A model checker, in contrast, symbolically enumerates the state space of the specification and determines whether any of the verification conditions are violated. In such a case, it will provide an error trace showing what sequence of state changes will trigger the violation.
These usually have very different back-end processing requirements but, while they could be combined into a single tool, the Coq prover does not appear to have done so.
The Temporal Logic of Actions (TLA+) specification language, along with the companion TLA+ Proof System (TLAPS) was developed by Leslie Lamport to reason about large formal specifications. It has been extended with the PlusCal algorithmic language that supports model checking of the algorithms that are translated into a TLA+ representation.
The µ-calculus is a notation used as a low-level underpinning for many formal methods approaches. You should also look at the Boolean satisfiability problem for a more brute force approach. Theorem provers are generally more sophisticated in their design and use traditional expert system/AI concepts along with libraries of proof rules defined by experts to provide the support required to discharge the proof obligations.
As an another example of a proof tool, you can look at the Event-B method and the accompanying Rodin development platform. This will, when refining a specification more concretely identify the proof obligations and attempt to mechanically discharge these, leaving the difficult ones for you to do.
For model checking you could look at:
among the freely available choices.