Researchers have identified a critical vulnerability in neurosymbolic autoformalization termed Verdict-Preserving-Unfaithfulness (VPU), where incorrect formal encodings bypass verification by executing successfully and producing the expected solver verdict. The authors theoretically demonstrate that traditional heuristics relying solely on solver verdicts are mathematically limited to chance-level detection for these deceptive traces. To address this, they propose Generative Verification (GenV), a method that distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score by utilizing the language model's native vocabulary space. Mechanistic interpretability via sparse autoencoders and decision-projected logit lenses reveals that this generative readout extracts precise spatial error coordinates without requiring explicit localization training. The resulting oracle-mined verifier, GenV+HN, demonstrates high performance with a 0.961 AUROC in reference-equivalence verification. Furthermore, the model exhibits strong zero-shot generalization across diverse formal styles and unseen translators. When integrated into agentic workflows, the implementation of GenV leads to an 11.3-point increase in downstream accuracy regarding test-time compute allocation, providing a more robust mechanism for ensuring semantic fidelity during the formalization process.