Formal veriication tooling increasingly relies on logic solvers as automated reasoning engines. A commonality among these solvers is the high complexity of their codebases, which makes bug occurrence disturbingly frequent. Tool competitions have showcased many examples of state-of-the-art solvers disagreeing on the satisiability of logic formulas, be it solvers for Boolean satisiability (SAT), satisiability modulo theories (SMT), or constrained Horn clauses (CHC). The validation of solvers’ results is thus of paramount importance, in order to increase the conidence not only in the solvers themselves, but also in the tooling which they underpin. Among the formalisms commonly used by modern veriication tools, CHC is one that has seen, at the same time, extensive practical usage and very little eforts in result validation. We propose a two-layered validation approach for witnesses of CHC satisiability that validates CHC models via proof-backed SMT queries. We developed a modular evaluation framework, ATHENA, and assessed the approach’s viability via large scale experimentation, comparing three CHC solvers, ive SMT solvers, and ive proof checkers. Our results indicate that the approach is feasible, with potential to be incorporated into CHC-based tooling, and also conirm the need for validation, with fourteen bugs being found in the tools used.