Is it possible to determine if a reduction is correct? Suppose we have an arbitrary term, x, in Lambda Calculus, or in an equivalent turing-complete system. Suppose we ask an oracle what is the normal form of that term, and it answers y. Is it possible to determine, in finite time, if the oracle answer's ir correct?

Secondary question: is there any system (non-turing complete, perhaps) where that would be possible?
I don't know what your "oracle" is, but without further information what you are asking is whether the following language is decidable:

$L:=\{ (t,u)\in\Lambda\times\Lambda \mathrel{|} t \rightarrow^* u, u \textrm{ normal}\}$

(with $\Lambda$ being the set of $\lambda$-terms). This is obviously not the case: for every Turing machine $M$, there is a $\lambda$-term $t_M$ (effectively computable from the description of $M$) such that $t_M$ reduces to a fixed normal form $u$ if $M$ terminates on the empty string and has no normal form otherwise; therefore, if $L$ were decidable, we would be able to decide the halting problem for $M$ on empty input by asking whether $(t_M,u)\in L$.

If your "oracle" gives more information, then of course the situation may very well be different.  For instance, if the oracle also gives an upper bound to the number of reduction steps needed to reach the purported normal form, then it is obviously decidable whether the oracle's answer is correct.

If you are actually asking about proof-carrying code (like D.W. suggests), please modify your question accordingly and I'll be happy to modify/remove my answer.