Pith. sign in

REVIEW 3 major objections 6 minor 19 references

Reconstructing veriT Proofs in Isabelle/HOL

T0 review · 3 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read veriT's detailed proofs can be checked step by step inside Isabelle/HOL, making a second SMT backend practical for Sledgehammer.

desk verdict Solid engineering paper adding a second SMT backend to Isabelle's smt tactic; the context-to-equality translation is the soft spot but the experiments and exposition carry it. read the letter →

arxiv 1908.09480 v1 pith:3VQXEHKQ submitted 2019-08-26 cs.LO

Mathias Fleury (Max Planck Institut for Informatics) , Hans-Jörg Schurr (University of Lorraine , CNRS , Inria , LORIA) This is my paper · ORCID
classification cs.LO MSC 03B3568T15
keywords proofreconstructionSMTsolververiTIsabelle/HOLSledgehammerSMT-LIBSkolemizationkernel-levelchecking
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper shows that proofs produced by the SMT solver veriT can be checked inside the Isabelle/HOL proof assistant, step by step, in the inference kernel. It describes a reconstruction pipeline that parses veriT's SMT-LIB-style proof output, unfolds shared terms, translates the formulas into Isabelle/HOL, and replays each proof rule as a theorem. The authors report that the resulting veriT-powered smt tactic solves most of the goals that the existing Z3 backend solves, and that Sledgehammer sometimes suggests it as the fastest way to close a goal. The point of the work is that proof-producing external solvers can be made trustworthy by kernel-level replay, and that a second, independently implemented backend widens the coverage of automation in a proof assistant.

What carries the argument

The load-bearing mechanism is the reconstruction pipeline: parse the flat SMT-LIB-style proof into a structured datatype, unfold shared terms, translate terms to Isabelle/HOL, then replay steps one by one by applying the corresponding Isabelle theorem and unifying premises. Two features carry most of the difficulty: veriT's context, a stack of variables and variable–term bindings that acts as a substitution, is reinterpreted as a list of equalities in Isabelle and combined with a renaming step to avoid capture; and Skolem constants are folded aggressively into the terms to keep them small enough to replay. The proof format itself is part of the mechanism: anchors delimit subproofs, define-fun commands provide shorthand for Skolem terms, and rule annotations like :args supply the instantiations explicitly.

What would settle it

Feed veriT a small unsat core with nested variable bindings of the form $y\mapsto z, x\mapsto y \vdash n.\ Pxy \simeq Pyz$, run the reconstruction, and check whether Isabelle accepts the step with and without the renaming pass; if it accepts it without renaming, the translation is unsound. More generally, instrument the replay to print every translated premise and conclusion, and search for any step whose conclusion is not a logical consequence of the translated premises.

Watch

Extended reading notes

Core claim

On its own terms, the paper claims that veriT's proof output is detailed enough for faithful reconstruction in Isabelle/HOL: every step of the logged proof can be replayed as a theorem of the Isabelle kernel, so a user who trusts the kernel gets a veriT proof checked without trusting veriT. The reconstruction handles veriT's fine-grained Skolemization steps, subproofs with local assumptions, contexts that act as substitutions, and term sharing through SMT-LIB names. The central design choice is to represent veriT's context as a list of equalities in Isabelle and to add a renaming pass so that variables already bound in the context keep the meaning veriT intends. Experiments replace Z3 by veriT in existing smt calls and add veriT as a Sledgehammer backend; the result is that veriT-powered smt is regularly suggested as the fastest successful tactic, with a small number of failures traced to a veriT proof-printing bug, incomplete arithmetic simplification, and timeouts.

Load-bearing premise

The whole approach stands or falls on the translation from veriT's proof terms to Isabelle terms being faithful: if a context, Skolem term, or subproof is mis-translated, the kernel could be replaying a step that is not the step veriT actually derived.

Editorial extensions

If this is right

  • A veriT-generated proof, once reconstructed, is a kernel-checked theorem in Isabelle/HOL, so no separate trust in veriT is needed.
  • Sledgehammer can run veriT-powered smt as one of its candidate tactics and will suggest it when it is fastest, which happened on 25 goals in the ordered-resolution formalization and 4 in the SSA formalization.
  • Proof formats with explicit Skolemization and subproofs are easier to replay than formats that hide these steps; the paper argues that more detail makes reconstruction more robust.
  • The shared parsing and term-translation infrastructure means that adding a solver backend does not require rewriting the SMT-LIB front end.
  • Incomplete arithmetic reconstruction remains a bottleneck: Isabelle's linarith does not simplify equations by their gcd, and the paper adds a gcd-simplification procedure to recover goals like the one in Section 3.2.4.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next experiment is to enable the gcd-based arithmetic simplification globally and measure how reconstruction success changes on arithmetic-heavy goals.
  • The context-renaming method points to a general design principle for SMT proof formats: print substitution contexts as explicit equalities with fresh variables so they become lists of assumptions in any LCF-style kernel.
  • Because parsing and term translation are shared with the Z3 backend, the same pipeline could likely be retargeted to other solvers emitting SMT-LIB-style detailed proofs, with the main work being per-solver proof rules.
  • If veriT printed the linear-combination coefficients for arithmetic contradictions, Isabelle would not have to rediscover them, potentially making reconstruction faster than the Z3 backend.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper describes an implementation that reconstructs proofs produced by the SMT solver veriT inside Isabelle/HOL's smt tactic. It explains veriT's proof format, the parsing and translation of SMT-LIB terms into Isabelle terms, the replay of individual proof rules, and the handling of subproofs, Skolemization, and linear arithmetic. The experimental evaluation has two parts: replacing Z3 by veriT in existing smt calls yields 447 successful reconstructions, 4 failures, 47 veriT timeouts, and 4 unknown results (Table 1); and using Sledgehammer on two Isabelle formalizations produces 25 and 4 proof goals where the veriT-powered smt tactic is suggested as fastest (Table 2). The paper also reports a known veriT proof-printing bug and notes that the code is not yet integrated into the Isabelle release.

Significance. If the reconstruction is faithful, this is a useful engineering contribution: it provides Isabelle/HOL with a second SMT solver backend and demonstrates that veriT's detailed, SMT-LIB-based proof output can be replayed by an LCF-style kernel. The paper is honest about the limitations and failures, and the 447 successful replays on existing smt calls are a concrete data point. However, the paper's central claim depends on a translation from veriT's context-based proof steps to Isabelle equalities that is not accompanied by a correctness argument. The ambiguity in Section 2.1 and the heuristic renaming in Section 3.1 are load-bearing, because the Isabelle kernel certifies only the translated goal, not the correspondence between that goal and the original veriT step. The contribution is therefore conditional on closing this semantic gap.

major comments (3)
  1. [§2.1 and §3.1] The formal definition of the context substitution is inconsistent with the running example. In §2.1, the substitution for Γ = Γ′, x↦ϕ is defined as σ_{Γ′,x↦ϕ} = σ_{Γ′} ∘ [ϕ/x]. For the context y↦z, x↦y, this gives σ = [z/y] ∘ [y/x]; applying it to Pxy yields Pzz, not the Pyz claimed in §3.1. The example only works if the substitution is understood as simultaneous (or with some other non-compositional semantics), but that semantics is not defined in the paper. Please correct the definition and state explicitly whether the substitutions in a context are applied simultaneously or sequentially, and verify that the example goes through under the stated semantics.
  2. [§3.1] The renaming patch for variables that occur on both sides of ≃ is described in one sentence and is not justified. The Isabelle kernel verifies each replayed step only after the translation to Isabelle terms; it does not verify that the translated step is the image of the veriT step under a meaning-preserving map. Since the paper claims faithful reconstruction rather than merely successful replay, add a precise statement of the translation's soundness: for each veriT rule and context, if the veriT step is valid in veriT's semantics, then the translated Isabelle goal is derivable from the translated premises (or, equivalently, successful replay entails that the original goal holds in Isabelle/HOL). Without such a statement, the 447 successful replays do not rule out a translation that is only accidentally correct on the test suite.
  3. [§4.1 and Table 1] The four reconstruction failures are not categorized, and the paper acknowledges a veriT proof-printing bug that causes reconstruction errors. Please state for each failed case whether the failure is due to the veriT bug, to linarith incompleteness, or to the translation. In addition, since the veriT bug is described as replacing a term by an equivalent term without logging the replacement, explain why this bug cannot cause a successful replay of a step that is not actually derivable from the premises; otherwise the 'nearly all proofs' claim in §4.1 is difficult to interpret as evidence for the soundness of the reconstruction.
minor comments (6)
  1. [Abstract and Table 2] The abstract says the veriT-powered smt tactic is 'regularly suggested' by Sledgehammer, but Table 2 shows only 25 of 5019 and 4 of 5961 proof goals; consider softening this to 'sometimes' or reporting the fractions explicitly in the abstract.
  2. [§2.1, Example 1] The sentence 'Here the term ¬p(εx.¬p(x)) is Skolemized' is confusing because the example derives an equivalence about ∀x.p(x); please clarify which term is Skolemized.
  3. [§3.1] The phrase 'the substitution only applies on the left-hand side' is unclear because 'left-hand side' could refer to the left of the turnstile or the left of ≃; please rephrase, for example by saying explicitly that σΓ is applied only to ϕ, not to ψ, in a step Γ ⊿ ϕ ≃ ψ.
  4. [§3.2.4] In the arithmetic example, the text says 'because x and y are integers', but the displayed goal also contains z; please state the sorts of all variables and explain how the simplified inequality 20 ≤ 10×x − 25×y is obtained from 16 ≤ 10×x − 25×y.
  5. [Figure 3] The box 'Unfold FO encoding' in the pipeline diagram is not explained in the text; a sentence describing what is unfolded and at which stage would make the figure self-contained.
  6. [Throughout] There are several typos: 'the veriable is quantified' (§2.1), 'which in turns naturally' (§3.2.3), 'the implicit simplifications prevents' (§6), and 'Isabelle does not generates XOR or lets' (Appendix A).

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper reports an engineering reconstruction validated by kernel replay against external veriT proofs, and its self-citations are background rather than load-bearing.

full rationale

The paper's central claim is empirical and implementation-oriented: veriT's proof output is parsed, translated, and replayed step-by-step inside Isabelle/HOL's inference kernel, with success measured against actual veriT proofs and external benchmark goals from the Isabelle distribution, the Archive of Formal Proofs, and Sledgehammer runs. This is not a derivation in which the conclusion is presupposed by the inputs. The correctness guarantee comes from the kernel's independent checking of each replayed step, not from the paper's own definitions or fitted parameters. The authors cite their own prior work [2,3] for the proof-format history and for a previous prototype, but those citations do not carry the reconstruction claim: the present paper itself specifies the proof syntax and rules (Sections 2 and Appendix A) and describes the reconstruction pipeline (Section 3). No uniqueness theorem, ansatz, or renamed known result is imported from the authors' earlier publications. The paper even reports a genuine veriT proof-generation bug (Section 4.1), which shows the checking process is not vacuous. Concerns about the unverified translation semantics in Section 3.1 and about the acknowledged arithmetic-reconstruction difficulties are correctness risks, not circularity. The derivation chain is therefore self-contained with respect to circularity, and the appropriate finding is no significant circularity.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

This is a systems paper; no free parameters or invented entities are introduced. The analysis assumes the standard trust anchors of LCF-style proof reconstruction.

assumptions (3)
  • domain assumption The Isabelle/HOL inference kernel is sound.
    The reconstruction only checks that each proof step is a valid inference in Isabelle/HOL; it relies on the kernel's soundness.
  • domain assumption The veriT proof format and its implicit transformations (double negation removal, duplicate literal removal, tautology simplification, equality reorientation) are sound representations of veriT's reasoning.
    The reconstruction treats these implicit transformations as valid; a missing or incorrect implicit step would break reconstruction or soundness.
  • domain assumption The proof output of veriT is well-formed according to the stated grammar and the last step is the empty clause.
    The parser assumes the grammar in Figure 2 and that proof steps form a DAG with the final empty clause.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Reconstructing veriT Proofs in Isabelle/HOL." pith.science (2026). https://pith.science/paper/3VQXEHKQ

@misc{pith2026190809480,
  author       = {Pith},
  title        = {Pith review of: Reconstructing veriT Proofs in Isabelle/HOL},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3VQXEHKQ}},
  note         = {Machine review of arXiv:1908.09480}
}
read the original abstract

Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theories solver veriT which is part of the smt tactic. We describe in detail the architecture of our improved reconstruction method and the challenges we faced in designing it. Our experiments show that the veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest method to automatically solve proof goals.

Figures

Figures reproduced from arXiv: 1908.09480 by the authors.

Figure 1
Figure 1. Example proof output. Assumptions are introduced (line 1–2); a subproof renames bound [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. The proof grammar hfunction_defi, hsorted_vari, and htermi are as defined in the standard. The hproof_termi is the recursive htermi nonterminal redefined with the additional production for the choice binder. Input problems in the SMT-LIB standard contain a list of commands that modify the internal state of the solver. In agreement with this approach veriT’s proofs are also formed by a list of commands. The assume co… view at source ↗
Figure 3
Figure 3. The reconstruction pipeline (indices, steps, . . . ) from the raw proof. During parsing of the raw proof we also unfold the sharing, because Isabelle does not offer any sharing functionality. The first transformation is a change of the disjunction representation. In the proof output, veriT represents the outermost disjunction as a multiset by using the cl operator. In Isabelle, we replace this multiset by a disjunct… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 14 canonical work pages

  1. [1]

    In Jean-Pierre Jouannaud & Zhong Shao, editors: CPP 2011, LNCS 7086, Springer, pp

    Micha¨el Armand, Germain Faure, Benjamin Gr ´egoire, Chantal Keller, Laurent Th ´ery & Benjamin Werner (2011): A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In Jean-Pierre Jouannaud & Zhong Shao, editors: CPP 2011, LNCS 7086, Springer, pp. 135–150, doi:10.1007/978-3-642-25379-9 12

    work page doi:10.1007/978-3-642-25379-9 2011

  2. [2]

    Blanchette, Mathias Fleury & Pascal Fontaine (2019): Scalable Fine-Grained Proofs for Formula Processing

    Haniel Barbosa, Jasmin C. Blanchette, Mathias Fleury & Pascal Fontaine (2019): Scalable Fine-Grained Proofs for Formula Processing. Journal of Automated Reasoning, doi:10.1007/s10817-018-09502-y

    doi:10.1007/s10817-018-09502-y 2019

  3. [3]

    Blanchette, Mathias Fleury, Pascal Fontaine & Hans-J ¨org Schurr (2019): Better SMT proofs for easier reconstruction

    Haniel Barbosa, Jasmin C. Blanchette, Mathias Fleury, Pascal Fontaine & Hans-J ¨org Schurr (2019): Better SMT proofs for easier reconstruction. In Thomas C. Hales, Cezary Kaliszyk, Ramana Kumar, Stephan Schulz & Josef Urban, editors: AITP 2019

    work page 2019

  4. [4]

    www.SMT-LIB.org

    Clark Barrett, Pascal Fontaine & Cesare Tinelli (2016):The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org

    work page 2016

  5. [5]

    In Armin Biere, Marijn J

    Clark Barrett, Roberto Sebastiani, Sanjit Seshia & Cesare Tinelli (2009): Satisfiability Modulo Theories. In Armin Biere, Marijn J. H. Heule, Hans van Maaren & Toby Walsh, editors: Handbook of Satisfiability , chapter 26, Frontiers in Artificial Intelligence and Applications 185, IOS Press, pp. 825–885

    work page 2009

  6. [6]

    In Pascal Fontaine & Aaron Stump, editors: PxTP 2011, pp

    Fr´ed´eric Besson, Pascal Fontaine & Laurent Th´ery (2011): A Flexible Proof Format for SMT: A Proposal. In Pascal Fontaine & Aaron Stump, editors: PxTP 2011, pp. 15–26. Available at https://hal.inria.fr/ hal-00642544/

    work page 2011

  7. [7]

    Blanchette, Sascha B ¨ohme, Mathias Fleury, Steffen J

    Jasmin C. Blanchette, Sascha B ¨ohme, Mathias Fleury, Steffen J. Smolka & Albert Steckermeier (2016): Semi-intelligible Isar Proofs from Machine-Generated Proofs. Journal of Automated Reasoning 56(2), pp. 155–200, doi:10.1007/s10817-015-9335-3

    doi:10.1007/s10817-015-9335-3 2016

  8. [8]

    In Matt Kaufmann & Lawrence C

    Sascha B¨ohme & Tjark Weber (2010): Fast LCF-Style Proof Reconstruction for Z3. In Matt Kaufmann & Lawrence C. Paulson, editors: ITP 2010, LNCS 6172, Springer, pp. 179–194, doi:10.1007/978-3-642-14052- 5 14

    work page doi:10.1007/978-3-642-14052- 2010

Show all 19 references
  1. [9]

    Thomas Bouton, Diego C. B. de Oliveira, David D ´eharbe & Pascal Fontaine (2009): veriT: An Open, Trustable and Efficient SMT-solver. In Renate A. Schmidt, editor: CADE 2009, LNCS 5663, Springer, pp. 151–156, doi:10.1007/978-3-642-02959-2 12

    2009 doi

  2. [10]

    In: CC, ACM, pp

    Sebastian Buchwald, Denis Lohner & Sebastian Ullrich (2016): Verified construction of static single assign- ment form. In: CC, ACM, pp. 67–76, doi:10.1145/2892208.2892211

    2016

  3. [11]

    In Pascal Fontaine & Aaron Stump, editors: PxTP 2011, pp

    David D´eharbe, Pascal Fontaine & Bruno Woltzenlogel Paleo (2011): Quantifier Inference Rules for SMT Proofs. In Pascal Fontaine & Aaron Stump, editors: PxTP 2011, pp. 33–39. Available at https://hal. inria.fr/hal-00642535

    2011

  4. [12]

    Reynolds & Cesare Tinelli (2016): Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

    Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds & Cesare Tinelli (2016): Extending SMTCoq, a Certified Checker for SMT (Extended Abstract) . In Jasmin C. Blanchette & Cezary Kaliszyk, editors: HaTT 2016, EPTCS 210, pp. 21–29, doi:10.4204/EPTCS.210.5

    2016 doi

  5. [13]

    Electronic Notes in Theoretical Computer Science 144(2), pp

    Sean McLaughlin, Clark Barrett & Yeting Ge (2006): Cooperating Theorem Provers: A Case Study Com- bining HOL-Light and CVC Lite . Electronic Notes in Theoretical Computer Science 144(2), pp. 43–51, doi:10.1016/j.entcs.2005.12.005

    2006 doi

  6. [14]

    Leonardo de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In C. R. Ramakrishnan & Jakob Rehof, editors: TACAS 2008, LNCS 4963, Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3 24. 50 Reconstructing veriT Proofs in Isabelle/HOL

    2008 doi

  7. [15]

    Blanchette, Dmitriy Traytel & Uwe Waldmann (2018): Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover

    Anders Schlichtkrull, Jasmin C. Blanchette, Dmitriy Traytel & Uwe Waldmann (2018): Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover. Archive of Formal Proofs. http://isa-afp.org/ entries/Ordered_Resolution_Prover.html, Formal proof development

    2018

  8. [16]

    Blanchette, Dmitriy Traytel & Uwe Waldmann (2018): Formalizing Bach- mair and Ganzinger’s Ordered Resolution Prover

    Anders Schlichtkrull, Jasmin C. Blanchette, Dmitriy Traytel & Uwe Waldmann (2018): Formalizing Bach- mair and Ganzinger’s Ordered Resolution Prover . In: IJCAR, LNCS 10900, Springer, pp. 89–107, doi:10.1007/978-3-319-94205-6 7

    2018 doi

  9. [17]

    Wiley - Interscience Series in Discrete Mathematics and Optimization, Wiley

    Alexander Schrijver (1999): Theory of Linear and Integer Programming . Wiley - Interscience Series in Discrete Mathematics and Optimization, Wiley

    1999

  10. [18]

    Formal Methods in System Design 42(1), pp

    Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean & Cesare Tinelli (2013): SMT Proof Checking Using a Logical Framework. Formal Methods in System Design 42(1), pp. 91–118, doi:10.1007/s10703-012- 0163-3

    2013 doi

  11. [19]

    Archive of Formal Proofs

    Sebastian Ullrich & Denis Lohner (2016): Verified Construction of Static Single Assignment Form. Archive of Formal Proofs. http://isa-afp.org/entries/Formal_SSA.html, Formal proof development. A List of Proof Rules Rule Description TRUE , FALSE , AND POS, AND NEQ, OR POS, OR NE...

    2016

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.