  We present a proof system for establishing the correctness of results
produced by optimization algorithms, with a focus on mixed-integer programming
(MIP). Our system generalizes the seminal work of Bogaerts, Gocht, McCreesh,
and Nordstr\"om (2022) for binary programs to handle any additional
difficulties arising from unbounded and continuous variables, and covers a
broad range of solving techniques, including symmetry handling, cutting planes,
and presolving reductions. Consistency across all decisions that affect the
feasible region is achieved by a pair of transitive relations on the set of
solutions, which relies on the newly introduced notion of consistent branching
trees. Combined with a series of machine-verifiable derivation rules, the
resulting framework offers practical solutions to enhance the trust in integer
programming as a methodology for applications where reliability and correctness
are key.

Optimization and Control