About

Computer science research is undergoing a transformation that mathematics has already begun to experience. Once a niche pursuit, formal verification is now a practical tool for building software and systems with real correctness and security guarantees, and a natural substrate for trustworthy AI systems that reason about code.

At the heart of this effort is CSLib, an open-source library of reusable components for proving theorems in computer science and writing formally verified code in the Lean proof assistant. CSLib aims to be for computer science what Mathlib is for mathematics. Mathlib has been tremendously impactful: it is a key reason for Lean's popularity within the mathematics research community, and it has played a critical role in training AI systems for mathematical reasoning. The foundation of computer science knowledge in Lean, however, remains quite limited. CSLib is a focused effort to change that — vastly expanding the range of computer science results formalized in Lean and, at the same time, building the infrastructure needed to put these results to work in real-world verification projects. In doing so, CSLib aims to enable the broad use of formal methods in computer science education and research, and facilitate the manual and AI-aided engineering of large-scale, formally verified systems.

What This Enables

A stronger computer science library in Lean means researchers and students can build on verified foundations rather than reinvent them — models of computation, programming language semantics, algorithms, and data structures, all mechanically verified. It means software and protocols can be built with machine-checked correctness and security guarantees. And it means trustworthy AI systems have a much richer substrate of formalized computer science knowledge to train on and reason over, the same role Mathlib has played for AI-assisted mathematics.

Learn more about our roadmap, how to contribute, our governance, or explore our learning resources.

With Openness and Intent

CSLib is a global, open source effort: available to everyone, and open to contributions from anyone. It is made possible by its many contributors and strategic organizations that support us.

We are deeply grateful to all our contributors, as well as our partners and sponsors, who support strategic projects and shared infrastructure for the growth of the project.