An equivalent definition of NP is that it consists of all problems that are decidable (not just verifiable) in polynomial time by a non-deterministic Turing machine. NTMs are known to be no more powerful than TMs in the sense that the set of problems decidable by NTMs is identical to the set of problems decidable by TMs, so clearly by this definition there can be no undecidable problems in NP.
To demonstrate that the two definitions of NP are equivalent, given the existence of a deterministic verifier you can demonstrate that a non-deterministic decider exists, and vice versa.
Say you have a deterministic polynomial verifier. Then there is also a machine that non-deterministically guesses a certificate of a length bounded by the polynomial corresponding to the certificate size bound of this problem/verifier and then runs the verifier. Since the alphabet is finite, the certificate for any given input is finite (and at most polynomial in the size of the input), and the verifier runs in polynomial time, the machine halts on all branches for all input and runs in (non-deterministic) polynomial time. Thus there is a non-deterministic decider for every deterministic verifier.
If you have a non-deterministic decider, then for every accepting computation you can write down the path of choices taken by the decider to reach the accept state. Since the decider runs in polynomial time, this path will be of at most polynomial length. And it's easy for a deterministic TM to validate that such a path is a valid path through an NTM to an accept state, so such paths form certificates for a polynomial time verifier for the problem. Thus there is a deterministic verifier for every non-deterministic decider.
Thus any undecidable problem cannot have a verifier that works on certificates of polynomial size (otherwise the existence of the verifier would imply the existence of a decider).
When you claim that a verifier exists for the halting problem, the certificate you're talking about is some encoding of (TM, I, N), where the TM halts on input I in N steps. This can indeed be verified in N steps, but the size of the certificate is not polynomial in the size of the (TM, I) input to the original problem (the halting problem); N can be arbitrarily large (regardless of encoding). If you try to convert such a verifier to a non-deterministic decider, you end up with a somewhat interesting machine. You should be able to prove that when run on (TM, I) for a TM that doesn't halt on input I no non-halting paths through the machine exist, but also that for any path leading to a halting state there is always another longer path (corresponding to a guess of a larger N), and thus there is no finite bound on its execution time. Essentially this is because there is an infinite space that needs to be explored by the initial non-deterministic guess. Converting such an NTM to a deterministic TM leads to one of those machines that neither loops nor halts on some input. In fact no NTM exists that can decide the halting problem, and so there is no verifier that works on certificates with a bounded size.
I'm not so familiar with Diophantine equations, but it looks like essentially the same problem applies to your argument there.
For this reason I find it easier to reason about the NTM definition of NP. There are verifiers for problems that are undecidable (just not ones that work on certificates that have a polynomial size bound in the size of the input to the original problem). In fact any TM that recognises but does not decide some language can be easily converted into a verifier for the same language.
If you do think about verifiers, I suppose you have to give their time bounds in terms of the size of the original problem input, not in terms of the certificate size; you can arbitrarily inflate the size of certificates so that the verifier runs in a lower time bound in terms of the size of the certificate.