Is there a decidable problem which has a proof that it cannot be proved to have a particular deciding Turing machine?
Let us examine the following language:

$x\in L \iff ZFC \hspace{1mm} \text{is consistent}$.

Clearly, $L$ is decidable, and is decided by either the constant 1 or 0 machines.

Proofs from ZFC for the statements "$M_0$ decides $L$", "$M_1$ decides $L$" cannot exist  (if ZFC is consistent), since any of those would imply a proof from ZFC about its own consistency (see Godels's second incompleteness).

Note that i can however, provide a proof that the following machine $M$ decides $L$:

Given input $x$, check if there exists a proof for the consistency of ZFC, of length$\le |x|$. If such proof is found, return 0, otherwise return 1. 

If ZFC is consistent, the above machine outputs 1 for all $x$. If it isn't, we also have a proof that the above machine decides $L$ (An inconsistent system can prove any statement). The problem is that i cant prove whether or not $M$ computes the constant 1 function.