Is it possible to prove that a problem $P$ is decidable in $O(\phi)$ without providing an algorithm that decides $P$ in $O(\phi)$? Phrased another way: Are there any problems that are known to be decidable in a better worst-case time complexity than the best known procedure?
 A: Easy answer:

Decide the set of numbers $n$ such that every even number between $4$ and $n$ is the sum of two primes.

This is known to be decidable in $O(1)$ time, because either Goldbach's conjecture is true and the program that always outputs "yes" will work, or the conjecture fails, in which case the program only needs to compare its input to a constant.
However, we don't know which algorithm decides this problem in $O(1)$ time, and if Goldbach's conjecture is true but unprovable (which looks fairly likely at this point), it will be forever unknown which algorithm to use.
Does this feel like cheating? One objection is that the set to decide is either $\mathbb N$ or $\{1,2,3,\ldots,n\}$ for some $n$, and all of those have known, or at least easily constructible, constant-time algorithms. However, that just shows that what we can prove about a problem doesn't depend only on the Platonic identity of the problem as a subset of $\mathbb N$ but rather on the particular description of the problem we need to prove things from. So I don't think you are going to make that objection.
A more serious objection is that we might want to reinterpret the question such that "decidable in $O(f(n))$ time" means that there is some algorithm that provably decides the problem, and happens to finish within $O(f(n))$ time each time we run it -- even though this bound may not itself be provable. We may even, without loss of generality, be so liberal as to accept a non-constructive proof that the algorithm exists, if only it also proves that if we ever find the algorithm, we would be able to prove that it decides the right problem.
Not-so-easy, but surprising, answer: Even with this reinterpretation, the answer is still that if you can prove (however non-constructively) that a particular problem is decidable within some particular asymptotic bound (in the above sense), then I can give you an algorithm that decides it within that asymptotic bound. In fact, I can give you an concrete algorithm right now that will run within any asymptotic upper bound you can prove for the problem, ever.
This is based on Levin's universal search theorem, and goes roughly like this:


*

*Enumerate all programs that provably decide the problem at hand. This can be done by enumerating all possible strings of symbols, in order of increasing length, and checking for each one whether it happens to be a valid proof (say, in ZFC or PA according to which kind of provability you want) that some program decides the problem.

*Simulate all of the found programs on the given input in parallel, time-sharing between them such that the search form more programs uses $\frac 12$ of the total time used, and the $i$th found program gets $\frac 1{2^{i+2}}$ of the total time we spend.

*Once any of the simulated programs halts, stop everything and halt with that answer.


Now, if you prove that there is an algorithm that decides the problem in $g(n) = O(f(n))$ time, then that algorithm, even if you don't know which it is, must have some index $i$ in the enumeration. Then the running time of the parallel search algorithm can be at most the sum of (a) the time it takes for the program-enumeration to reach index $i$ (which is independent of $n$ and therefore just a constant term, asymptotically), and (b) $g(n)$, times $2^{i+2}$ (because the simulation only gets a fraction of the total time we use), times the slowdown factor inherent in simulating the found program instead of running it directly. In a reasonable cost model, this slowdown can be shown to be at most a constant factor.
Thus, the running time of the search algorithm is at most a constant term plus a constant times $g(n)$, which is $O(f(n))$ because $g(n)$ is. And that is a worst-case estimate because it assumes that algorithm $i$ in the enumeration is the first to stop, but it might possibly be another algorithm that wins the race, in which case the search algorithm can run strictly faster than $O(f(n))$.
And the best thing is you can go right ahead and write this program now. You'll need: a proof checker (more or less an off-the-shelf component); a linear-slowdown interpreter for a general-purpose programming language (very off-the-shelf, but watch out for patents); a formal semantics for the interpreted language (here you'll need a literature search, or possibly to hire a CS graduate student); and a formal statement of the problem you want to solve (likely the hardest part).
The worst thing is, of course, that the constant factors that the big-O notation hides will be truly, mind-bogglingly gargantuan. It's not a practically feasible algorithm for anything -- in fact do not expect any test run to finish before the heat death of the universe. But mathematically speaking it's going to work impeccably!
