CSLib: The Lean Computer Science Library

Clark W. Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura 0001, Alexandre Rademaker, Sorrachai Yingchareonthawornchai [2026].
In CoRR abs/2602.04846.

Abstract

We introduce CSLib, an open-source framework for proving computer-science-related theorems and writing formally verified code in the Lean proof assistant. CSLib aims to be for computer science what Lean's 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 also played a critical role in the training of AI systems for mathematical reasoning. However, the base of computer science knowledge in Lean is currently quite limited. CSLib will vastly enhance this knowledge base and provide infrastructure for using this knowledge in real-world verification projects. By doing so, CSLib will (1) enable the broad use of Lean in computer science education and research, and (2) facilitate the manual and AI-aided engineering of large-scale formally verified systems.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2602-04846,
  author       = {Clark W. Barrett and
                  Swarat Chaudhuri and
                  Fabrizio Montesi and
                  Jim Grundy and
                  Pushmeet Kohli and
                  Leonardo de Moura and
                  Alexandre Rademaker and
                  Sorrachai Yingchareonthawornchai},
  title        = {CSLib: The Lean Computer Science Library},
  journal      = {CoRR},
  volume       = {abs/2602.04846},
  year         = {2026},
  url          = {https://doi.org/10.48550/arXiv.2602.04846},
  doi          = {10.48550/ARXIV.2602.04846},
  eprinttype   = {arXiv},
  eprint       = {2602.04846},
  timestamp    = {Thu, 19 Mar 2026 09:22:46 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2602-04846.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):