Using the definition from Sipser of a verifier as a machine that always halts (e.g. accepts or rejects a given input), I believe the language $\overline{E_{TM}}$ (e.g. the language consisting of strings of the form $<M>$ describing turing machines which have non-empty languages) has a verifier.
My claim - we can always provide an accepting computation history of a given machine M on some arbitrary input as a witness that proves the language of that machine is not empty. Going through this computation history (which would be a finite length input) and using the description of the turing machine ($<M>$) to guarantee its correctness and completeness is straight forward. Is this correct or am I missing something big? No claims are being made yet about the actual complexity of doing this, only on whether it is verifiable.
I believe that simply providing the machine description $<M>$ and some input $w$ we claim to be in the language recognized by M is not sufficient, since if M loops indefinitely on that input w our verifier will never halt.
