Is the operator-state correspondence an axiom or a theorem? The operator-state correspondence – the statement that the states of a theory are in one-to-one correspondence with its (local) operators – always seemed like a working-principle to me, rather than a result one can derive. More precisely, I always had the impression we use it to define what we mean by the states of the theory. Especially since some theories don't have a predefined notion of Lagrangian/Hamiltonian, and therefore the "states" of the theory is a rather vague notion: what do we really mean by the states, if we don't have a Hamiltonian to diagonalise? The spectrum of operators seems to be a much more definite concept, and we define the states by acting with them on the vacuum (à la Verma). Is my understanding correct? Is the operator-state correspondence an axiom? Is it a definition? Or is it a theorem?
Note: I'm interested in the generic case here. Perhaps there is a particular toy-model where one can prove the correspondence, but that is not what I'm really looking for.
 A: It depends on your views, I guess. There is a derivation of operator-state correspondence from path integral, see, e.g., TASI lecture notes. This is good if you're fine with intuitive understanding of what states and local operators are.
There is a more axiomatic point of view. You are asking how do we know what is the Hilbert space of states in a QFT if we do not know what the Hamiltonian is. First of all, let's make the assumption that there is a unique vacuum state, which is invariant under all symmetries, call it $|0\rangle$. Then, since we are talking about a QFT, let's say that there is a real scalar field $\phi(x)$. We can then start forming new states by acting with it on the vacuum,
$$
\phi(x_1)|0\rangle,\quad \phi(x_1)\phi(x_2)|0\rangle,\quad\ldots
$$
An immediate problem is that these states are not normalizable, since say the norm of the first state is $\langle0|\phi(x)\phi(x)|0\rangle$, which is a two-pt function at coincident points, which is ill-defined. (Say in CFT you immediately know this is infinite. Also note I'm doing normal Lorenzian QFT here, not radial quantization.) 
To fix this problem, one considers states
$$
\int d^dx_1 f(x_1)\phi(x_1)|0\rangle,\quad \int d^dx_1 d^dx_2 f(x_1,x_2)\phi(x_1)\phi(x_2)|0\rangle,\quad\ldots
$$
where $f$ are Schwartz test functions. These states have finite norms (this is one of Wightman axioms, it can be explicitly verified, e.g., in CFT two- and three-point functions.) One then defines the vacuum "superselection sector" $\mathcal{H}_0$ to be the Hilbert space of states which can be created in this fashion (note that they are not all linearly independent; their inner products are computed by correlation functions). One can take this to be the Hilbert space of states if one is interested only in correlation functions of local operators. If there are non-local operators, then there may be other sectors, this highly depends on how you define your theory. 
In the above we used just $\phi$ and this will be a theory of a real scalar field, more generally you can use whatever local operators you have to create new states. However, it is important that you don't need all local operators to create all states, since you can act with one operators multiple times.
This defines the space of states. Definition of the space of local operators is a bit tricky. In particular, you need a notion of completeness for the set of local operators. I think the correct requirement is that your set contains those operators which you used to define the states (e.g. $\phi$ in the above example), and that it is closed under an asymptotic OPE expansion. With this definition, you can prove in CFT that this OPE expansions actually converge on the vacuum and thus all the states above can be reduced by the OPE to states created by a single local operator from your complete set. This allows you to prove operator-state correspondence from Wightman axioms+asymptotic OPE.
