Verified software development in Lean

Julia Markus Himmel

Lean FRO

Did you know that Lean is not just a theorem prover, but also a really good programming language? Also, check out all of the cool things that we added to Lean in the past two years that make it even better for programming and proving things about programs

Julia Markus Himmel

Lean FRO

Lean is a programming language

It's a functional programming language in the ML familiy just like OCaml, Haskell, F#, etc.

It compiles to fast native code.

It can be and is used to write any kind of program, not just Lean metaprograms.

As you know, it supports proofs, so you can do verified software development (as opposed to just software verification) in it!

Language Server & VS Code Extension

It's what makes Lean so productive (and fun)!

Way too many highlights to even attempt listing them.

Unknown identifier code action

Signature help

New compiler & `do` elaborator

Rewritten for better maintainability and extensibility

Expect more fixes, improvements and extension points!

Module System

Fine-grained control over which information files export

Default flips from public to private

Amazing for rebuild times

Amazing for kernel checking times

Amazing for encapsulation

Coinductive predicates

coinductive InfSeq (R : α → α → Prop) : α → Prop where
  | step : R a b → InfSeq R b → InfSeq R a

Automatically generates the coinduction principle:

#check@InfSeq.coinduct : ∀ {α : Sort u_1} (R : α → α → Prop) (pred : α → Prop),
  (∀ (a : α), pred a → ∃ b, R a b ∧ pred b) → ∀ (a : α), pred a → InfSeq R a @InfSeq.coinduct
@InfSeq.coinduct : ∀ {α : Sort u_1} (R : α → α → Prop) (pred : α → Prop),
  (∀ (a : α), pred a → ∃ b, R a b ∧ pred b) → ∀ (a : α), pred a → InfSeq R a

Verso

Our framework for building Lean-aware documentation tools.

These slides are powered by Verso!

theorem List.toArray_comp_toList :
    List.toArray (α := α) ∘ Array.toList = id := byα:Type u_1⊢ toArray ∘ Array.toList = id
  funext ahα:Type u_1a:Array α⊢ (toArray ∘ Array.toList) a = id a
  simpAll goals completed! 🐙

Cool new feature: Verso docstrings are checked and interactive!

set_option doc.verso true

/-- One side of the bijection between {name}`List` and {name}`ArayUnknown constant `Aray`` -/
theorem foo {l : List α} : l.toArray.toList = l := byα:Type u_1l:List α⊢ l.toArray.toList = l
  simpAll goals completed! 🐙

Grind

example (f : Nat → Nat)
    (h₁ : f (f x) = x)
    (h₂ : f (f (f y)) = y) :
    f x = y → f y = x := byx:Naty:Natf:Nat → Nath₁:f (f x) = xh₂:f (f (f y)) = y⊢ f x = y → f y = x
  grindAll goals completed! 🐙

SMT-style tactic: E-matching, congruence closure, case splitting

Good for mathematics, amazing for programming

Sometimes subtle to drive well

Grind Interactive Mode

example (x y : Rat) (_ : x^2 = 1) (_ : x + y = 1) :
    y ≤ 2 := byx:Raty:Ratx✝¹:x ^ 2 = 1x✝:x + y = 1⊢ y ≤ 2
  grindAll goals completed! 🐙`grind` failed
grindx y:Rath:x ^ 2 = 1h_1:x + y = 1h_2:¬y ≤ 2⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x ^ 2 = 1
[prop] x + y = 1
[prop] ¬y ≤ 2
[eqc] False propositions
[prop] y ≤ 2
[eqc] Equivalence classes
[eqc] {1, x + y, x ^ 2}
[ematch] E-matching patterns
[thm] Nat.pow_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[thm] Nat.div_pow_of_pos: [@HPow.hPow `[Nat] `[Nat] `[Nat] `[instHPow] #2 #1]
[linarith] Linarith assignment for `Rat`
[assign] x := -2
[assign] y := 3
[assign] 「x ^ 2」 := 1
[ring] Ring `Rat`
[basis] Basis
[_] y ^ 2 + -2 * y = 0
[_] x + y + -1 = 0

example (x y : Rat) (_ : x^2 = 1) (_ : x + y = 1) :
    y ≤ 2 := byx:Raty:Ratx✝¹:x ^ 2 = 1x✝:x + y = 1⊢ y ≤ 2
  grind =>
    have : x = 1 ∨ x = -1grindx:Raty:Ratx✝¹:x ^ 2 = 1x✝:x + y = 1h✝:¬y ≤ 2this:x = 1 ∨ x = -1⊢ False
    finishAll goals completed! 🐙

Functional induction

def ackermann : (Nat × Nat) → Nat
  | (0, m) => m + 1
  | (n+1, 0) => ackermann (n, 1)
  | (n+1, m+1) => ackermann (n, ackermann (n + 1, m))
termination_by p => p

fun_induction generates induction goals mirroring the recursive structure:

exampledeclaration uses `sorry` : P (ackermann p) := byP:Nat → Propp:Nat × Nat⊢ P (ackermann p)
  fun_induction ackermann p with
  | case1 m =>case1P:Nat → Propm:Nat⊢ P (m + 1) sorryAll goals completed! 🐙
  | case2 n ih =>case2P:Nat → Propn:Natih:P (ackermann (n, 1))⊢ P (ackermann (n, 1)) sorryAll goals completed! 🐙
  | case3 n m ih₁ ih₂ =>case3P:Nat → Propn:Natm:Natih₁:P (ackermann (n + 1, m))ih₂:P (ackermann (n, ackermann (n + 1, m)))⊢ P (ackermann (n, ackermann (n + 1, m))) sorryAll goals completed! 🐙

Std.Do / mvcgen

abbrev TwoBankAccountsM := StateM (Nat × Nat)

def transferFromFirstToSecond (amt : Nat) :
    TwoBankAccountsM Unit := do
  -- Debit first account
  modify (fun (first, second) => (first - amt, second))
  -- Credit second account
  modify (fun (first, second) => (first, second + amt))

theorem transfer_preserves_balance {amt : Nat} {balance : Nat} :
    ⦃fun (accts : Nat × Nat) =>
      ⌜amt ≤ accts.1 ∧ accts.1 + accts.2 = balance⌝⦄
    transferFromFirstToSecond amt
    ⦃⇓ _ (accts : Nat × Nat) =>
      ⌜accts.1 + accts.2 = balance⌝⦄ := byamt:Natbalance:Nat⊢ ⦃fun accts => ⌜amt ≤ accts.fst ∧ accts.fst + accts.snd = balance⌝⦄
  transferFromFirstToSecond amt ⦃PostCond.noThrow fun x accts => ⌜accts.fst + accts.snd = balance⌝⦄
  mvcgen [transferFromFirstToSecond]vc1amt:Natbalance:Nats✝:Nat × Nath✝:amt ≤ s✝.fst ∧ s✝.fst + s✝.snd = balancet✝¹:PUnit × Nat × Nat := (PUnit.unit, s✝.fst - amt, s✝.snd)t✝:Unit × Nat × Nat := (PUnit.unit, t✝¹.snd.fst, t✝¹.snd.snd + amt)⊢ t✝.snd.fst + t✝.snd.snd = balance
  grindAll goals completed! 🐙

Concurrency Primitives

example : IO Unit := do
  let ch ← Std.Channel.new (α := Nat)
    (capacity := (10 : Nat))
  let _ ← ch.send 42
  let task ← ch.recv
  let v := task.get
  IO.println v

Std.Mutex: mutual exclusion guarding shared state
Std.Condvar: condition variable
Std.Channel: multi-producer multi-consumer FIFO
Std.Broadcast: broadcast channel
Std.Barrier: synchronization barrier
Std.CancellationToken: cooperative cancellation

Async I/O

Built on libuv, fully asynchronous:

def listenAndWait : Async Bool := do
  let server ← Socket.Server.mk
  server.listen 128

  let sleep ← Sleep.mk 1000

  Selectable.one #[
    .case server.acceptSelector (fun _ => pure true),
    .case sleep.selector (fun _ => pure false)]

HTTP server & client

Coming soon (PRs in review):

HTTP/1.1 server
HTTP client including TLS support

Date and Time library

#eval"2026-03-11 13:02 → 2026-03-18 13:02" do
  let now ← Timestamp.now
  let rules ← Database.defaultGetZoneRules "Europe/Berlin"
  let berlin := ZonedDateTime.ofTimestamp now rules
  let nextWeek := berlin.addDays 7
  let fmt := "uuuu-MM-dd HH:mm"
  return s!"{berlin.format fmt} → {nextWeek.format fmt}"
"2026-03-11 13:02 → 2026-03-18 13:02"

Iterators

Lazy, composable, provably terminating:

#eval#[20, 40] [1, 2, 3, 4, 5].iter
  |>.filter (· % 2 == 0)
  |>.map (· * 10)
  |>.toArray
#[20, 40]

Combinators: map, filter, filterMap, flatMap, take, ...
Consumers: fold, toArray, toList, count, ...
Iter (pure) and IterM (monadic)
Built-in finiteness tracking for termination proofs

Containers

Verified standard library containers with specification lemmas:

Hash-based: HashMap, HashSet
Tree-based (weight-balanced BSTs): TreeMap, TreeSet

Also: dependent maps, extensional maps and sets, variants suitable for use in nested inductives

def sameChars (s₁ s₂ : String) : Bool :=
  s₁.chars.toHashSet == s₂.chars.toHashSet

theorem sameChars_iff {s₁ s₂ : String} :
    sameChars s₁ s₂ ↔ (∀ c, c ∈ s₁.toList ↔ c ∈ s₂.toList) :=
  ...

Strings

Strings are UTF-8 encoded byte arrays carrying a validity proof
String.Slice: zero-copy view into a string with bounds proofs
Safe character access: no runtime bounds or validity checks needed
Pattern-based API: split, contains, startsWith, ...

-- Uses KMP!
#evaltrue "hello, world!".contains "o, "
true

theorem contains_string_iff {t s : String} :
    s.contains t ↔ t.toList <:+: s.toList :=
  ...