Neural tools for formal verification

We develop practical tools that make formal proof assistants easier to use. For example, LLMstep uses language models to provide verified next-step suggestions in Lean.

LLMstep integrates language models and the Lean proof assistant.
LLMstep suggestions on a real-world formalization of the Amazon Web Services Cedar Policy Language.

Related publications


  1. Sean Welleck, and Rahul Saha
    In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, 2023