Let $A$ be a set of decision algorithms which are running in polynomial time and which takes natural numbers as inputs.
$x\in A$ if and only if
for $i\in N$
$x(i)=0$ or $x(i)=1$
and running time of $x(i)$ is smaller than $n^k$ ($n$ is digit of $i$)
Now consider a $\mathcal{NP}$ problem for the set $A$.
Problem: "For given $x\in A$, is there any $i\in N$, such that $x(i)=0$?"
For this $\mathcal{NP}$ problem, there is a decider of non-deterministic Turing machine $M$
$$ M(x) = \left\{ \begin{array}{ll} 1\text{ if there exists i∈ N, such that x(i)=0 }\\ 0\text{ otherwise} \end{array} \right. $$
And for this NDTM, there is a verifier of polynomial Deterministic Turing Machine $V$,
$$ V(x,i) = \left\{ \begin{array}{ll} 1\text{ if x(i)=0 }\\ 0\text{ otherwise} \end{array} \right. $$
Question : By the Cook-Levin theorem, I think something can be transformed into a Boolean formula. What is transformed into a Boolean formula?
$M$? $M(x)$? $V$? $V(x)$? $x$? or the NP problem itself?
The usual version of the Cook-Levin theorem provides a transformation from the decider $M$, but the truth value of the variables is (partially) set by the input $x$. That is, there are variables of the form $S_{i,\rho}$ which are true if the $i$th symbol on the input tape is $\rho$ (so you have about $n\times|\Sigma|$ of these, where $n$ is the length of encoding of the input and $\Sigma$ is the input alphabet).
It would not be too hard to imagine that there would be an alternate proof that usese $V$ instead of $M$. Indeed, Levin's proof mapped from search problems, rather than decisions problems anyway. The key part in any such proof though is that we need to be able to map any problem in $\mathcal{NP}$ to SAT. Thus we need to use some universal property of all problems in $\mathcal{NP}$, such as that they all have a NDTM that decides them, or a DTM that verifies them.