VERGE: Verifier Execution Regimes Break Greedy Equivalence in Speculative LLM Serving

Greedy speculative decoding is lossless only if packed target verification reproduces ordinary autoregressive (AR) target decisions on the same prefix. We trace violations of this systems contract from local verifier flips to real-drafter decision errors and finally to user-visible output. Controlled and real-drafter experiments independently reproduce about 0.34% strict reachable AR-packed disagreement, and the neural drafter encounters strict false accepts rather than merely an upper-bound risk. Free-running speculative output differs from AR on 53.55% of 592 prompts by token 128; 29.90% first diverge at positive AR margin, and every first divergence maps to a measured verifier event while prefixes are still identical. Forcing both paths to PyTorch MATH produces no detectable reduction in strict disagreement (MATH-AUTO = +0.012 percentage points, 95% CI [-0.077, +0.106] pp). Thus high-level backend switching is not a sufficient mechanism, and pinning a backend flag is insufficient to guarantee greedy equivalence.