Verified Checker for Mixed-Integer Programming Certificates

To establish trust in mixed-integer programming (MIP), modern solvers such as SCIP can emit VIPR certificates for infeasibility and objective-range results. These certificates make solver results independently checkable and capture the proof steps produced by a practical, general-purpose MIP solver. However, the VIPR reference checker is an unverified C++ program, so an implementation error could cause it to accept an invalid certificate. We present LeanVIPR, a VIPR checker implemented and formally verified in Lean 4. We formalize the semantics and soundness of the VIPR proof system — including linear combination, integer rounding, assumptions, and branch closure — and prove that LeanVIPR is sound and terminating. Consequently, acceptance establishes either that the original MIP is infeasible, or that the listed solutions are feasible and the reported objective range is valid. To improve checking performance for infeasibility certificates, we also support sound backward slicing: acceptance of a sliced certificate establishes infeasibility of the original MIP.