Lean 4: A Unified Platform for Programming and Verification

Leo de Moura
Senior Principal Applied Scientist, AWS
Chief Architect, Lean FRO

NASA Formal Methods Symposium | May 6, 2026

zlib in Lean

A general-purpose AI converted zlib (a C compression library) to Lean, passed the test suite, and proved the code correct.

theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
    (hsize : data.size < 1024 * 1024 * 1024) :
    ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data

Round-trip correctness, every compression level, machine-checked. lean-zip

When AI Writes the World's Software, Who Verifies It?

What is Lean?

A programming language and a proof assistant

Same language for code and proofs.

Lean is implemented in Lean. Very extensible.

Lean is scalable.

Small trusted kernel. Proofs can be exported and independently checked.

Programming and Theorem Proving in Lean

"You have written my favorite computer game" — Kevin Buzzard

def reverse : List α → List α
  | [] => []
  | x :: xs => reverse xs ++ [x]

theorem reverse_append (xs ys : List α)
    : reverse (xs ++ ys) = reverse ys ++ reverse xs := byα:Type u_1xs:List αys:List α⊢ reverse (xs ++ ys) = reverse ys ++ reverse xs
  induction xs with
  | nil =>nilα:Type u_1ys:List α⊢ reverse ([] ++ ys) = reverse ys ++ reverse [] simp [reverse]All goals completed! 🐙
  | cons x xs ih =>consα:Type u_1ys:List αx:αxs:List αih:reverse (xs ++ ys) = reverse ys ++ reverse xs⊢ reverse (x :: xs ++ ys) = reverse ys ++ reverse (x :: xs) simp [reverse, ih]All goals completed! 🐙

#eval[3, 2, 1] reverse [1, 2, 3]
[3, 2, 1]

The "game board": you see goals and hypotheses, then apply moves (tactics).

Each tactic transforms the goal until nothing remains. The kernel checks the final proof term.

The Kernel Catches Mistakes

example : reverse [1, 2, 3] = [1, 2, 3] := by⊢ reverse [1, 2, 3] = [1, 2, 3] simp [reverse]⊢ Falseunsolved goals
⊢ False

You don't need to trust me, or my automation. You only need to trust the small kernel.

Incorrect proofs are rejected.

Multiple Independent Kernels

arena.lean-lang.org hosts independent kernel implementations.

The reference kernel — C++.
nanoda — Rust.
lean4lean — Lean.
nanobruijn — Rust.
Many others.

Anyone can build a kernel and submit it.

Disagreement between independent kernels exposes bugs that neither would catch alone.

The State of Lean

250,000+ unique installations: VS Code (143K) + Open VSX (107K).

9,000+ GitHub repositories depending on Lean.

Industry: AWS, Google, Microsoft, Mistral, Nethermind, Galois, others.

"Lean has become the de facto choice for AI-based systems of mathematical reasoning." — ACM SIGPLAN Award

Lean as an IDE

Real-time feedback: errors, goals, and hints as you type. The IDE is where we collaborate with AI now.

Claude Code: sum.lean with sorry

AI Proves the Theorem

AI found the proof and explained its strategy in natural language:

Claude Code: sum.lean proved

Interactive Walkthrough: Sum Formula

def sum (n : Nat) : Nat :=
  if n = 0 then
    0
  else
    n + sum (n-1)

theorem sum_eq : 2 * sum n = n * (n+1) := byn:Nat⊢ 2 * sum n = n * (n + 1)
  induction n with
  | zero =>zero⊢ 2 * sum 0 = 0 * (0 + 1) simp [sum]All goals completed! 🐙
  | succ n ih =>succn:Natih:2 * sum n = n * (n + 1)⊢ 2 * sum (n + 1) = (n + 1) * (n + 1 + 1)
    unfold sumsuccn:Natih:2 * sum n = n * (n + 1)⊢ (2 * if n + 1 = 0 then 0 else n + 1 + sum (n + 1 - 1)) = (n + 1) * (n + 1 + 1); simpsuccn:Natih:2 * sum n = n * (n + 1)⊢ 2 * (n + 1 + sum n) = (n + 1) * (n + 1 + 1)
    rw [Nat.mul_add, ih, ← Nat.add_mul]succn:Natih:2 * sum n = n * (n + 1)⊢ (2 + n) * (n + 1) = (n + 1) * (n + 1 + 1)
    rw [Nat.add_comm 2 n, Nat.mul_comm]All goals completed! 🐙

Mathlib: 2.2M+ Lines of Formalized Mathematics

270,000+ formalized theorems.
750+ contributors.
2.2M+ lines of Lean.
1,500+ type classes and 20,000+ instances.
No competing proof assistant has this engagement.

Mathlib dependency graph

The Liquid Tensor Experiment

In 2020, Peter Scholze posed a formalization challenge.

"I spent much of 2019 obsessed with the proof of this theorem, almost getting crazy over it. I still have some small lingering doubts." — Peter Scholze

Johan Commelin led a team that verified the proof, with only minor corrections.

They verified and simplified it without fully understanding the proof. Lean was a guide.

"The Lean Proof Assistant was really that: an assistant in navigating through the thick jungle that this proof is." — Peter Scholze

Nature article on LTE

Lean Is Taking Mathematics by Storm

Six Fields Medalists engaged: Tao, Scholze, Viazovska, Gowers, Hairer, Freedman.

Carleson's Theorem (completed) — van Doorn
Liquid Tensor Experiment (completed) — Commelin
Equational Theories Project, Tao (completed)
Sphere Packing — Birkbeck, Hariharan, Lee, Ma, Mehta, Viazovska
Fermat's Last Theorem — Buzzard
Inter-Universal Teichmüller Theory — Mochizuki

At this scale, mathematics needs build systems, dependency graphs, code review, release engineering, and a precise medium for communication.

Reading vs Writing Formal Math

It is easier to read formal math than write it.
Formal math is easier to read than LaTeX.
You can click through, inspect definitions, check types.
AI can explain formal proofs and is making the writing part easier.

$Formal math in Lean$

Proof Assistants in the Age of AI

Verso: Written in Lean. Checked by Lean.

These slides are written in Verso.
Every code example you have seen — and will see — is type-checked by Lean as part of the build.
Verso is a domain-specific language embedded in Lean.
lean-lang.org is written in Verso.
My homepage is written in Verso.
Future math papers will embed type-checked Lean code.
Built by David Thrane Christiansen at the Lean FRO.

Verso: source and rendered output

Software Verification

Lean is not only for mathematics.

Cedar (AWS): Verified Authorization

Cedar — open-source authorization policy language. Used by AWS Verified Permissions and AWS Verified Access.

Cedar spec: the model is written in Lean.

Three examples of verified components: evaluator, authorizer, validator.

forbid_trumps_permit — if any forbid policy is satisfied, the request is denied.
allowed_only_if_explicitly_permitted — a request is allowed only if at least one permit policy is satisfied.
typecheck_is_sound — if the validator accepts a policy, evaluation produces a boolean.

Cedar website

Cedar — The Engineering Story

Executable Lean model alongside Rust production code. Lean model ~10× smaller than Rust.

Cedar differential testing

~100M differential random tests nightly. Lean: 5 μs/test. Rust: 7 μs/test.
Release gate: no Cedar version ships unless model, proofs, and differential tests are current.

"We've found Lean to be a great tool for verified software development." — Emina Torlak

SampCert (AWS): Verified Differential Privacy

Differential privacy is the gold standard for privacy-preserving data analysis. Implementing it correctly is hard.

Mironov's attack exploited floating-point to break DP. Bugs in random number generation have destroyed privacy guarantees in real systems.

SampCert (Jean-Baptiste Tristan): the first comprehensive, mechanized foundation for executable DP implementations.

12,000+ lines of Lean proof.
Discrete Laplace and Gaussian samplers, proved correct using Fourier analysis and the Poisson summation formula from Mathlib.
Composition of mechanisms with budgets γ₁ and γ₂ yields budget γ₁ + γ₂.
Postprocessing: functions that don't access the secret database don't degrade privacy.

SampCert — Deployed at AWS

Custom code extractor: the deployed artifact does not go through the Lean compiler. TCB includes the extractor, not the compiler.

Performance: SampCert outperforms diffprivlib by >2× for discrete Gaussians.

Deployed in AWS Clean Rooms Differential Privacy.

PLDI 2025: "Verified Foundations for Differential Privacy."

"SampCert uses the Poisson summation formula from Mathlib to prove a production privacy service correct."

Strata (AWS): Language Syntax and Semantics

Strata: extensible platform for formalizing language syntax and semantics. Built in Lean. Open source.

Key idea: dialects (inspired by MLIR). Orthogonal, composable building blocks for modeling programming constructs.

Core, C_Simp, Laurel, SMTLib, Python, Boole.
Laurel pipeline: Python/Java/JavaScript → Laurel → Strata Core → VCG → SMT.
Dialect Definition Mechanism (DDM): embedded DSL in Lean for defining syntax and typing rules.
Boogie/Dafny-style verification infrastructure, built in Lean and extensible via Lean's metaprogramming.

Waimea (AWS): Verified Compiler for Trainium

CompCert-style verified compiler for AWS Trainium, Amazon's custom AI accelerator chip. ~200,000 lines of Lean code.

The ISA specification changes several times per week. Not a fixed ISA like x86.
Lean provides an up-to-date simulator that hardware and verification engineers share.
Lean + AI keeps the team in sync with hardware changes. Several hundred instructions per generation.

Long-term goal: end-to-end compiler verification — source program compiles to Trainium machine code, with a proof that compilation preserves semantics.

A single miscompilation on a training run that costs millions in compute is catastrophic.

SymCrypt (Microsoft): Verified Cryptography

SymCrypt verification with Aeneas

SymCrypt — Microsoft's core cryptographic library, rewritten in Rust.

Verification pipeline: Charon → Aeneas → Lean.

Aeneas: translates safe Rust to pure functional Lean code. The bridge that makes Rust verification in Lean practical.

SymCrypt — Verifying Code as Engineers Write It

They verify the Rust code as written by software engineers. No special verification-friendly subset.

Code is evolving: new optimizations for specific hardware (AVX-512, Arm NEON, …). Proofs adapt to rewrites.

"We are verifying code faster than we can write it." — Son Ho, SymCrypt, Microsoft

The proof maintenance burden is real and unavoidable. The fact that it stays manageable is the point.

Anneal (Google): Verified Unsafe Rust

Google's zerocopy team building "literate verification" for unsafe Rust using Lean and Aeneas.

Unsafe Rust accounts for ~2/3 of vulnerabilities in the Rust ecosystem. Safety invariants are documented only in prose comments.

Anneal: developers write Lean specifications directly in Rust doc comments.

spec blocks for safe code.
unsafe(axiom) blocks for opaque unsafe operations with pre/post conditions.
Type invariants for struct safety properties.
cargo anneal verify runs the pipeline: Charon → Aeneas → Lean.

Designed for AI agents. Antigravity demonstrated authoring unsafe Rust and proving its soundness.

Veil: Verified Distributed Protocols

Veil: verification of distributed protocols. Built on Lean as a library using Lean metaprogramming.

Push-button verification via SMT (cvc5/Z3) for decidable fragments.
Full interactive proofs in Lean when automation falls short.
Seamless transition between the two modes.
Foundational: Veil's VCG is proven sound w.r.t. the specification language semantics.
16 distributed protocol case studies. All 16 verified. Ivy failed on 2. 87.5% verified in under 15 seconds.

Veil: ring leader election

Veil — Beyond EPR + The Rabia Finding

Verified Paxos, Suzuki-Kasami, Reliable Broadcast outside the decidable EPR fragment. This is where Ivy's automation breaks down.

The Rabia finding: while porting Rabia from Ivy + Rocq to Veil, the team spotted an invariant discrepancy that went undetected across two separate tools.

One unified framework caught what two could not.

Loom (POPL 2026): the foundational layer underneath Veil. Correct-by-construction verifiers from monad transformer algebras.

Kraken (Google): x64 Semantics in Lean

Kraken is an x64 model written in Lean.

Intended for verifying sequential software that performs computations using common registers and memory.

Project started after the Lean@Google Hackathon in December 2025.

Move Borrow Checker: The Problem

Ilya Sergey (VERSE lab) formalized and verified Move's borrow checker in Lean. 39,000 lines of mechanized metatheory in 27 working days, using Claude as an AI coding assistant.

Move: smart contract language for the Sui and Aptos blockchains. Rust-like ownership discipline. References are access paths rooted in local variables. No lifetime annotations.

The borrow checker: tracks reachability between references using regular expressions over field paths.

Move Borrow Checker: What Was Proved

Formalized in Lean:

Relational type system encoding
Executable algorithmic type checker
Soundness proof: the algorithmic checker is sound w.r.t. the relational rules
Runtime semantics as a definitional interpreter
Type soundness: progress + preservation. Any function accepted by the type checker never reaches a preventable error across all execution paths.

39,000 non-blank lines. 267 commits. 153 preservation lemmas across 23 statement forms.

Move Borrow Checker: AI's Role

Claude (Opus 4.5/4.6) handled proof repair, pattern propagation, routine preservation cases.

Human insight still needed for novel proof strategies (e.g., weakening lemmas, inter-procedural reasoning for function calls took two days).

27 working days. Estimated 5-6 months without AI. Second largest PL metatheory mechanization in Lean, and very likely the largest accomplished predominantly using AI.

Blog post

CSLib: A Mathlib for Computer Science

CSLib aims to be a foundation for teaching, research, and new verification efforts, including AI-assisted.

CSLib: adding to CS foundations

Steering committee: Clark Barrett, Swarat Chaudhuri, Jim Grundy, Pushmeet Kohli, Leo de Moura, Fabrizio Montesi.

Signal Shot

Signal Shot is a public moonshot to verify the Signal protocol and its Rust implementation using Lean.

It is a joint effort of Signal (Rolfe Schmidt), the Beneficial AI Foundation (Max Tegmark), and the Lean FRO.

The pieces:

Aeneas,
Mathlib and CSLib,
Symbolic proof automation (grind) and scalable verification generation (SymM),
and AI.

Proof Automation

Do We Still Need Proof Automation?

"I thought AI would prove all theorems for us now."

Tactics are like game moves.
Better tactics = shorter proofs.
Better tactics = more powerful AI.
Compact proofs = better training data = better AI provers.

40 lines replaced by one grind call

What Is `grind`?

New proof automation, shipped in Lean v4.22. Kim Morrison and me.

A virtual whiteboard, inspired by modern SMT solvers.

Writes facts on the board. Merges equivalent terms.
Cooperating engines: congruence closure, E-matching, constraint propagation, guided case analysis.
Satellite theory solvers: cutsat (linear integer arithmetic), commutative rings (Gröbner), linarith, AC.
Native to dependent type theory. No translation to FOL.
Produces ordinary Lean proof terms. Kernel-checkable.

Lean Goal

→

Preprocessing

→

Internalization

→

E-graph

↔

cutsat

↔

rings

↔

linarith

↔

orders

↔

`grind` — Theory Combination

example [CommRing α] [NoNatZeroDivisors α]
    (a b c : α) (f : α → Nat)
    : a + b + c = 3 →
      a^2 + b^2 + c^2 = 5 →
      a^3 + b^3 + c^3 = 7 →
      f (a^4 + b^4) + f (9 - c^4) ≠ 1 := byα:Type u_1inst✝¹:CommRing αinst✝:NoNatZeroDivisors αa:αb:αc:αf:α → Nat⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → f (a ^ 4 + b ^ 4) + f (9 - c ^ 4) ≠ 1
  grindAll goals completed! 🐙

Three solvers meet at the E-graph:

Ring solver derives a^4 + b^4 = 9 - c^4.
Congruence closure lifts it to f (a^4 + b^4) = f (9 - c^4).
Linear integer arithmetic closes 2 * f (9 - c^4) ≠ 1.

The Nelson-Oppen playbook. Inside dependent type theory. No SMT translation layer.

`grind` — Typeclass-Parameterized Solvers

Satellite solvers activate automatically when the type classes are present.

cutsat — ToInt class. Int, Int32, BitVec 64, Fin n.
Ring — CommRing, CommSemiring, Field, IsCharP, NoNatZeroDivisors.
linarith — module over the integers. Preorders, partial, linear orders.
AC — any associative-commutative operator.

example (x y : Int)
    : 27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45 →
      -10 ≤ 7*x - 9*y →   7*x - 9*y ≤ 4 → False := byx:Inty:Int⊢ 27 ≤ 11 * x + 13 * y → 11 * x + 13 * y ≤ 45 → -10 ≤ 7 * x - 9 * y → 7 * x - 9 * y ≤ 4 → False
  grindAll goals completed! 🐙

-- BitVec 8 is a CommRing of characteristic 256.
-- No bitvector-specific theory needed.
example (x : BitVec 8) : (x - 16) * (x + 16) = x^2 := byx:BitVec 8⊢ (x - 16) * (x + 16) = x ^ 2
  grindAll goals completed! 🐙

`grind` — Annotations and E-Matching

Library authors annotate theorems; grind instantiates them by E-matching — pattern matching modulo the E-graph.

[grind =] — use the LHS as the E-matching pattern.
[grind →] — forward reasoning: patterns from hypotheses.
[grind ←] — backward reasoning: patterns from the conclusion.
grind_pattern — custom multi-patterns.
Constraint system on patterns: guard, check, is_value, is_strict_value.

@[grind =] theorem fg {x} : f (g x) = x := byx:Nat⊢ f (g x) = x
  unfold f gx:Nat⊢ 2 * x / 2 = x; omegaAll goals completed! 🐙

example {a b c} : f a = b → a = g c → b = c := bya:Natb:Natc:Nat⊢ f a = b → a = g c → b = c
  grindAll goals completed! 🐙

4,000+ grind uses in Mathlib.

Better Tactics = Better AI

example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
    (d t d_inv : α)
    (Δ40 : d * (d + t + d * t) = 0)
    (Δ41 : d^2 * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
    : d * d_inv = 1 →
      t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := byα:Type u_1inst✝²:CommRing αinst✝¹:IsCharP α 0inst✝:NoNatZeroDivisors αd:αt:αd_inv:αΔ40:d * (d + t + d * t) = 0Δ41:d ^ 2 * (d + d * t - 2 * d * t ^ 2 + d * t ^ 4 + d ^ 2 * t ^ 4) = 0⊢ d * d_inv = 1 → t + 2 * t ^ 2 - t ^ 3 - 2 * t ^ 4 + t ^ 5 = 0
  grindAll goals completed! 🐙

Quantum algebra example from "Categories generated by a trivalent vertex" — Morrison, Peters, Snyder.

When grind closes a goal in one step instead of fifty, the AI search tree shrinks dramatically.

Tao on `grind`

"I have been experimenting recently with the new tactic grind in Lean, which is a powerful tool inspired by 'good old-fashioned AI' such as satisfiability modulo theories (SMT) solvers... When I apply grind to a given subgoal, it can report a success within seconds... But, importantly, when this does not work, I quickly get a grind failed message." — Terence Tao

VC Generation & Scalability

VC Generation

A VC generator turns code and specifications into proof obligations.

Lean-based VC generators:

Aeneas — Rust verification via translation to Lean.
Velvet — a Dafny-style verifier built in Lean.
mvcgen — Lean's VC generator for monadic programs.

Issue: Verification condition generation with proof assistants has not scaled so far.

Adam Chlipala's group documented this for Rocq. The same story holds in Lean.

Andres' Challenge — The Language

Andres Erbsen — Google ISE Formal. Bedrock2. Fiat Cryptography.

A Rocq veteran distilled the scaling problem into a minimal challenge at Lean@Google Hackathon.

A small deeply embedded imperative language.

inductive Binop where
  | add | sub
  deriving Repr

inductive Expr where
  | literal (v: Int)
  | var (x: String)
  | op (bop : Binop) (e1 e2 : Expr)
  deriving Repr

inductive Cmd where
  | skip : Cmd
  | set : String → Expr → Cmd
  | seq : Cmd → Cmd → Cmd
  | input : String → Cmd
  -- ..
  deriving Repr

abbrev Memory       := PartialMap Word Byte
abbrev LocalContext := PartialMap String Word

Andres' Challenge — Operational Semantics

inductive IOEvent
  | IN : Word → IOEvent
  | OUT : Word → IOEvent

abbrev Post := List IOEvent → Memory → LocalContext → Prop

inductive Exec : Cmd → List IOEvent → Memory → LocalContext → Post → Prop
  | skip  : post es m l → Exec .skip es m l post
  | seq   : Exec c1 es m l mid →
            (∀ es' m' l', mid es' m' l' → Exec c2 es' m' l' post) →
            Exec (.seq c1 c2) es m l post
  | set   : (h_eval : Expr.eval m l e = some v) →
            (h_post : post es m (PartialMap.put l x v)) →
            Exec (.set x e) es m l post
  | input : (∀ v, post (IOEvent.IN v :: es) m (PartialMap.put l x v)) →
            Exec (.input x) es m l post
-- ..

theorem Exec.seq_cps (c1 c2 : Cmd) (es : List IOEvent)
    (m : Memory) (l : LocalContext) (post : Post)
    : Exec c1 es m l (fun es' m' l' => Exec c2 es' m' l' post) →
      Exec (.seq c1 c2) es m l post := byc1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Post⊢ (Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' post) → Exec (c1.seq c2) es m l post
  intro hc1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Posth:Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' post⊢ Exec (c1.seq c2) es m l post; apply Exec.seqac1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Posth:Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' post⊢ Exec c1 es m l ?midac1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Posth:Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' post⊢ ∀ (es' : List IOEvent) (m' : Memory) (l' : LocalContext), ?mid es' m' l' → Exec c2 es' m' l' postmidc1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Posth:Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' post⊢ Post; apply hac1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Posth:Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' post⊢ ∀ (es' : List IOEvent) (m' : Memory) (l' : LocalContext), Exec c2 es' m' l' post → Exec c2 es' m' l' post; introsac1:Cmdc2:Cmdes:List IOEventm:Memoryl:LocalContextpost:Posth:Exec c1 es m l fun es' m' l' => Exec c2 es' m' l' postes'✝:List IOEventm'✝:Memoryl'✝:LocalContexta✝:Exec c2 es'✝ m'✝ l'✝ post⊢ Exec c2 es'✝ m'✝ l'✝ post; assumptionAll goals completed! 🐙

Andres' Challenge — A Parametric Program

notation:130 a " ;;\n" b => Cmd.seq a b
notation:150 x " ::= " e:150 => Cmd.set x e
notation:160 a " +' " b:160 => Expr.op Binop.add (Expr.var a) (Expr.var b)
notation:160 a " -' " b:160 => Expr.op Binop.sub (Expr.var a) (Expr.var b)

/-
Generates a command sequence of the form
input b
a := b
a := a + a; a := a - b
...
a := a + a; a := a - b
-/
def generated_cmd (n : Nat) (a b : String) : Cmd :=
  .input b ;;
  a ::= .var b ;;
  repeated_cmds n a b

abbrev spec (m : Memory) : Post :=
  fun es m' l =>
    m' = m ∧
    ∃ v : Word, es = [IOEvent.IN v] ∧ l.get "a" = some v

def Goal (n : Nat) : Prop :=
  ∀ m l, Exec (generated_cmd n "a" "b") [] m l (spec m)

Andres' Challenge — Baseline

example : Goal 1 := by⊢ Goal 1
  intro m lm:Memoryl:LocalContext⊢ Exec (generated_cmd 1 "a" "b") [] m l (spec m); simp only [generated_cmd, repeated_cmds]m:Memoryl:LocalContext⊢ Exec
  (Cmd.input "b" ;;
    "a" ::= Expr.var "b" ;;
      "a" ::= "a" +' "a" ;;
        "a" ::= "a" -' "b" ;;
          Cmd.skip)
  [] m l (spec m); unfold specm:Memoryl:LocalContext⊢ Exec
  (Cmd.input "b" ;;
    "a" ::= Expr.var "b" ;;
      "a" ::= "a" +' "a" ;;
        "a" ::= "a" -' "b" ;;
          Cmd.skip)
  [] m l fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v
  apply Exec.seq_cpsam:Memoryl:LocalContext⊢ Exec (Cmd.input "b") [] m l fun es' m' l' =>
  Exec
    ("a" ::= Expr.var "b" ;;
      "a" ::= "a" +' "a" ;;
        "a" ::= "a" -' "b" ;;
          Cmd.skip)
    es' m' l' fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v; apply Exec.inputa.am:Memoryl:LocalContext⊢ ∀ (v : Word),
  Exec
    ("a" ::= Expr.var "b" ;;
      "a" ::= "a" +' "a" ;;
        "a" ::= "a" -' "b" ;;
          Cmd.skip)
    [IOEvent.IN v] m (PartialMap.put l "b" v) fun es m' l =>
    m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v; intro va.am:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= Expr.var "b" ;;
    "a" ::= "a" +' "a" ;;
      "a" ::= "a" -' "b" ;;
        Cmd.skip)
  [IOEvent.IN v] m (PartialMap.put l "b" v) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v
  apply Exec.seq_cpsa.a.am:Memoryl:LocalContextv:Word⊢ Exec ("a" ::= Expr.var "b") [IOEvent.IN v] m (PartialMap.put l "b" v) fun es' m' l' =>
  Exec
    ("a" ::= "a" +' "a" ;;
      "a" ::= "a" -' "b" ;;
        Cmd.skip)
    es' m' l' fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v; apply Exec.seta.a.a.h_evalm:Memoryl:LocalContextv:Word⊢ Expr.eval m (PartialMap.put l "b" v) (Expr.var "b") = some ?a.a.a.v✝a.a.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= "a" +' "a" ;;
    "a" ::= "a" -' "b" ;;
      Cmd.skip)
  [IOEvent.IN v] m ((PartialMap.put l "b" v).put "a" ?a.a.a.v✝) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some va.a.a.vm:Memoryl:LocalContextv:Word⊢ Word; simp_vca.a.a.h_evalm:Memoryl:LocalContextv:Word⊢ v = ?a.a.a.v✝a.a.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= "a" +' "a" ;;
    "a" ::= "a" -' "b" ;;
      Cmd.skip)
  [IOEvent.IN v] m ((PartialMap.put l "b" v).put "a" ?a.a.a.v✝) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some va.a.a.vm:Memoryl:LocalContextv:Word⊢ Word; rfla.a.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= "a" +' "a" ;;
    "a" ::= "a" -' "b" ;;
      Cmd.skip)
  [IOEvent.IN v] m ((PartialMap.put l "b" v).put "a" v) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v
  apply Exec.seq_cpsa.a.a.h_post.am:Memoryl:LocalContextv:Word⊢ Exec ("a" ::= "a" +' "a") [IOEvent.IN v] m ((PartialMap.put l "b" v).put "a" v) fun es' m' l' =>
  Exec
    ("a" ::= "a" -' "b" ;;
      Cmd.skip)
    es' m' l' fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v; apply Exec.seta.a.a.h_post.a.h_evalm:Memoryl:LocalContextv:Word⊢ Expr.eval m ((PartialMap.put l "b" v).put "a" v) ("a" +' "a") = some ?a.a.a.h_post.a.v✝a.a.a.h_post.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= "a" -' "b" ;;
    Cmd.skip)
  [IOEvent.IN v] m (((PartialMap.put l "b" v).put "a" v).put "a" ?a.a.a.h_post.a.v✝) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some va.a.a.h_post.a.vm:Memoryl:LocalContextv:Word⊢ Word; simp_vca.a.a.h_post.a.h_evalm:Memoryl:LocalContextv:Word⊢ Word.add (some v) (some v) = ?a.a.a.h_post.a.v✝a.a.a.h_post.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= "a" -' "b" ;;
    Cmd.skip)
  [IOEvent.IN v] m (((PartialMap.put l "b" v).put "a" v).put "a" ?a.a.a.h_post.a.v✝) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some va.a.a.h_post.a.vm:Memoryl:LocalContextv:Word⊢ Word; rfla.a.a.h_post.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec
  ("a" ::= "a" -' "b" ;;
    Cmd.skip)
  [IOEvent.IN v] m (((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v))) fun es m' l =>
  m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v
  apply Exec.seq_cpsa.a.a.h_post.a.h_post.am:Memoryl:LocalContextv:Word⊢ Exec ("a" ::= "a" -' "b") [IOEvent.IN v] m (((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v)))
  fun es' m' l' =>
  Exec Cmd.skip es' m' l' fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v; apply Exec.seta.a.a.h_post.a.h_post.a.h_evalm:Memoryl:LocalContextv:Word⊢ Expr.eval m (((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v))) ("a" -' "b") =
  some ?a.a.a.h_post.a.h_post.a.v✝a.a.a.h_post.a.h_post.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec Cmd.skip [IOEvent.IN v] m
  ((((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v))).put "a" ?a.a.a.h_post.a.h_post.a.v✝)
  fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some va.a.a.h_post.a.h_post.a.vm:Memoryl:LocalContextv:Word⊢ Word; simp_vca.a.a.h_post.a.h_post.a.h_evalm:Memoryl:LocalContextv:Word⊢ v = ?a.a.a.h_post.a.h_post.a.v✝a.a.a.h_post.a.h_post.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec Cmd.skip [IOEvent.IN v] m
  ((((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v))).put "a" ?a.a.a.h_post.a.h_post.a.v✝)
  fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some va.a.a.h_post.a.h_post.a.vm:Memoryl:LocalContextv:Word⊢ Word; rfla.a.a.h_post.a.h_post.a.h_postm:Memoryl:LocalContextv:Word⊢ Exec Cmd.skip [IOEvent.IN v] m ((((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v))).put "a" v)
  fun es m' l => m' = m ∧ ∃ v, es = [IOEvent.IN v] ∧ PartialMap.get l "a" = some v
  apply Exec.skipa.a.a.h_post.a.h_post.a.h_post.am:Memoryl:LocalContextv:Word⊢ m = m ∧
  ∃ v_1,
    [IOEvent.IN v] = [IOEvent.IN v_1] ∧
      ((((PartialMap.put l "b" v).put "a" v).put "a" (Word.add (some v) (some v))).put "a" v).get "a" = some v_1
  simp only [List.cons.injEq, IOEvent.IN.injEq, and_true, PartialMap.put_put,
    PartialMap.get_put, Option.some.injEq, and_self, exists_eq']All goals completed! 🐙

With Lean's default tactic framework, MetaM, this is superlinear.

Andres' Challenge tactics time by goal size

What Must Be Fast in VC Generation

A VC generator turns code and specifications into proof obligations.

Lean-based VC generators: Aeneas, Velvet, mvcgen.

All three share the same idiom — and need:

Efficient apply.
Efficient metavariable management.
Preserve term sharing.
Reuse simp results across VCs and across simulation steps.
Do not traverse the same subterms over and over.

SymM: Making Verification Scale

SymM: new monadic framework for high-performance software verification. Born after the Lean@Google Hackathon.
Designed for tools like Aeneas, mvcgen and Velvet that need to discharge thousands of verification conditions efficiently.

Without this, verifying something as large as Signal is slow and painful. With it, verification conditions get discharged efficiently.

SymM vs MetaM benchmark

SymM with cache reuse

SymM Interactive Mode

Humans and AI both need to inspect and steer VC generation.

example (p q : Prop) : p → q → p ∧ q := byp:Propq:Prop⊢ p → q → p ∧ q
  sym =>
    intro hp hqgrindp:Propq:Prophp:phq:q⊢ p ∧ q
    apply And.introp:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q
    apply hpp:Propq:Prophp:phq:q⊢ q
    apply hqAll goals completed! 🐙

register_sym_simp chainSimp where
  post := ground >> rewrite [Nat.add_zero, Nat.zero_add]

example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ 2*y + (1 + 0) := byx:Naty:Nath:x ≤ y⊢ 1 - 1 + x ≤ 2 * y + (1 + 0)
  sym =>
    simp chainSimpgrindx:Naty:Nath:x ≤ y⊢ x ≤ 2 * y + 1
    liaAll goals completed! 🐙

mvcgen — Ported to `SymM`

Lean's VC generator for monadic programs. Ported to SymM by Sebastian Graf (Lean FRO).

Andres' challenge using Lean monadic code. Linear out to n=1000.

Tactic time

Kernel time

Velvet — Ported to `SymM`

A Dafny-style verifier in Lean. Ported to SymM by Vova (Lean FRO intern). Preliminary results.

Before: Velvet ran ~3× slower than Dafny.
After: Faster than Dafny on 24 of 27 benchmarks; competitive on the other 3 (differenceMinMax, findEvenNumbers, mergeSorted).

One port beat Dafny on 24 of 27. Dafny has a vast TCB.

Dafny vs Velvet vs Velvet + Loom2 verification time

AI

Accelerating formal verification.

"Vibe Proving"

So many people are choosing Lean that even casual users are proving theorems with ChatGPT.

Erdos Prize paper

"The bottleneck for using AI to create strategies and make conjectures is we have to rely on human experts and the test of time to validate whether something is plausible or not." — Terence Tao, Dwarkesh Patel interview

International Mathematical Olympiad (IMO)

To date, every AI achieving medal-level IMO performance with formal proofs used Lean.

AlphaProof (Google DeepMind) — silver medal, IMO 2024
Aristotle (Harmonic) — gold medal, IMO 2025
SEED Prover (ByteDance) — silver medal, IMO 2025

AI startups

Leanstral (Mistral): the first open-source code agent designed for Lean 4.
Axiom: solved 12/12 problems on Putnam 2025.
DeepSeek Prover-V2: 88.9% on miniF2F. Open-source, 671B parameters.
Harmonic: Built the Aristotle AI — gold medal, IMO 2025.

Startups using Lean

The Lean FRO

Nonprofit. 20 engineers. Open source. Controlled by no single company.

Sebastian Ullrich and I launched it in August 2023.

29 releases and 8,500+ pull requests merged since launch.

Lean is not a research project anymore. We run the Lean FRO as a startup.

Public roadmaps | Our team

Conclusion

The Lean is extensible, scalable, and trusted.

SymM turn a superlinear bottleneck into a linear one.

Adoption: 250,000+ unique installs. 9,000+ GitHub repositories.
Trust: Multiple independent kernels. Comparator. Small TCB.
Mathematics on Lean: Six Fields Medalists. Liquid Tensor Experiment. Fermat's Last Theorem. Sphere packing. Equational Theories Project. Tao's Analysis I.
AI on Lean: Every AI achieving medal-level IMO performance with formal proofs used Lean (AlphaProof, Aristotle, SEED Prover). Axiom: 12/12 on Putnam 2025. zlib verified by a general AI.
Lean FRO: 20 engineers building Lean full-time.

Thank You

Leo de Moura
lean-lang.org
leanprover.zulipchat.com
lean-fro.org
leo@lean-fro.org

NFM 2026