Document Open Access Logo

Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

Authors Hanna Lachnitt , Mathias Fleury , Haniel Barbosa , Jibiana Jakpor , Bruno Andreotti , Andrew Reynolds , Hans-Jörg Schurr , Clark Barrett , Cesare Tinelli

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.26.pdf
  • Filesize: 1.04 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • interactive theorem proving
  • proof assistants
  • Isabelle/HOL
  • SMT
  • certification
  • proof certificates
  • proof reconstruction
  • proof automation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Sledgehammer is a tool that increases the level of automation in the Isabelle/HOL proof assistant by asking external automatic theorem provers (ATPs), including SMT solvers, to prove the current goal. When the external ATP succeeds it must provide enough evidence that the goal holds for Isabelle to be able to reprove it internally based on that evidence. In particular, Isabelle can do this by replaying fine-grained proof certificates from proof-producing SMT solvers as long as they are expressed in the Alethe format, which until now was supported only by the veriT SMT solver. We report on our experience adding proof reconstruction support for the cvc5 SMT solver in Isabelle by extending cvc5 to produce proofs in the Alethe format and then adapting Isabelle to reconstruct those proofs. We discuss several difficulties and pitfalls we encountered and describe a set of tools and techniques we developed to improve the process. A notable outcome of this effort is that Isabelle can now be used as an independent proof checker for SMT problems written in the SMT-LIB standard. We evaluate cvc5’s integration on a set of SMT-LIB benchmarks originating from Isabelle as well as on a set of Isabelle proofs. Our results confirm that this integration complements and improves Sledgehammer’s capabilities.

Cite As Get BibTex

Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.26

Author Details

Hanna Lachnitt
  • Stanford University, CA, USA
Mathias Fleury
  • University of Freiburg, Germany
Haniel Barbosa
  • Universidade Federal de Minas Gerais, Belo Horizonte, Brazil
Jibiana Jakpor
  • Stanford University, CA, USA
Bruno Andreotti
  • Universidade Federal de Minas Gerais, Belo Horizonte, Brazil
Andrew Reynolds
  • University of Iowa, Iowa City, IA, USA
Hans-Jörg Schurr
  • University of Iowa, Iowa City, IA, USA
Clark Barrett
  • Stanford University, CA, USA
Cesare Tinelli
  • University of Iowa, Iowa City, IA, USA

Funding

This work was supported in part by the Stanford Center for Automated Reasoning, a gift from Amazon Web Services, a gift from Intel Corporation, and the Defense Advanced Research Projects Agency (DARPA) under contract FA8750-24-2-1001. Any opinions, findings, and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of DARPA.

References

  1. Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 367-386. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_19.
  2. The authors of cvc5. cvc5’s C++ API. https://cvc5.github.io/docs-ci/docs-main/api/cpp/enums/proofrule.html, 2025. [Online; accessed 12-Feburary-2025].
  3. The authors of cvc5. Proof production. https://cvc5.github.io/docs-ci/docs-main/proofs/proofs.html, 2025. [Online; accessed 10-Mar-2025].
  4. Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:3)2022.
  5. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 415-442. Springer, 2022. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  6. Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning, 64(3):485-510, 2020. URL: https://doi.org/10.1007/s10817-018-09502-y.
  7. Haniel Barbosa, Mathias Fleury, Pascal Fontaine, and Hans-Jörg Schurr. The Alethe Proof Format. An Evolving Specification and Reference. https://verit.gitlabpages.uliege.be/alethe/specification.pdf, 2024. [Online; accessed 22-November-2025].
  8. Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark Barrett. Flexible proof production in an industrial-strength SMT solver. In Jasmin Blanchette, Laura Kovács, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 15-35. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_3.
  9. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016. Google Scholar
  10. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109-128, 2013. URL: https://doi.org/10.1007/S10817-013-9278-5.
  11. Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, volume 6173 of Lecture Notes in Computer Science, pages 107-121. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14203-1_9.
  12. Sascha Böhme and Tjark Weber. Fast LCF-style proof reconstruction for Z3. In Interactive Theorem Proving: First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings 1, pages 179-194. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14052-5_14.
  13. Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, and Pascal Fontaine. veriT: An open, trustable and efficient SMT-solver. In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science, pages 151-156. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_12.
  14. Jürgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An interpolating SMT solver. In Alastair F. Donaldson and David Parker, editors, Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, volume 7385 of Lecture Notes in Computer Science, pages 248-254. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31759-0_19.
  15. Alessio Coltellacci, Stephan Merz, and Gilles Dowek. Reconstruction of SMT proofs with Lambdapi. In Giles Reger and Yoni Zohar, editors, Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024), Montreal, Canada, July, 22-23, 2024, volume 3725 of CEUR Workshop Proceedings, pages 13-23. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3725/paper8.pdf.
  16. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt Jr., Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 220-236. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  17. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Proofs and refutations, and Z3. In Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate A. Schmidt, and Stephan Schulz, editors, Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. URL: https://ceur-ws.org/Vol-418/paper10.pdf.
  18. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  19. Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, and Makarius Wenzel. Seventeen provers under the hammer. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 8:1-8:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITP.2022.8.
  20. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett. Smtcoq: A plug-in for integrating SMT solvers into Coq. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 126-133. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_7.
  21. Herbert B. Enderton. A mathematical introduction to logic. Academic Press, 1972. Google Scholar
  22. Mathias Fleury and Nikolaj Bjorner. Internal variables in proofs. https://github.com/Z3Prover/z3/issues/5073, 2021. [Online; accessed 22-November-2025].
  23. Mathias Fleury and Hans-Jörg Schurr. Reconstructing veriT proofs in Isabelle/HOL. In Giselle Reis and Haniel Barbosa, editors, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019, volume 301 of EPTCS, pages 36-50, 2019. URL: https://doi.org/10.4204/EPTCS.301.6.
  24. Mohamed Yacine El Haddad, Guillaume Burel, and Frédéric Blanqui. EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). In Giselle Reis and Haniel Barbosa, editors, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019, volume 301 of EPTCS, pages 27-35, 2019. URL: https://doi.org/10.4204/EPTCS.301.5.
  25. S Hitharth, Cayden Codel, Hanna Lachnitt, and Bruno Dutertre. Extending DRAT to SMT. In 2024 Formal Methods in Computer-Aided Design (FMCAD), pages 18-28. TU Wien Academic Press, 2024. URL: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_8.
  26. Jochen Hoenicke and Tanja Schindler. A simple proof format for SMT. In David Déharbe and Antti E. J. Hyvärinen, editors, Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022, volume 3185 of CEUR Workshop Proceedings, pages 54-70. CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3185/paper9527.pdf.
  27. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207-220, 2009. Google Scholar
  28. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an os kernel. In Jeanna Neefe Matthews and Thomas E. Anderson, editors, Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, pages 207-220. ACM, 2009. URL: https://doi.org/10.1145/1629575.1629596.
  29. Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett, and Cesare Tinelli. IsaRare: Automatic verification of SMT rewrites in Isabelle/HOL. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14570 of Lecture Notes in Computer Science, pages 311-330. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-57246-3_17.
  30. Peter Lammich. The GRAT tool chain - efficient (UN)SAT certificate checking with formal correctness guarantees. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 457-463. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_29.
  31. Peter Lammich. Fast and verified UNSAT certificate checking. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 439-457. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_26.
  32. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-45949-9.
  33. Andres Nötzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Reconstructing fine-grained proofs of rewrites using a domain-specific language. In Alberto Griggio and Neha Rungta, editors, 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pages 65-74. IEEE, 2022. URL: https://doi.org/10.34727/2022/ISBN.978-3-85448-053-2_12.
  34. Lawrence C. Paulson, Tobias Nipkow, and Makarius Wenzel. From LCF to Isabelle/HOL. CoRR, abs/1907.02836, 2019. URL: https://arxiv.org/abs/1907.02836.
  35. Florian Pollitt, Mathias Fleury, and Armin Biere. Faster LRAT checking than solving with CaDiCaL. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 21:1-21:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.21.
  36. Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine. Alethe: Towards a generic SMT proof format (extended abstract). In Chantal Keller and Mathias Fleury, editors, Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021, volume 336 of EPTCS, pages 49-54, 2021. URL: https://doi.org/10.4204/EPTCS.336.6.
  37. Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais. Reliable reconstruction of fine-grained proofs in a proof assistant. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 450-467. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_26.
  38. Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT proof checking using a logical framework. Formal Methods in System Design, 42(1):91-118, 2013. URL: https://doi.org/10.1007/s10703-012-0163-3.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact