Weekly
News about Lean, the theorem prover and programming language.
Software, hardware, protocols, and cryptography verified with Lean. 32 items, newest first.
Ilya Sergey formalised and proved the correctness of the new borrow checker for Move, a smart contract language deployed on the Sui and Aptos blockchains: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant (Claude Code).
Checked against: proofsandintuitions.net
Santosh Nagarakatte's group built FLoPS, which formalizes the upcoming IEEE-P3109 standard for low-precision floating-point arithmetic in Lean. The work found errors in the draft standard, which were reported to the working group and fixed, and established properties of algorithms such as Fast2Sum in the context of P3109.
Checked against: mathstodon.xyz
LambdaClass described Truth Research ZK, which turns Lean 4 specifications into optimized C and Rust code with formal correctness guarantees, noting one axiom (applyIndex_tensor_eq) needed for the tensor product of permutations. A pull request by Kim Morrison, prepared with Claude Code, proves that axiom as a theorem.
Checked against: amo-lean#2blog.lambdaclass.com
In a February 9, 2026 post, Ilya Sergey walks through modelling, model checking, and proving the Dolev-Strong Floodset consensus protocol in Veil, VERSE lab's auto-active Lean-based verifier for distributed protocols. Veil's model checker Lace explored 54904 states, 362 of them distinct, and caught a deliberately introduced agreement bug.
Checked against: proofsandintuitions.net
In an article, Predictable Machines, Inc. explains why it chose Lean as the foundation for Predictable Code, saying Lean's combination of a programming language and a theorem prover makes it possible to formally verify that AI-generated code stays aligned with specifications as systems evolve.
Checked against: LinkedIn postpredictablemachines.com
Gavin Mendel-Gleason reports that opencode, GPT-5.2 and lean-lsp-mcp produced a provably correct citation streaming program for a RAG answering system in two hours with no interventions. Gavin Mendel-Gleason argues that LLMs increase software generation faster than software understanding, and calls the approach vericoding (vibe-coding using programme verification).
Checked against: LinkedIn post
A Proofs and Intuitions post walks through Velvet, a verifier embedded in Lean as a library and developed by VERSE Lab. Velvet discharges most proof obligations with SMT solvers (such as Z3 and cvc5) and tactics like grind, then leaves the rest for interactive proof. In the example, Claude Code and Harmonic's Aristotle each finished the remaining proof.
Checked against: proofsandintuitions.net
Logical Intelligence posted on X an AI-generated, formally verified compiler from λ-calculus to CPS, written in Lean4. The post explains formal verification as code that comes with a mathematical proof, checked by the computer, that it works correctly in all cases, not just the ones tested.
Checked against: @logic_int on X