  We describe a method for building composable and extensible verification
procedures within the Coq proof assistant. Unlike traditional methods that rely
on run-time generation and checking of proofs, we use verified-correct
procedures with Coq soundness proofs. Though they are internalized in Coq's
logic, our provers support sound extension by users with hints over new
domains, enabling automated reasoning about user-defined abstract predicates.
We maintain soundness by developing an architecture for modular packaging,
construction, and composition of hint databases, which had previously only been
implemented in Coq at the level of its dynamically typed, proof-generating
tactic language. Our provers also include rich handling of unification
variables, enabling integration with other tactic-based deduction steps within
Coq. We have implemented our techniques in MirrorShard, an open-source
framework for reflective verification. We demonstrate its applicability by
instantiating it to separation logic in order to reason about imperative
program verification.
