"Verifiable information": is this a known concept? The following seems to me like a natural definition and I wonder whether it's been studied somewhere

Consider $\mathsf{X} \subset 2^{\lbrace 0, 1 \rbrace^*}$ a set of languages. 
Then $K \subset \lbrace 0, 1 \rbrace^\omega$ is called "$\mathsf{X}$-verifiable information" when there is $L \in \mathsf{X}$ s.t.

(i) Given $x \in L$, every prefix of $x$ is in $L$

(ii) Given $f \in K$, every prefix of $f$ is in $L$

(iii) Given $f \notin K$, the length $n$ prefix of $f$ is outside $L$ for $n &gt;&gt; 0$

For example $\lbrace f \rbrace$ is $\mathsf{R}$-verifiable information iff $f$ is computable. This can be seen by constructing an algorithm which runs the verification on all strings of length $n$ and collects the prefixes of length $m$ of those strings which passed the verification. For $n &gt;&gt; m$, the only prefix which remains is the correct one

However if $K$ is $\mathsf{R}$-verifiable information it doesn't mean every $f \in K$ is computable: for example consider $K = \lbrace 0, 1 \rbrace^\omega$

A non-trivial example of $\lbrace f \rbrace$ which is $\mathsf{P}$-verifiable is as follows. Consider $L \in \mathsf{NP} \cap \mathsf{coNP}$ and let $f$ be an encoding of $L$ together with the corresponding $\mathsf{NP}$ and $\mathsf{coNP}$ witnesses (i.e. for each $x \in \lbrace 0, 1 \rbrace^*$, $f$ encodes either an $\mathsf{NP}$-witness proving $x \in L$ or a $\mathsf{coNP}$-witness proving $x \notin L$)
$K\subseteq\{0,1\}^\omega$ is $\mathsf{R}$-verifiable if and only if $K$ is a $\Pi^0_1$ class (in Cantor space), a concept that has been studied extensively in computability-theory. They are also called effectively closed sets.

A set $K$ is a $\Pi^0_1$ class iff it is the set of infinite paths through a recursive (computable) tree, and this is the version of the concept that you defined.

A monograph devoted to them:

Effectively Closed Sets (Douglas Cenzer and Jeffrey B. Remmel), Perspectives in Logic, Cambridge U. Press, 350 pages, to appear.