Week of Apr 30, 2026

Edition 14: 13 items published for Apr 23 to Apr 30, 2026.

Leo de Moura presents scalable software verification in Lean at SViL 2026

At SViL 2026 at INRIA Paris on April 20, 2026, Leo de Moura presented SymM, a monad for symbolic simulation and VC generation (turning code and specifications into proof obligations). On one challenge it ran about 100× faster than MetaM, and a Velvet port beat Dafny on 24 of 27 benchmarks.

Checked against: leodemoura.github.io

Verification Apr 20

Signal Shot launches to formally verify the Signal protocol and app in Lean

The Beneficial AI Foundation, Signal, and the Lean FRO launched Signal Shot on April 20, 2026, at the Software Verification in Lean workshop in Paris, with a talk by Max Tegmark and others. Leo de Moura writes that the effort targets libsignal's Rust implementation, translated to Lean with Aeneas, Son Ho's Rust-to-Lean functional translator.

Checked against: leodemoura.github.io beneficialaifoundation.org

AI and formalization Apr 25

Sidharth Hariharan, Maryna Viazovska and coauthors report on formalizing 8-dimensional sphere packing

The paper describes how Maryna Viazovska's 2016 solution of the sphere packing problem in dimension 8 was formally verified in Lean in February 2026, with the final stages done by Math, Inc.'s autoformalization model Gauss. It discusses the techniques used, the collaboration between humans and Gauss, and remaining project objectives.

First page of the paper — Image: paperswithlean.com

Checked against: arXiv:2604.23468

AI and formalization Apr 23

Alex Meiburg shares Aristotle-authored Z80 emulator with verified assembly GCD

Alex Meiburg asked Aristotle to formalize a Z80 emulator, build an assembler, and write a BigNum GCD in about 80 assembly instructions, then verify it by modeling the whole CPU execution. After 14 rounds of submitting to Aristotle (without editing the prompt), the proof succeeded.

Checked against: leanprover.zulipchat.com

Verification Apr 30

Mark Ruvald Pedersen releases Clift, an AutoCorres-style C verification pipeline for Lean 4

Clift verifies C programs by lifting them into Lean 4, following the methodology pioneered by seL4's AutoCorres pipeline in Isabelle/HOL and adapting AutoCorres2's five-stage pipeline to Lean 4's type theory. The accompanying paper reports that Claude Opus 4.6 generated the vast majority of the code, with 1,698 theorems and 12 remaining sorry.

Checked against: paper (pdf)eisbaw/Clift

Lean core Apr 29

Leo de Moura merges grind diagnostics, solver fixes, and a ring-degree limit

The new grind.ematch.diagnostics option tracks how E-matching theorem instances depend on each other, and a ringMaxDegree option (default 1024) bounds polynomial degree in the grind ring solver. Other merged pull requests fix beta reduction to respect the generation threshold, fix a kernel error for Nat casts to non-Int types, and extend the homomorphism demo.

Checked against: lean4#13558 lean4#13585 lean4#13560 lean4#13453 lean4#13532 lean4#13520

Lean core Apr 30

Joachim Breitner's experimental nanobruijn kernel type-checks all of Mathlib

nanobruijn, an experimental Lean 4 type checker in Rust forked from nanoda_lib, keeps expressions as pure de Bruijn indices with shift-homomorphic caching, and type-checks all of Mathlib (670k declarations) with 0 errors and 0 timeouts. The code changes were written by Claude (Anthropic), directed by Joachim Breitner.

Checked against: nomeata/nanobruijn

Lean core Apr 22

Lake gains builtin environment linting through new lake lint flags

A pull request by Wojciech Różowski, merged on 2026-04-22, adds builtin environment linting support to Lake, accessible via lake lint flags such as --builtin-lint and --clippy. It also introduces two builtin linters upstreamed from Mathlib (defLemma and checkUnivs) and a builtinLint package configuration option.

Checked against: lean4#13431

Lean core Apr 19

Leo de Moura merges fixes for Lean's Sym framework and sym => mode

The pull requests fix a bug where satellite solvers (lia, ring, linarith) in sym => interactive mode threw an internal error, prune goals assigned by isDefEq, stop Sym.intros from assigning a metavariable when it introduces no binders, and restore eta-reduction of Sym.simp patterns containing loose pattern variables.

Checked against: lean4#13472 lean4#13474 lean4#13451 lean4#13448 lean4#13452

Lean core Apr 30

David Thrane Christiansen adds a full-page search to Verso

A merged pull request by David Thrane Christiansen adds a full-page search to Verso, accessed by pressing enter in the search field. The page shows more results, provides more context, and has more filtering features.

Checked against: verso#847

Lean core Apr 15

vscode-lean4 adds picker-based input method for Unicode abbreviations

A merged pull request by Marc Huisinga adds three commands (Find, Copy, and Insert Unicode Symbol) that search symbols by abbreviation or by symbol, making it easier to insert Unicode into non-editor dialogs. Copy and Insert are bound to Ctrl+Alt+\ depending on whether a text editor is focused.

Checked against: vscode-lean4#762

Papers and events Apr 30

Stanford hosted the Future of Mathematics Symposium on AI and formal methods

The symposium, held May 1-2, 2026, opened with Leo de Moura of Amazon speaking on "Machine-Checked Mathematics in the Age of AI." Other talks included Clark Barrett on CSLib, a platform for AI-assisted formal verification in Lean, Kevin Buzzard on autoformalisation, and Maryna Viazovska on formalizing the sphere packing problem.

Checked against: events.stanford.edu

Papers and events Mar 18

Leo de Moura surveys industrial and AI uses of Lean at ETAPS 2026

Leo de Moura gave an ETAPS tutorial on April 13, 2026, then an ETAPS Industry Day talk on April 15 covering Cedar (access control), SampCert (privacy), Strata (languages), Waimea (compiler), SymCrypt (crypto), Anneal (unsafe Rust) and Veil (distributed protocols), plus AI provers for which Lean is the training environment, evaluation harness, and deployment target.

Checked against: leodemoura.github.io