Is there a tool that can check whether m |= p holds, where m and p are both ltl formula
Yes, you can use an LTL-to-Büchi-automaton translator for this.
Let's assume that you want to check if $\psi \rightarrow \psi'$ is a valid LTL formula, i.e., every word satisfying the LTL property $\psi$ also satisfies the LTL property $\psi'$. This case is equivalent to finding out if $\psi \wedge \neg \psi'$ is satisfiable. Your $\psi \models \psi'$ notation is another way of writing this, but I would avoid it since the $\models$ relation is often defined differently in current research papers on the topic.
If we translate $\psi \wedge \neg \psi'$ to a Büchi automaton, we can easily check if its language is empty. In fact, optimizing LTL-to-Büchi translators remove states with an empty language, and hence you only need to check if the resulting automaton has no accepting state.
On example LTL-to-Büchi translator is ltl3ba. For instance, if you want to check if $\mathsf{F G }\,a$ implies $\mathsf{G F}\,a$, you can do that as follows:
./ltl3ba -f &quot;(F G a) &amp;&amp; !(G F a)&quot;

Here, &quot;-f&quot; stands for &quot;translate this formula that is given as a parameter&quot;.
The result is given in SPIN never claim form:
never {    /* (F G a) &amp;&amp; !(G F a) */
T0_init:
    false;
}

There is no state ending with &quot;_accept&quot; in the name, which means in the SPIN never claim notation that there is no accepting state. So $(\mathsf{F G }\,a) \wedge \neg (\mathsf{G F}\,a)$ is not satisfiable.
There is also at least one LTL-to-Büchi translator with a web interface, namely the one from the SPOT framework.