Bagahk is a verified decision procedure which tests the boolean validity of a formula modulo background theories implemented in the Coq proof assistant. The algorithm has been shown sound and complete, proving that it will recognize always and only recognize valid formulas. These proofs have been formalized in Coq and accompany the source code. Currently, bagahk handles the background theory of ground equations, a subset of the theory of equality with unterpreted function symbols, but work continues on extending this to the full theory. A full description of the bagahk project can be found here.