Coq, specifically Gallina, is absolutely a specification tool. It's not only that, but it's one of the big use cases it's explicitly designed to support.
No, it’s not. Gallina is not a specification tool in the way TLA+ is (even if coq calls it its specification language). Gallina is a language used to write mathematical statements which you intend to prove. It’s not designed to write specifications.
Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really want to. It still remains an interactive prover.
Oh, if you define specification as something that should be done by people without a PhD, you might have a point.
I don't think software that needs specs should be done by people without a PhD. Jokes aside, I am not saying that Coq is an easy or simple specification tool. But of course it is a specification tool. Actually, it is one of the very few serious specification tools out there.
Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really want to. It still remains an interactive prover.