For the practical evaluation of quantified Boolean formulas (QBFs) an additional preprocessing step is beneficial in many cases. The application of a preprocessor, however, prevented the extraction of proofs for the original formula. Such proofs are required to independently validate correctness of the preprocessor?s rewritings and the solver?s result. To address this issue, we introduced the QRAT proof system. With QRAT it is possible to capture all state-of-the-art preprocessing techniques in a uniform manner and to check the result of a preprocessor efficiently.