Formally Verified Certification of Constraint Programming Proofs
This work presents a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics and develops FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models.