AI Tools for Formal Verification

We build AI-powered tools that make formal verification more accessible, efficient, and useful to mathematicians and programmers.

Related publications

2026

  1. Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
    Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations
    Hita Kambhamettu, Will Crichton, Sean Welleck, and 2 more authors
    arXiv, 2026
  2. DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
    DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
    Tate Rowney, Riyaz Ahuja, Jeremy Avigad, and 1 more author
    2026
    FMCAD 2026
    Code
  3. LeanArchitect: Automating Blueprint Generation for Humans and AI
    LeanArchitect: Automating Blueprint Generation for Humans and AI
    Thomas Zhu, Pietro Monticone, Jeremy Avigad, and 1 more author
    2026
    ITP 2026
    Code
  4. Premise Selection for a Lean Hammer
    Premise Selection for a Lean Hammer
    Thomas Zhu, Joshua Clune, Jeremy Avigad, and 2 more authors
    2026
    ICLR 2026 Oral (Top 1%)
    Code Website

2023

  1. llmstep: LLM proofstep suggestions in Lean
    llmstep: LLM proofstep suggestions in Lean
    Sean Welleck, and Rahul Saha
    In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, 2023