PyCHC is a solver-agnostic framework for the design and certified solving of constrained Horn clause (CHC) systems.

PyCHC provides intuitive Python APIs to create and manipulate CHC systems programmatically and solve them using different backend solvers.

To increase the trustworthiness of the results, PyCHC offers a certification pipeline using independent SMT solvers and proof checkers, thereby combining the contributions presented in the papers  "Unsatisfiability Proofs for Horn Solving" and "Validation of CHC Satisfiability with ATHENA".

PyCHC can be found on the GitHub page https://github.com/usi-verification-and-security/pychc