An open-source library of reusable components for proving theorems in computer science and writing formally verified code in the Lean programming language and proof assistant.

Why CSLib

  • Formalized foundations of computer science
    Computational models, complexity, and core theory across many areas of CS.
  • A toolkit for reasoning about programs
    Verify properties of your code, building on decades of deductive verification.
  • A repository of verified algorithms and data structures
    Reusable, machine-checked implementations you can build on.
  • A foundation for trustworthy AI
    A shared vocabulary to train models on.
Sponsors and Partners