The question came to my mind while studying the NP definition. Do we know any such languages?
For any instance of a problem, take the instance itself as the certificate. Linear size, verifiable in polynomial time for problems in P, not known for problems in NP.
Every NEXPTIME complete language has a certificate of length 0 that can be checked in time $2^{2^{n^{O(1)}}}$, but does not have polynomial length certificate that can be checked in polynomial time.