Deciding the set of all Turing machines that halt in at most $k|x|$ steps $\forall x \in \Sigma^*$ Let $L = \{ &lt;M&gt; | M$ halts on every input $x$ in at most $200 * |x|$ steps $\}$. 

Is $L$ decidable? Recognizable?

Given that membership in $L$ asserts something about $M$'s behavior on an infinite set of strings, it seems extremely unlikely to me that $L$ could be either. I have shown that co-$L$ is Turing-recognizable (I think): you can make an enumerator that tests each $M_1, M_2, \dots, $ for each $s_1, s_2, \dots$ and emits $M$ if it does not accept some $s$ in at most $200|x|$ steps.

Since co-$L$ is recognizable, either $L$ is not recognizable, or it is decidable. I can't imagine that $L$ is decidable. However, it definitely cannot be reduced to the halting problem, nor can Rice's theorem be applied to it (since the quality in question is the quality of halting in a particular number of steps, being able to decide it doesn't let us decide other arbitrary properties).

It seems to me that the best way to go will be to show that $L$ lets me recognize something that is unrecognizable, since the only problems it solves are ones which require me to run over infinite sets of strings. But I can't think of what this could be. I thought that maybe co-HALT would work, but I can't ever prove that a TM will never halt on some input.

I'm stuck. What direction should I go in?
The language is actually decidable, but the proof is quite involved, and uses crossing-sequence arguments. See this paper for details.

If you change $200|x|$ to a faster growing function, such as $|x|\log |x|$ (plus some constant), then the language becomes undecidable by standard reduction arguments.