String constraints are crucial in many SMT-based applications, yet solvers that rely on automata-based reasoning, such as OSTRICH, currently lack support for producing independently checkable proofs. This work addresses this limitation by formalizing the core rules of the Regular Constraint Propagation calculus in the Alethe proof format. Furthermore, the Carcara proof checker is extended with verification procedures for these rules, supported by a dedicated automata module. Together, these contributions enable reliable checking of OSTRICH proofs and strengthen the certification infrastructure for automated reasoning with string constraints.