Crush: Extensible Proof Automation for Lean

Summary (Overview)

• Crush is an extensible SMT-backed proof automation framework for the Lean proof assistant that bridges the gap between Lean's higher-order, polymorphic logic and first-order SMT solvers.
• The framework employs defunctionalization to encode higher-order functions (including lambdas, partial applications, and function-valued arguments) into first-order SMT logic, with a mechanized soundness proof in Lean itself.
• Crush provides extensible translation interfaces (head-indexed and type-indexed rewrite rules) allowing users to customize how Lean types, functions, and operators are encoded to SMT without modifying the core translator.
• It supports two proof reconstruction paths: unsat core-guided search using native Lean tactics, and full replay of solver inference steps (Alethe format) via extensible rewrite rules.
• In evaluation across 754 verification conditions from four benchmark suites (Curated, Cashmere, Velvet, PLean), crush discharges 709 VCs (94.0%) when trusting the solver and 693 (91.9%) with kernel-checked proofs, outperforming all baselines including auto (82.5%), grind (85.0%), lean-smt, and Duper.

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses the integration of automated theorem provers (ATPs) with proof assistants (PAs). While PAs like Lean, Rocq, Isabelle/HOL, and Agda provide rich type systems supporting higher-order and polymorphic constructs, ATPs like Z3, CVC5, and E-Prover offer powerful automation but support less expressive (typically first-order) logics.

The two main challenges in this integration are:

1. Translation (ITP → ATP): Translating expressive proof obligations (with polymorphism, higher-order functions, user-defined abstractions) into the solver's first-order logic.
2. Proof Reconstruction (ATP → ITP): Reconstructing kernel-checkable proofs from solver certificates (unsat cores or proof scripts).

Limitations of Existing Approaches

The paper highlights key gaps in existing tools for Lean:

• lean-auto: Supports polymorphism but lacks higher-order function support, custom encodings, and proof reconstruction.
• LeanHammer: Supports higher-order functions but lacks extensible encodings and replay.
• lean-smt: Supports extensible encodings and replay but not higher-order functions.
• grind and aesop: Native Lean tactics with good proof production but limited to internal decision procedures.

Table 1 (from paper): Qualitative comparison of goal translation and proof reconstruction.

Methodology

3. Extensible Lean-to-SMT Translation

Crush provides two mechanisms for translating Lean terms into SMT:

3.1 Definition Unfolding

The @[crush_unfold] attribute exposes defining equations of functions to the SMT query. For example:

@[crush_unfold]
def clamp (x lo hi : Int) : Int :=
    if x < lo then lo
    else if hi < x then hi else x

theorem clamp_bounds (x lo hi : Int) (h : lo ≤ hi) :
    lo ≤ clamp x lo hi ∧ clamp x lo hi ≤ hi := by
  crush

3.2 Head- and Type-Indexed Term Translation

Let $e^{\flat}$ denote the SMT term produced from a Lean expression $e$, and $\tau^{\flat}$ denote the SMT sort used to represent a Lean type $\tau$.

• Head-indexed translation: Rewrite rules matching the head symbol of an application. E.g., for the NAND function:

  $$(\text{Nand } x \; y)^{\flat} = \mathsf{bvnand}(x^{\flat}, y^{\flat})$$

• Type-indexed translation: Rewrites grouped by type, e.g., handling both Bool.not and Bool.xor under a Bool type pattern.

3.3 Coordinating Sort and Term Translation

Users can define rewrite rules over type applications to encode custom Lean types. For example, TotalMap κ ν can be encoded as SMT Array sort, with get → select and set → store. Crush performs light-weight sort checking on emitted queries to catch incompatible sort/term translations.

4. Higher-Order Translation via Defunctionalization

4.1 Defunctionalization

For a nondependent function type $\theta = \sigma_1 \rightarrow \dots \rightarrow \sigma_n \rightarrow \tau$ (where $\tau$ is not a function type), crush introduces:

1. An uninterpreted sort $\mathsf{Fn}_{\theta}$ for function values.
2. An application symbol with signature:

$$\mathsf{app}_{\theta}: \mathsf{Fn}_{\theta} \times \sigma_{1}^{\flat} \times \dots \times \sigma_{n}^{\flat} \to \tau^{\flat}$$

Lambdas and captured variables: For each lambda $\ell = \lambda x_1 \dots x_n.\; e$, a fresh uninterpreted symbol $\mathsf{clos}_{\ell}$ is introduced, with axiom:

$$\forall \bar{y}, \bar{x}. \quad \mathsf{app}_{\theta}(\mathsf{clos}_{\ell}(\bar{y}), \bar{x}) = e^{\flat}$$

where $\bar{y}$ are captured variables.

Partial application: η-expansion transforms partial applications into closures. Function equality: Extensionality axioms are emitted when comparing function values. Guarded subtypes (e.g., Nat within Int) are represented with guards like $x \geq 0$.

4.2 Soundness of Defunctionalization

The paper formalizes higher-order (HO) and first-order (FO) languages with denotational semantics (Fig. 8), then proves:

Theorem 1 (Soundness): For every finite collection $T$ of closed higher-order formulas, if $\mathcal{D}(T)$ is unsatisfiable, then $T$ is unsatisfiable.

Key definitions include:

• Defunctionalization $\mathcal{F}(e) = (e^{\flat}, C_e, E_e)$ where $C_e$ are closure equations and $E_e$ are extensionality axioms.
• First-order encoding: $\mathcal{D}(T) = \bigcup_{\varphi \in T} \left(C_{\varphi} \cup E_{\varphi} \cup \{\varphi^{\flat}\}\right)$

The proof uses a canonical model extension $M^{\star}$ interpreting Fn sorts as function spaces:

$$\llbracket \mathsf{Fn}_{\theta} \rrbracket_{M^{\star}} = \llbracket \theta \rrbracket_{M}$$

5. Proof Reconstruction

Crush supports two reconstruction approaches:

5.1 Core-Guided Reconstruction

• Maps unsat core assertions back to Lean hypotheses
• Searches for proofs using native Lean tactics (e.g., omega, grind)
• Extensible via @[crush_reconstruct] theorem hints

5.2 Extensible Solver Inference Replay

• Replays Alethe proof scripts from SMT solvers
• register_crush_replay term: maps SMT operators to Lean terms (type-checked by kernel)
• register_crush_replay rule: translates solver inference steps to Lean proofs

Example: handling bv-not-idemp rule using BitVec.not_not lemma: $\sim(\sim x) = x$

Empirical Validation / Results

6. Evaluation Setup

• 754 VCs across four suites: Curated (20), Cashmere (38), Velvet (504), PLean (192)
• Baselines: lean-auto (auto), Duper, lean-smt, Grind
• Hardware: Apple M1 Pro, 32 GB RAM
• Solver: CVC5 1.3.4
• Limits: 5s per solver call, 1M Lean heartbeats per tactic

6.1 Verification Coverage

Crush achieves the highest overall coverage even with kernel-checked proofs required. Runtime curves show a tradeoff: grind is faster on many VCs but crush achieves higher overall coverage.

6.2 Pairwise Comparison

Table 2 (from paper): Head-to-head comparison with crush using proof reconstruction.

Crush discharges more VCs in all pairs except against auto on PLean (2 vs. 10).

6.3 Proof Reconstruction Analysis

Table 3 (from paper): Proof reconstruction failures among 503 VCs discharged by SMT.

Key finding: Adding core-guided reconstruction enables crush to close many more VCs (693 vs. 241 with Alethe replay alone, vs. 431 for lean-smt). The main limitation is that CVC5 cannot generate Alethe proofs for all theories (particularly arrays).

Table 4 (from paper): Implementation size of built-in Alethe replay extensions.

Theoretical and Practical Implications

Theoretical Contributions

1. Mechanized soundness proof: Unlike tools like CoqHammer that have informal soundness arguments with known approximation issues, crush formally proves the soundness of its defunctionalization pass in Lean itself, providing strong correctness guarantees.

2. First-class treatment of higher-order functions: The defunctionalization approach with explicit application symbols, closure axioms, and extensionality provides a principled bridge between higher-order and first-order logic.

3. Extensible architecture: The pattern-based translation and replay interfaces separate the core pipeline from user extensions, allowing customization without compromising the core's soundness.

Practical Implications

1. Improved verification coverage: Crush discharges 94.0% of VCs (91.9% with proofs), significantly outperforming native tactics (grind: 85.0%) and existing SMT integrations (lean-smt: 57.2%, Duper: 54.8%).

2. Kernel-level trust: All reconstructed proofs are independently checked by the Lean kernel, maintaining the highest level of trustworthiness.

3. Low implementation overhead for extensions: The replay library required only 1,053 LoC for 55 handlers covering six theory categories, demonstrating the practicality of the extension interface.

4. Flexible integration: Crush works both as a standalone tactic and as a backend for third-party automation systems like Loom.

Conclusion

Main Takeaways

Crush successfully addresses the two main challenges of ATP-PA integration:

1. Translation: Supports higher-order, polymorphic Lean constructs via defunctionalization with a mechanized soundness proof.
2. Proof reconstruction: Combines unsat core-guided search with extensible Alethe proof replay for kernel-checked proofs.

The framework outperforms all baselines across diverse benchmark suites covering verification, distributed protocols, and general mathematics, achieving high coverage even when kernel-checked proofs are required.

Future Work

The authors identify several directions for future research:

1. Dependent function types: Extending the supported fragment beyond nondependent higher-order constructs.
2. Broader soundness formalization: Extending beyond defunctionalization to the full Lean-to-SMT-LIB translation.
3. Additional proof integrations: Integrating tactics like Duper, supporting CPC certificates, and synthesizing non-emptiness proofs for choice expressions in solver certificates.
4. Better SAT feedback: Distinguishing true vs. spurious counter-examples when the solver reports SAT.

Data Availability

The implementation, mechanized proofs, benchmark data, and reproduction scripts are publicly available at: https://github.com/AD1024/lean-crush/tree/tacas-ae