Unary in $P$, binary not in $P$

I would like to know if there is a known decision problem with the following characteristics:

• Represented in unary, the problem is decidable in polynomial time.

• Represented in binary, the problem is not decidable in polynomial time (and this fact has been proved, not just conjectured).

For example, Subset-Sum is in $P$ when represented in unary, but it is $NP$-complete in binary. However, this problem does not satisfy my second requirement because we do not know whether $P=NP$.

Every single-exponential (i.e. known to be solvable in $O(c^n)$ for some constant $c$) EXPTIME-complete problem will answer your requirements.

For example, see checking thorough rerefinement on finite modal transition systems.

StackExchange Computer Science Q#27587, answer score: 7