Is it possible to determine if a reduction is correct?
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.