In model-checking, you describe an abstracted version of your system and you can automatically check some properties. Your model has to be small enough (in term of number of states) to be processed by the tool, and the class of formulas you can express may be limited. Typically, you can check safety properties (such as assert statement in your code).
On the other hand, using a theorem prover (I think "proof assistant" is a better term, you can work on more accurate representations of your system and express any properties, but most proofs have to be done manually which requires time and expertise.
As for dependently typed language, I think most of them are not expressive enough to express complex properties such as "the system will eventually reach a consensus if no more than half of the process fail". And those that are are more akin to theorem provers.
In model-checking, you describe an abstracted version of your system and you can automatically check some properties. Your model has to be small enough (in term of number of states) to be processed by the tool, and the class of formulas you can express may be limited. Typically, you can check safety properties (such as assert statement in your code).
On the other hand, using a theorem prover (I think "proof assistant" is a better term, you can work on more accurate representations of your system and express any properties, but most proofs have to be done manually which requires time and expertise.
As for dependently typed language, I think most of them are not expressive enough to express complex properties such as "the system will eventually reach a consensus if no more than half of the process fail". And those that are are more akin to theorem provers.