Forgive my ignorance, as I did read through everything you posted, but i'm not sure I fully understand how such a system avoids an attack of this form:

function check (bits) { sleep(bits) return false }

Where 'sleep' may be replaced by some appropriately long-running, arbitrary computation (since presumably these proof programs are not allowed to actually wait). Obviously for input data as complex as a sudoku answer the sleep would be near-infinitely long, but you could surely extract at least several bits of the answer in this way and thereby iteratively extract the whole thing, no?

Is there some mitigation for this that i'm missing?