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.