Software Development
Redmond, WA 6,591 followers
Supporting the Formal Mathematics revolution
About us
Lean FRO is a nonprofit dedicated to advancing the Formal Mathematics revolution. The FRO’s purpose is to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant. Our 5-year mission is to empower Lean towards self-sustainability.
- Industry
- Software Development
- Company size
- 11-50 employees
- Headquarters
- Redmond, WA
- Type
- Nonprofit
- Founded
- 2023
Locations
Employees at Lean FRO
Updates
-
Lean FRO reposted this
Vero: Can AI agents build formally verified software repositories? We built a benchmark to find out. The short answer: not yet. AI agents write more and more of our code, but unit tests and review cannot rule out edge-case bugs. Formal verification can: a machine-checked proof that an implementation satisfies its specification eliminates, for all inputs, every class of bug the specification captures. And the software where this matters most, OS kernels, cryptographic protocols, distributed systems, lives in multi-module repositories, not standalone functions. Today we are releasing Vero, the first benchmark for joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module Lean 4 projects curated from real-world repositories in Python, Dafny, Verus, and Coq: 743 APIs and 2,705 formal specifications spanning cryptographic protocols, smart contracts, distributed systems, and core data structures. Agents must implement every API and produce machine-checked Lean 4 proofs that their code satisfies every specification. What we found: • Vero is challenging for the frontier models. The strongest configuration (GPT-5.5 at xhigh reasoning) fully verifies only 27 of 43 repositories, and 10 repositories remain unsolved across every configuration we tested. • The bottleneck is not local proof skill. The best agent passes 87% of individual specifications. What separates full solves is repository-scale organization: discovering shared invariants and building reusable lemma libraries. In successful runs, roughly 74% of proof lines live in helper lemmas shared across specifications. • Implementation freedom cuts both ways. Agents sometimes replace hard-to-verify algorithms with simpler, provable ones. But when proofs stall, they grind on proofs rather than refactoring the code into a more provable form. Vero also introduces a formal audit mechanism: agents can submit machine-checked proofs that a specification is unsatisfiable or a reference implementation is incorrect. Benchmark defects become correctable findings backed by formal evidence instead of silent penalties on capable agents. The benchmark, curation pipeline, and evaluation harness are open source. Paper: https://lnkd.in/gbdswiWF Code: https://lnkd.in/gfPWiuG3
-
Lean FRO reposted this
SAIR's next competition has arrived: the Lean Kernel Challenge. We're bringing the community together to improve the performance of verified computation in the Lean 4 kernel—the trusted component that checks every proof accepted by Lean. The competition is co-organized by Lean FRO and the SAIR Foundation. Organizing Committee: Joachim Breitner, Leonardo de Moura, Kim Morrison, and Terence Tao. The Lean Kernel Challenge invites participants to submit optimized implementations with machine-checked proofs of correctness. After the evaluation phase, all results and benchmark data will be released under an open-source license as a collective contribution to Lean's development. Stage 1 pre-registration is now open. The competition officially launches on September 15, 2026. Learn more and pre-register: https://lnkd.in/gMDGrWeg #SAIR #Lean4 #FormalVerification
Lean Kernel Challenge - Stage 1 | SAIR Foundation competition.sair.foundation -
Lean FRO reposted this
I'm looking forward to this one! Come talk to me and we'll get all of PDEs done in Tau Ceti. :-) https://lnkd.in/evNTSDSx
Register for "Frontier of PDE Formalization and Analysis with AI", taking place December 7-8, 2026 in Berkeley, CA and online. Limited funding for in-person participation is available for early-career mathematicians, including graduate students, who register early (by Oct. 15): https://lnkd.in/eCbAFepq. This workshop is supported by the AI for Math Fund. The formalization of mathematics is undergoing a quiet revolution. Computational proof assistants like Lean now make it possible to build verified, machine-checkable libraries of mathematics at scale, and the frontier of partial differential equations (PDEs) stands as one of the most profound and underexplored territories in this landscape. At the same time, large language models and AI for mathematics (AI4Math) are beginning to reshape how researchers discover, conjecture, and verify mathematical results. This workshop brings together three communities — PDE analysts, Lean/Mathlib developers, and AI/AI4Math researchers from both academia and industry — to chart a shared path forward. Our central aim is to produce a clear, community-endorsed roadmap (1-year, 3-year, and 5-year horizons) for the formalization and AI-assisted analysis of PDEs, spanning undergraduate and graduate textbook material through to active research frontiers. We will identify the PDE topics most ripe for formalization in Mathlib, the AI tools best positioned to accelerate that work, and the collaborative structures needed to sustain long-term progress. Organizers: Wuyang Chen, Simon Fraser University; Patrick Shafto, Rutgers University; Weiran Sun, Simon Fraser University Audience: SLMath members in residence and interested mathematicians, Lean/mathlib enthusiasts, AI researchers, including graduate students and researchers in academia and industry. You may consider bringing your PC as this event might involve hands-on coding sessions, but this is not required. Some familiarity with Lean will be helpful.
-
The Lean FRO Year 4 Part 1 roadmap, covering September 2026 through February 2027, is now published. It sets out our priorities for Lean and ecosystem support for the first half of our fourth year of operations. 🔗 Read the full roadmap here: https://lnkd.in/gsSfs-b5 #LeanLang #LeanProver
-
Lean FRO reposted this
Everyone says vibe coding is ready for real software. But would you ship code whose correctness has never been verified? Would you maintain code that no one can maintain? 1. Our workshop CFP is now open at NeurIPS 2026: “AI for Verifiable Coding” (Atlanta, Dec. 12th): neuro-symbolic agents working with proof assistants, model checkers, and compiler feedback, specification generation, proof engineering, program verification, verified AI systems, and benchmarks for real deployments. Speakers and panelists span both academia and industry. 2. We are also thrilled to announce a competition track with prizes: Lean proof refactoring! Frontier models write proofs that compile, but real projects live with their proofs for years, and refactoring is inherently multi-objective: proof length, compilation cost, and cross-version compatibility, along with the trade-offs among them, are largely ignored today. This open-arena leaderboard is a joint effort with Amazon, UT Austin, and popular Lean repos such as CSLib, Physlib, and ArkLib. 3. Cash prizes! We will award cash prizes to the winner and runner-up in both the paper track and the competition track. Our sponsor lineup is being finalized, with more to come, so stay tuned! 4. Deadlines (AoE): - [Paper Track] Abstract: Sep. 11 | Paper: Sep. 13 | Decision: Sep. 29 | Camera-ready: Oct. 14 - [Competition Track] Warm-up test now open | Final Submission: Oct. 1 - Nov. 8 | Announcement: Nov. 22 - Website: https://lnkd.in/ge8cMkNr - OpenReview (Paper Track): https://lnkd.in/g2UeNsrh - OpenReview (Competition Track): https://lnkd.in/gwb_Rz8n - Reviewer's Self-Nomination Form: https://lnkd.in/g5QZKR9x Huge thanks to organizers across SFU, AWS, Korea U, UC Berkeley, MIT, USC, Microsoft, Oxford! Soonho Kong Hakjoo Oh Jingxuan He Jacqueline Mitchell Amanda Liu Zhe Ye Xiaodong Liu Varun Pant Simon Frieder Jialin Lu #NeurIPS2026 · #MachineLearning · #AI · #FormalMethods · #ProgramVerification · #LeanProver · #TheoremProving · #ProofAssistant · #AI4Math · #NeuroSymbolic · #SoftwareVerification · #VibeCoding · #CallForPapers · #CFP · #Competition
VeriCodeGen: AI for Verifiable Coding — NeurIPS 2026 Workshop vericodegen.github.io -
Lean FRO reposted this
Today we're launching the Palomar Registry https://lnkd.in/enMR4mJV, an index of formalized mathematics repositories with a valid comparator setup and formalization.yaml metadata. Limited automatic review rejects submissions with obvious discrepancies between the informal and formal statements, and errors in the metadata. This is jointly incubated by the Lean FRO and the Institute for Computer-Aided Reasoning in Mathematics - ICARM, and the initial advisory board consists of Jeremy Avigad, Matthew Ballard, Jaume de Dios Pont, Nestor Guillen, Bryna Kra, myself, Terence Tao, Ravi Vakil, and Akshay Venkatesh. Please read our Palomar Statement (https://lnkd.in/ex32Zmxr), explaining the motivation behind this registry, and our About page (https://lnkd.in/exkcuggd) to understand the mechanism. Terry has also written about Palomar on his blog https://lnkd.in/e6euYfrS. Palomar doesn't have any opinions about use of AI: there are already entries ranging from no-AI-at-all to autonomously formalized. What we do expect is that this is explained clearly in your formalization.yaml file. If you have a repository with at least one of a comparator setup or a formalization.yaml metadata, we'd encourage you to fulfill the requirements and submit. You can find detailed instructions at https://lnkd.in/ej4WAdnQ, or just get started at https://lnkd.in/eY-hpiJD (it's a fairly interactive process that should help you identify problems with your submission: bug reports are very welcome). (There's also an llms.txt (https://lnkd.in/eAPjQjXC) if you'd like to have an agent help you submit.)
-
Lean FRO reposted this
Excited to announce the launch of the CSLib Initiative! This will do for CS what Mathlib is doing for math, and enable formal verification of software. Thanks to Coefficient Giving for their support. This builds on Renaissance Philanthropy's support for the Mathlib Initiative and the AI for Math Fund (backed by Alexander Gerko and XTX Markets) and Convergent Research's support for the Lean FRO. We have also received great proposals to (1) formalize open source software and libraries, (2) develop better benchmarks for formally verified code generation; (3) formalize other fields such as physics and quantum computing; (4) leverage formal verification for technical approaches to AI safety.
We're delighted to announce the launch of CSLib Initiative, a new fund at Renaissance Philanthropy. CSLib is an open-source framework for formalizing computer-science theory and writing formally verified code in Lean, an open-source proof assistant. The base of computer-science knowledge formalized in Lean remains limited; CSLib is designed to close that gap. By providing a shared foundation of definitions, theorems, and reusable components, CSLib enables researchers to build on one another’s work rather than repeatedly starting from scratch. In doing so, it also creates a growing body of verified knowledge that future AI systems can use to reason about software. This is becoming increasingly important as AI dramatically lowers the cost of developing formally verified software. Formal verification can make software more reliable and resilient to cyberattacks — and, in turn, provide stronger foundations for building AI systems we can trust. The CSLib Initiative, led by Alexandre Rademaker, is launching to provide ongoing support for the CSLib project to help the open-source community grow. It has been made possible by a founding grant from Coefficient Giving. Since launching in June 2025, CSLib’s 47 contributors have submitted 453 merged pull requests across 529 commits, producing 164 Lean files and 21,704 lines of verified code — including 1,570 machine-checked theorems and lemmas and 805 definitions and constructions. As Fabrizio Montesi, Director and Professor at the Centre for Formal Methods and Future Computing, Syddansk Universitet - University of Southern Denmark, says: “CSLib is an enormously ambitious project that aims to catalyse a revolution in computer programming and research: to make formal methods applicable at planetary scale and provide the bedrock for building digital systems we can trust.” Read more in Tom Kalil’s Q&A with Alexandre here: https://lnkd.in/e-5aRakg Get in touch at info@renphil.org
-
Lean FRO reposted this
🎉 Great news for the future of AI and software! 🎉 Renaissance Philanthropy launches the CSLib Initiative, a new fund to support the development of CSLib (cslib.io), established with an investment from Coefficient Giving. The fund works in close collaboration with CSLib's governance by means of an advisory board, where I have the pleasure to serve with Clark Barrett, Swarat Chaudhuri, Jim Grundy, Pushmeet Kohli, and Leonardo de Moura. We're also extremely lucky to have secured a great Director in Alexandre Rademaker! Looking forward to a great collaboration. A big thank you to Tom Kalil at Renaissance Philanthropy for his support and making this possible. #CSLib #FormalMethods Lean FRO Centre for Formal Methods and Future Computing (FORM) Danish Institute for Advanced Study (DIAS) Department of Mathematics and Computer Science (IMADA), University of Southern Denmark (SDU)
We're delighted to announce the launch of CSLib Initiative, a new fund at Renaissance Philanthropy. CSLib is an open-source framework for formalizing computer-science theory and writing formally verified code in Lean, an open-source proof assistant. The base of computer-science knowledge formalized in Lean remains limited; CSLib is designed to close that gap. By providing a shared foundation of definitions, theorems, and reusable components, CSLib enables researchers to build on one another’s work rather than repeatedly starting from scratch. In doing so, it also creates a growing body of verified knowledge that future AI systems can use to reason about software. This is becoming increasingly important as AI dramatically lowers the cost of developing formally verified software. Formal verification can make software more reliable and resilient to cyberattacks — and, in turn, provide stronger foundations for building AI systems we can trust. The CSLib Initiative, led by Alexandre Rademaker, is launching to provide ongoing support for the CSLib project to help the open-source community grow. It has been made possible by a founding grant from Coefficient Giving. Since launching in June 2025, CSLib’s 47 contributors have submitted 453 merged pull requests across 529 commits, producing 164 Lean files and 21,704 lines of verified code — including 1,570 machine-checked theorems and lemmas and 805 definitions and constructions. As Fabrizio Montesi, Director and Professor at the Centre for Formal Methods and Future Computing, Syddansk Universitet - University of Southern Denmark, says: “CSLib is an enormously ambitious project that aims to catalyse a revolution in computer programming and research: to make formal methods applicable at planetary scale and provide the bedrock for building digital systems we can trust.” Read more in Tom Kalil’s Q&A with Alexandre here: https://lnkd.in/e-5aRakg Get in touch at info@renphil.org
-
Fantastic news for the Lean ecosystem! We're thrilled that CSLib is to be supported by Renaissance Philanthropy. Congrats to Alexandre Rademaker, Fabrizio Montesi and all CSLib contributors!
We're delighted to announce the launch of CSLib Initiative, a new fund at Renaissance Philanthropy. CSLib is an open-source framework for formalizing computer-science theory and writing formally verified code in Lean, an open-source proof assistant. The base of computer-science knowledge formalized in Lean remains limited; CSLib is designed to close that gap. By providing a shared foundation of definitions, theorems, and reusable components, CSLib enables researchers to build on one another’s work rather than repeatedly starting from scratch. In doing so, it also creates a growing body of verified knowledge that future AI systems can use to reason about software. This is becoming increasingly important as AI dramatically lowers the cost of developing formally verified software. Formal verification can make software more reliable and resilient to cyberattacks — and, in turn, provide stronger foundations for building AI systems we can trust. The CSLib Initiative, led by Alexandre Rademaker, is launching to provide ongoing support for the CSLib project to help the open-source community grow. It has been made possible by a founding grant from Coefficient Giving. Since launching in June 2025, CSLib’s 47 contributors have submitted 453 merged pull requests across 529 commits, producing 164 Lean files and 21,704 lines of verified code — including 1,570 machine-checked theorems and lemmas and 805 definitions and constructions. As Fabrizio Montesi, Director and Professor at the Centre for Formal Methods and Future Computing, Syddansk Universitet - University of Southern Denmark, says: “CSLib is an enormously ambitious project that aims to catalyse a revolution in computer programming and research: to make formal methods applicable at planetary scale and provide the bedrock for building digital systems we can trust.” Read more in Tom Kalil’s Q&A with Alexandre here: https://lnkd.in/e-5aRakg Get in touch at info@renphil.org