What Autoformalize-and-Verify Buys: Certified Error is a Property of the Verifier, not the Generator

Autoformalize-and-verify pipelines promise machine-checkable guarantees on LLM outputs, but are typically demonstrated on small curated sets and rarely measured against the guarantee they actually deliver. We evaluate one at scale. A frozen Qwen2.5-7B-Instruct generator answers math word problems while independent translator models formalize the same problems into SMT-LIB — question only, never the candidate answer. Z3 certifies an answer only when enough translators' encodings entail it; otherwise the system abstains. Conformal risk control wraps the verified channel in a distribution-free bound on the certified-wrong rate. Across six datasets spanning a 61–99% generator accuracy range, the certified-error rate is flat: it is a property of the verification layer, not of the generator. At a three-translator agreement threshold the system certifies 34.5% of problems with zero certified errors across 72 gated templates, bound 4.08%. Replacing a 76.1% generator with a 97.7% one moves coverage by 1.4 points. We report all pre-registered outcomes, including two falsified predictions — among them cross-family decorrelation, the mechanism this design is usually assumed to rely on. The certified-error floor is real, but it does not come from where the design predicted.