"if A()=a and runtime(A)<N then U()=u" can only be proved by an agent that represents runtime() explicitly, which means it would probably find (relatively short) general proofs of the form (max proof length)<L => runtime < some function of L,
and
agent proves X => length of proof of X < max proof length.

Although, now that I think of it more, this does not help, as in this setting the agent may easily prove X but not "agent proves X"... You're right, the proof of the second statement is not obviously short.