Week of Apr 23, 2026

Edition 13: 5 items published for Apr 16 to Apr 23, 2026.

Beneficial AI Foundation launches Signal Shot to verify Signal in Lean

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

Verification Apr 20

Dsyme's Lean Squad workflow applies Lean 4 verification to three codebases

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

AI and formalization Apr 21

New arXiv papers test LLM formalization faithfulness, agents, and benchmarks in Lean

Kyuhee Kim, Auguste Poiroux and Antoine Bosselut evaluate GPT-5 and DeepSeek-R1 on 303 first-order logic problems: GPT-5 fabricates axioms during proof generation, while DeepSeek-R1 mistranslates premises. Other papers introduce PRIME, a benchmark of 156 theorems annotated in Lean 4, analyze tool-augmented formalization agents, and formalize the Wu-Ritt characteristic set method.

First page of the paper — Image: paperswithlean.com

Checked against: arXiv:2604.19459 arXiv:2604.19000 arXiv:2604.16538 arXiv:2604.14912 arXiv:2604.18882

Verification Apr 23

Alexandre Rademaker presents a port of AWS's s2n-bignum to Lean 4

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.io atlas-computing-org/bignum

Papers and events Apr 20

Software Verification in Lean 2026 workshop recordings now available

Talks from the one-day workshop at INRIA Paris on April 20, 2026 are on YouTube, including a talk presenting SymM, a new monadic framework for high-performance verification tools built on Lean, Son Ho on SymCrypt, and Karthikeyan Bhargavan on verifying cryptographic applications. Derek Sorensen's talk was not recorded, and slides were provided instead.

Checked against: beneficial-ai-foundation.github.io leodemoura.github.io