Proving that a Turing machine decides a language in NP
In general, ZF does not prove that $T$ decides $L$, unless ZF is inconsistent. 

Take e.g. $L$ to be the language of words having even length (which is in P, hence in NP).

Consider the TM $T$ which on input $w$, crafts the first $|w|$ proofs in ZF. 
If any such proof proves a contradiction, accept.
Otherwise, accept if and only if $|w|$ is even.

We note that $T$ decides $L$ if and only if ZF is consistent. So, if ZF can prove that $T$ decides $L$, it is proving its own consistency, hence by Godel's second incompleteness theorem ZF is inconsistent.