Recorded 14 February 2023. Haniel Barbosa of Universidade Federal de Minas Gerais in Belo Horizonte presents "Better SMT proofs for certifying compliance and correctness" at IPAM's Machine Assisted Proofs Workshop. Abstract: SMT solvers can be hard to trust, since it generally means assuming their large and complex codebases do not contain bugs leading to wrong results. Machine-checkable certificates, via proofs of the logical reasoning the solver has performed, address this issue by decoupling confidence in the results from the solver’s implementation. In this talk we will describe the complete redesign and extension of cvc5's (a state-of-the-art SMT solver) proof-production infrastructure, thus enabling its better integration into proof assistants, such as Lean and Isabelle/HOL, and industrial settings. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/