Your proof of eval(box) relied on the fact that eval(box) can't be false and also provably true. But that fact is equivalent to consistency of the formal theory, so it can't be proven within the formal theory itself, by Godel's theorem. Of course, since eval(box) is a terminating computation that returns true (your proof of that is correct), the formal theory can eventually prove that by step-by-step simulation. But that proof will be much longer than your proof above, and much longer than n1. In fact, proves(box,n1) will return false, and your comment serves as a nice proof of that by reductio.

Don't get discouraged, it's a very common mistake =)