Problems that are decidable but cannot be verified in polynomial time While working on a somewhat unrelated project for Suresh I recently came across some work done by Page and Opper about User-Composable systems and a portion of their work briefly discussed problems that cannot be verified in polynomial time.  I have been unable to find much information about other problems that cannot be verified in polynomial time or an analysis of a such a problem.  I was wondering if any of you knew of any such problems and/or how to analyze them.

As stated in the comments a better way to phrase this question is:
What problems are decidable but outside of NP?
The most important thing to realize from a theoretical standpoint is that NP is actually a relatively small class of all decidable languages. That said, many of the interesting problems in computer science lie within NP so they get a lot of attention. 

It's conjectured that $NP \subsetneq PH \subsetneq PSPACE \subsetneq EXP \subsetneq NEXP$.

The classes PH, PSPACE, and EXP contain many of the "interesting" problems in $R \setminus NP$, which is what I assume you're asking about in this question. So far NEXP has gotten all of the attention because $NP \subsetneq NEXP$ is the only proper containment that we can prove (by the nondeterministic time hierarchy theorem, as I mentioned above).

Here are some interesting concrete examples of problems in some of these other classes:


Determining if a player has a winning strategy in chess or Go (adapted to n x n boards) is EXP-complete.
MAJ-SAT, the problem of determining whether over half of the assignments to the variables in a boolean formula satisfy that formula, is in PSPACE. It is also complete for the smaller class PP.
EXACT-CLIQUE, the problem of determining whether the largest clique in a graph is of size exactly k, is in $\Sigma_2^P$, part of the second level of the polynomial hierarchy.