Describir: Generating and Exploiting Automated Reasoning Proof Certificates: Moving toward a full suite of proof-producing automated reasoning tools with SMT solvers that can produce full, independently checkable proofs for real-world problems.