Proof Certificates in Satisfiability Modulo Theories - SMT Solver Integration and Verification

Learn about proof certificates in Satisfiability Modulo Theories (SMT) through a 59-minute Topos Institute Colloquium talk that explores automated reasoning paradigms and theorem proving. Dive into the development of proof certificates for the cvc5 SMT solver, understanding how they enable independent verification of theorem correctness while reducing trusted code requirements. Explore the integration possibilities with proof assistants like Coq, Isabelle/HOL, and Lean. Follow the journey through SMT solving fundamentals, including Boolean Satisfiability, proof module architecture, and the challenges of SMT proofs. Examine key components such as internal proof calculus, proof generators, and the generation process for substitution and rewriting. Gain insights into the practical applications of SMT proofs and their role in enhancing automated reasoning systems.