Structural nested loops can be abstracted into polyhedral models, based on which one can perform aggressive loop optimizations; however, the optimizations are often heuristic and complex, and therefore error-prone. Meanwhile, verified compilers, though rigorously correct, still miss powerful optimizing transformations and therefore produce less efficient code than industrial ones. To bridge this gap, this work provides a general verified validation framework based on Bernstein's conditions for affine scheduling, the core component of polyhedral optimization techniques. It is parameterized over the concrete definitions and proofs of the instruction language to be reusable. As shown in our evaluation, the framework is flexible enough to support both existing verified compilers like CompCert and existing polyhedral compilers like Pluto. The result is fully mechanized in the Coq proof assistant.