Weekly
News about Lean, the theorem prover and programming language.
Software, hardware, protocols, and cryptography verified with Lean. 32 items, newest first.
SymCert, implemented in Lean, builds verified SMT-based analyses of Cedar policies, an open-source authorization language. In the FMCAD 2026 paper, five analyses used in a Cedar analysis service at Amazon Web Services were modeled and proved in one work day, and three extensions for new Cedar features took 4 to 8 days each.
Checked against: paper (pdf)
Flapjack is bringing the Pancake compiler, originally verified in HOL4, and its proofs to Lean, with a path compiling a fragment of Pancake to RISC-V where all stages except parsing and AST conversion have a correctness theorem. A MIPS32 backend targets the Ziren zkVM, but its output has been run only on Ziren's Lean model.
Checked against: flapjack-lang.dev
NASA Jet Propulsion Laboratory's PropertyKindCalculus formalizes René Dybkær's ontology on property, extended with Flater's tracking of kinds of quantities, and is described as the first in which the quantity calculus itself, beyond the taxonomy around it, is a checked artifact. It includes catalogues for eleven of the thirteen ISO/IEC 80000 parts.
Checked against: nasa-jpl/PropertyKindCalculus
Boris Cherny reports that a couple of short prompts to Opus 5.5 produced 16 PRs fixing various bugs and race conditions in the Claude Agent SDK. Boris Cherny also sometimes combines Lean and TLA+ to look for issues around data flow, concurrency, and state management.
Checked against: @bcherny on XLinkedIn post
During an audit of the Miden VM, a zero-knowledge VM with its own assembly language, Trail of Bits had agents build a Lean model of the VM executor, producing 95 correctness proofs covering all binary arithmetic components of the core library. The work identified two subtle bugs that the existing unit test suite did not catch.
Checked against: blog.trailofbits.com
Velvet 2.0 is now based on Lean's most recent verification machinery, is easier to set up and 10x faster, adding exception specs, ghost state and named proof goals. Vermilion, an experimental Lean 4 backend for the Verus Rust verifier, turns each obligation into a Lean theorem checked by the Lean kernel.
Checked against: LinkedIn postilyasergey/vermilion
Chunhao Liao, Hongxu Xu, Xintong Zhou, Yizhou Zhang and Chengnian Sun present Trivet, which verifies or refutes 147 of 148 LLVM transformations, including 60 loop-free transformations with symbolic bitwidths and 27 loop-containing cases. Every successful verdict is checked by the Lean kernel.
Checked against: arXiv:2609.19583
Using Aeneas, which extracts a pure model of Rust code in Lean, a 237 KLOC Lean development establishes safety, panic-freedom, and functional correctness of 16.7 KLOC of Rust, including SHA-3 and ML-KEM ported from C. AI agents autonomously write proofs, which the Lean kernel independently verifies.
Checked against: arXiv:2609.15648
In under two weeks, Certora built an experimental C-to-Lean pipeline and proved that the Clight (CompCert's C intermediate representation) model of zlib's 266-line inflate_table function is memory-safe and terminating. The proof, around 20,000 lines of Lean, was written almost entirely by LLMs, and the Lean kernel checked every step.
Checked against: certora.com
The repository adds passwordless sign-in, SQL migrations, OpenTelemetry traces and logs, an MCP endpoint, and deployment to AWS Lambda, built on Paul Butcher's own Lean libraries. Markup is typed and formally verified (a <div> inside a <p> is a type error), and lean-json is proved correct against the grammar of RFC 8259.
Checked against: paulbutcher/lean-todomvc-max
Predictable Code uses Lean 4 formal verification to prove that AI-generated code matches specifications, and is currently in private beta. Predictable Machines also open-sourced lean4-json-schema, which derives JSON Schemas from types and proves at compile time that serialization always validates, and lean4-tree-sitter, typed bindings for tree-sitter.
Checked against: predictablemachines.comcode.predictablemachines.com
Ziyi Yang, Wenji Fang, Chen Chen, Zhiyao Xie, and Hongce Zhang present CircuitProver, an agentic Lean 4-based verification framework that translates hardware designs and natural language specifications into Lean 4 models and reuses verified lemmas across tasks. Across 63 tasks it proves all benchmarks, while a vanilla agent solves 92.1% of them.
Checked against: arXiv:2607.27259
In a Logos Research prototype, a deterministic translator turns both the original and the rewrite into Lean, and a theorem prover proves the two compute the same result on every input. For iCPPI, a portfolio-insurance algorithm, the machine-checked proof ran to some 22,000 characters, with floats modelled as exact real numbers.
Checked against: logosresearch.ai
ArkLib, a project supported by the Ethereum Foundation, mechanizes the probabilistic security proofs that succinct non-interactive arguments of knowledge (SNARKs) depend on. It gives zk engineers and cryptography researchers machine-checked specifications and executable references for proof systems where a single soundness bug can be catastrophic.
Checked against: lean-lang.org
Peter O'Hearn is hiring a postdoc in the Meta London office who will work closely with Peter O'Hearn and others in the new AI Verification team, collaborating across Meta Superintelligence Labs and possibly building on lean/CSLib, Iris-Lean and loom/velvet.
Checked against: LinkedIn post
Talos provides a Wasm interpreter optimized for reasoning plus a WP calculus layer for proving program properties, with a proof that the num-integer crate's gcd using Stein's algorithm is correct. The early-stage project aims for full Wasm coverage by passing the official testsuite, and verification of any Rust crate that compiles to Wasm.
Checked against: leanprover.zulipchat.com
Jonathan Protzenko's case study uses Aeneas, a toolchain for verifying Rust programs through a functional translation to Lean, on jxl-rs, a Rust rewrite of the jpeg-xl codec. The proof shows an unchecked array access always stays within bounds and showcases recent Aeneas features, including official grind support and loop combinators.
Checked against: jonathan.protzenko.fr
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
s2n-bignum is a collection of integer arithmetic routines in pure machine code for cryptographic applications, and each function ships with a machine-checked proof in HOL Light. The CSLib Community port, presented at INRIA Paris 2026, covers the ARM (aarch64) part first, with the first two tutorials completed.
Checked against: arademaker.github.ioatlas-computing-org/bignum
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.iobeneficialaifoundation.org
The Beneficial AI Foundation is verifying the Signal protocol and its Rust implementation in Lean, a public project meant to show that formal verification of major applications is doable today. The plan proves security properties of a protocol model, then uses the Aeneas tool to translate Signal's Rust code to Lean and check it against that model.
Checked against: beneficialaifoundation.org
Lean Squad, a GitHub Agentic Workflow, proved 443 theorems for raft-rs with three human nudge comments for about $240, and 518 theorems for Cloudflare's quiche, where it found an Ord antisymmetry violation. It also proved 259 theorems for PX4-Autopilot and found 2 bugs. Every definition and theorem statement is AI written.
Checked against: dsyme.net
Veil is an open-source multi-modal verification framework for distributed protocols, embedded in Lean. It combines symbolic and concrete model checking, SMT-based automated proofs, and interactive theorem proving in a single tool with foundational guarantees and in-editor feedback.
Checked against: lean-lang.org
CatCrypt provides a pipeline from Rust reference implementations, translated with the Hax tool, to security proofs in Lean, covering 172 cryptographic protocols and constructions (110 with the full Rust-to-Lean pipeline). Bas Spitters developed the whole library in two months working with GenAI.
Checked against: eprint.iacr.org