isFormulaStringB is PolyTimeDecidable

The formula-string check $V(x,w) = \mathtt{isFormulaStringB}(x)$ is polynomial-time decidable.

isFormulaStringB x tests whether the binary string $x$ is a valid encoding of a CNF formula by decoding $x$ into a formula $\varphi$ and re-encoding it, then comparing the result with $x$. Both decoding and encoding traverse the input once, so the entire check runs in time $O(|x|^2)$ (quadratic due to the list equality comparison).

A multi-tape Turing machine implementing this check uses one tape for the input $x$, additional work tapes for the intermediate encoding, and writes the verdict on the output tape. Since the check depends only on $x$ (the certificate $w$ is ignored), the machine runs in at most $c(|x|+|w|+1)^d$ steps for suitable constants $c, d$.