In this paper, we present an Isabelle/HOL formalization of co-rewrite pairs for non-reachability in conditional rewriting. In particular, we formalize polynomial interpretations over negative integers as well as the weighted path order (WPO) and its variant co-WPO. All of these three co-rewrite pairs are also added to the verified certifier CeTA, which is now capable to check such non-reachability proofs. In combination with a prototype automatic tool we are able to synthesize certified non-reachability proofs on a database of 146 non-reachability problems, including 6 problems where other existing tools fail.