{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:00:55Z","timestamp":1784804455807,"version":"3.55.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325884","type":"print"},{"value":"9783032325891","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    SMT solvers are used in many safety-critical applications. To provide evidence of the correctness of their answers, some SMT solvers generate externally checkable proof certificates. We present a high-performance checker for SMT proof certificates called\n                    <jats:italic>Ethos<\/jats:italic>\n                    . In contrast with other dedicated SMT proof checkers, Ethos does not implement a fixed proof calculus. Instead, it allows users to specify their own calculus in the declarative language Eunoia, which extends the familiar SMT-LIB syntax to make that easy and convenient. We give a short overview of Eunoia and then focus on Ethos itself. We describe multiple optimization and implementation details which make Ethos fast and practical. We also evaluate Ethos on proofs generated by cvc5, showing that the flexibility of Ethos allows us to efficiently check fine-grained proofs, containing no proof holes, over all SMT-LIB logics without floating point arithmetic.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32589-1_19","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:03:53Z","timestamp":1784801033000},"page":"305-314","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Ethos: A Fast Proof Checker for\u00a0the\u00a0Eunoia Logical Framework"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0829-5056","authenticated-orcid":false,"given":"Hans-J\u00f6rg","family":"Schurr","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8653-8084","authenticated-orcid":false,"given":"Mallku","family":"Soldevila","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: Carcara: An efficient proof checker and elaborator for SMT proofs in the alethe format. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part I. Lecture Notes in Computer Science, vol. 13993, pp. 367\u2013386. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"19_CR2","doi-asserted-by":"publisher","unstructured":"Assaf, A., et al.: DEDUKTI: a logical framework based on the $$\\lambda $$$$\\Pi $$-calculus modulo theory. CoRR abs\/2311.07185 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2311.07185","DOI":"10.48550\/ARXIV.2311.07185"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: CVC5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"19_CR4","unstructured":"Barbosa, H., Fleury, M., Fontaine, P., Schurr, H.J.: The Alethe proof format: an evolving specification and reference (2026). https:\/\/verit.gitlabpages.uliege.be\/alethe\/specification.pdf"},{"key":"19_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). https:\/\/www.smt-lib.org"},{"key":"19_CR6","unstructured":"Blanqui, F.: Translating libraries of definitions and theorems between proof systems (invited talk). In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving, ITP 2024, Tbilisi, Georgia, 9\u201314 September 2024. LIPIcs, vol.\u00a0309, pp. 2:1\u20132:1. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.2"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Bouchet, M., et al.: Block public access: trust safety verification of access control policies. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, 8\u201313 November 2020, pp. 281\u2013291. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409728","DOI":"10.1145\/3368089.3409728"},{"issue":"1","key":"19_CR8","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM 40(1), 143\u2013184 (1993). https:\/\/doi.org\/10.1145\/138027.138060","journal-title":"J. ACM"},{"key":"19_CR9","doi-asserted-by":"publisher","unstructured":"Hitarth, S., Codel, C.R., Lachnitt, H., Dutertre, B.: Extending DRAT to SMT. In: Narodytska, N., R\u00fcmmer, P. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, 15\u201318 October 2024, pp. 1\u201311. IEEE (2024). https:\/\/doi.org\/10.34727\/2024\/ISBN.978-3-85448-065-5_8","DOI":"10.34727\/2024\/ISBN.978-3-85448-065-5_8"},{"key":"19_CR10","unstructured":"Hoenicke, J., Schindler, T.: A simple proof format for SMT. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) 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, 11\u201312 August 2022. CEUR Workshop Proceedings, vol.\u00a03185, pp. 54\u201370. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3185\/paper9527.pdf"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., et al.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, 17\u201321 October 2022, pp. 65\u201374. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_12","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_12"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2025 (non-incremental benchmarks) (2025). https:\/\/doi.org\/10.5281\/zenodo.16740866","DOI":"10.5281\/zenodo.16740866"},{"key":"19_CR13","unstructured":"Reynolds, A., Schurr, H.J., Soldevila, M., Tinelli, C.: The ethos user manual (2026). https:\/\/github.com\/cvc5\/ethos\/blob\/main\/user_manual.md"},{"key":"19_CR14","doi-asserted-by":"publisher","unstructured":"Schurr, H., et al.: Exploring the SMT-LIB benchmark library. In: Junges, S., Katz, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, 11\u201316 April 2026, Proceedings, Part I, pp. 150\u2013169. Lecture Notes in Computer Science, Springer (2026). https:\/\/doi.org\/10.1007\/978-3-032-22752-2_8","DOI":"10.1007\/978-3-032-22752-2_8"},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). In: Keller, C., Fleury, M. (eds.) Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, 11 July 2021. EPTCS, vol.\u00a0336, pp. 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Schurr, H.J., Preiner, M., Niemetz, A., Barrett, C., Fontaine, P., Tinelli, C.: SMT-LIB catalog 2025 (2025). https:\/\/doi.org\/10.5281\/zenodo.16290040","DOI":"10.5281\/zenodo.16290040"},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/S10703-012-0163-3","volume":"42","author":"A Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Meth. Syst. Des. 42(1), 91\u2013118 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0163-3","journal-title":"Formal Meth. Syst. Des."},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: Stepping stones in the TPTP world. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, 3\u20136 July 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14739, pp. 30\u201350. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_3","DOI":"10.1007\/978-3-031-63498-7_3"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32589-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:03:58Z","timestamp":1784801038000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32589-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325884","9783032325891"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32589-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}