How to challenge Hutter's algorithm?
But $M_{\mathsf{F},p^*}$ will take double exponential time in the length of $x$ to arrive at that conclusion, if I'm not mistaken.


That $M_{\mathsf{F},p^*}$ will take double exponential time is a conjecture at best. Too see that this conjecture is pretty strong, take any formula $\phi$ that is formally independent of $\mathsf F$, and ask whether a short proof of $\phi$ can be found in $\mathsf F$. Any algorithm that can answer this question quickly (with "no") can also answer the same question for $\phi=\bot$ quickly (with "no"), because any formula can be derived in a single step from $\bot$.


  Now I wonder whether there are more interesting ways to make $M_{\mathsf{F},p^*}$ look bad, perhaps similar in spirit to Rice's theorem?


Formal systems are not just bad at proving their own consistency, they are also famously bad at proving some sequence to be random. So we could ask whether a given finite sequence can be reproduced by some program shorter than $m$ symbols taking fewer than $n$ steps. The restriction to fewer than $n$ steps allows us to implement $p^*$ as a brute force search. If the sequence and $m$ are kept fixed and binary encoding is used for $n$, the resulting problem seems to be in $EXP$. Maybe it's better not to fix the sequence and $m$, because then the problem seems to be in $NEXP$.

What about a function $p^*$ based on Rice's theorem? No progress yet...