Since others have described the high-level difference between checking and proving, I will point out that you might not want to use a dependently typed language even if you plan on doing some proving.
A large cost of formal verification is designing and implementing specifications. For this reason, even if you plan on proofs for some components, it still makes sense to use a tool which supports both model checking and theorem proving using a single specification. Especially if your interests are non-academic.
Type-theoretic proof assistants typically don't support model checking (or, it's at least fair to say it's not in the culture even where supported). So to use model checking, you have to re-implement the specification.
A large cost of formal verification is designing and implementing specifications. For this reason, even if you plan on proofs for some components, it still makes sense to use a tool which supports both model checking and theorem proving using a single specification. Especially if your interests are non-academic.
Type-theoretic proof assistants typically don't support model checking (or, it's at least fair to say it's not in the culture even where supported). So to use model checking, you have to re-implement the specification.