Software Verification in Lean (SVIL) comes to Stanford University on Saturday, November 7. Co-organized by Beneficial AI Foundation and Lean FRO, it is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end verification of security-critical systems. Talks will cover Rust verification with the Aeneas framework, low-level software verification, and formally verified OS kernels. Speakers include Max Tegmark, Shaowei Lin, Leonardo de Moura, Jonathan Protzenko, Andres Erbsen, and Mike Dodds. In-person space is limited. Non-local and waitlisted registrants will receive a livestream link, and recordings will be available afterward. Program and registration:

@AnthropicAI has shared the first end-to-end, computer-checked proof of Fermat's Last Theorem: 13 million lines of Lean, 29,500 intermediate theorems. Their announcement calls it "the largest Lean proof ever constructed." See also Kevin Buzzard's blog post about the proof: 🔗 Anthropic's announce post: 🔗 The code: #LeanLang# #LeanProver# #FLT#

The Beneficial AI Foundation asks: "Can we prove that Signal's cryptography is secure — not just on paper, but in actual code?" Signal Shot, launched today in Paris, is a public moonshot to formally verify the Signal protocol and its Rust implementation using Lean. Open to contributions! 🔗 #leanlang# #leanprover# #softwareverification# #baif# #signal#