CSLib: Lean’s Formal Software Foundation
Bottom line up front: If you love Lean and care about software, you’re likely to be excited about the progress on CSLib and might be interested in contributing to one of these two tracks present below.
If you’re reading this, you’re likely already familiar with Lean (the programming language and proof-assistant that’s steadily gaining notability for its use by mathematicians like Terry Tao and AI-for-math efforts like Google DeepMind’s DeepThink). There’s incredible value in using a computer to rigorously and automatically check the correctness of the mathematical proof for a theorem: you don’t have to either trust that the proof is correct or understand and verify every line yourself before you can use the theorem in your own proofs. And you could imagine wanting to rigorously verify software properties as well.
To prove theorems about mathematics, Lean starts from axioms, foundational and widely agreed upon truths, that are combined with formal logic. In software, axioms might take the form of formalizations of programming languages or functional descriptions of how compilers and operating systems behave. If we start from precise, logical definitions, we can prove properties about real code with the same rigor mathematicians use for theorems.
This matters because once you formalize these foundations, you can prove useful things about software. This is already commonly used in high-assurance software (e.g., proving that a cryptography library implements a particular function correctly, or that a microkernel provides guaranteed isolation between processes). However, many of these proof systems were designed for specific verification tasks at a time when the skills, expertise, and cost of generating specifications and proofs were very high. Now that we have a clear line of sight to a future in which the cost of generating proofs and code is very low, it is more important than ever to build a general foundation for proving software properties. This will enable us to compose different properties of subsystems to prove properties of overarching systems. (Imagine being able to easily and confidently reason about privacy guarantees, worst-case runtime bounds, or memory safety for your entire system because every library you import came with such guaranteed assurances.)
This is the long-term promise of CSLib, a new project and library in Lean 4, setting out to build verified foundations that connect high-level CS theory to low-level executable code. At Atlas Computing, we’re proud to host Alexandre Rademaker, one of CSLib’s tech leads, as we see this work as fundamental to building robust software systems. Feel free to check out cslib.io for documentation, or the CSLib roadmap for the full technical vision and where different pieces fit together.
More than an analog of MathLib
Lean has been transformative for mathematics, and Mathlib (the home of the various definitions and proven theorems in Lean) has led to an ecosystem where mathematicians can formalize proofs, build on each other’s work, and verify results with unprecedented rigor. But proving things about software is very different from proving things about math; for example, I’ve yet to meet a mathematician who cares about the performance of their proofs, or a computer scientist who doesn’t care about the performance of their code.
CSLib has two complementary pillars:
Formalizing core CS concepts directly in Lean, like models of computation, algorithms, data structures, and their properties
Building an infrastructure for Lean-based reasoning about everyday imperative code.
Together, these enable proving properties about real software using the theoretical foundations from the first pillar.
This is infrastructure work, and we need a community to help us formalize this computer science. Just as MathLib is building a community and working toward formalizing all sufficiently important theorems in mathematics, CSLib is building a community to formalize the undergraduate CS curriculum and eventually provide strong assurances about (eventually all) sufficiently important software. This will start with developing and building consensus around a set of design choices that the AI-for-software and AI-for-math communities are ready to build on.
Two Ways to Contribute
If you find yourself with some time over the holidays and have a fondness for Lean, here are two active tracks where I hear that CSLib would love some contributions:
Track 1: Formalizing CS Foundations, algorithms, and data structures
The current effort can be seen here, but will eventually include everything from cryptography and complexity theory. If you want to contribute, read the contributing guidelines and familiarize yourself with the repository structure.
Track 2: Verifying Low-Level Code
At Atlas, Alex is porting AWS’s s2n-bignum library to Lean. s2n-bignum provides cryptographic integer arithmetic routines in pure assembly (x86_64 and ARM), each with machine-checked formal proofs in HOL Light. Our goal is to bring these verified implementations to Lean’s ecosystem. The first ARM assembly proof has been completed and is available at github.com/atlas-computing-org/bignum. Near-term priorities include expanding the executable ARM model, completing Mach-O binary parsing, and implementing decision procedures for bit-vectors. The bignum project will serve as an early CSLib consumer, demonstrating how verified low-level code can leverage CSLib’s foundations. We expect to reuse general-purpose definitions and theorems from CSLib throughout the bignum proofs, creating a practical feedback loop that helps shape CSLib’s development.
If you’re looking for a place to ask questions, check out the website and the Zulip community forum.
Why It Matters
The connection between these two tracks might not be evident at first. But consider: you’re simultaneously building the theoretical vocabulary (graphs, complexity, algorithms) and the verified compilation path (starting with proven arithmetic primitives). When both exist, you can finally do something remarkable: prove properties about real systems, from algorithm choice down to machine instructions.
This is how we get to a world where:
Compilers come with correctness guarantees
Operating system kernels have verified security properties
Algorithm implementations carry proven complexity bounds
Software infrastructure is trustworthy by construction
CSLib is seeding this ecosystem. It’s early enough that your contributions will shape the whole trajectory.