Source-linked AI summary
CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai
TL;DR
Computer science lacks a Mathlib-like repository of formalized knowledge and infrastructure for broad Lean-based verification. CSLib addresses this gap through two pillars: formalized computer-science concepts and Boole-based reasoning about imperative code. The framework is intended to support reliable systems, computer-science research, and AI-assisted formalization, while recognizing limitations in its current approaches and managing AI risks through review.
Problem
Computer science has no universal repository of formalized knowledge comparable to Mathlib, limiting Lean-based formal verification and research infrastructure.
Method
CSLib combines formalized computer-science concepts with Boole infrastructure that generates Lean verification conditions and supports verified implementations.
Results
CSLib provides a Lean-based medium for mathematically grounded computer-science research and development, including verification of Boole-language programs.
Takeaways & Limitations
CSLib is intended to reduce verification costs, support researchers and engineers, and enable formalization and proof workflows involving AI.
Takeaways & Limitations
The current complexity API relies on manual tick annotations and cannot directly prove lower-bound statements, while AI-generated formalizations may be buggy or incomprehensible.
Abstract
from arXiv · showhide
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.
1 Introduction
CSLib proposes a Mathlib-like repository for formalized computer-science knowledge in Lean, paired with infrastructure for verifying everyday imperative code. It is intended to address the cost of formal verification while supporting reliable systems, scalable research, and AI-assisted formalization.
- CSLib addresses the absence of a universal repository of formalized computer-science knowledge comparable to Mathlib.
- Its first pillar formalizes computation models, algorithms, data structures, concurrency, programming-language foundations, and relevant mathematics with correctness and complexity proofs.
- Its second pillar provides Boole, verification-condition generation, and verified implementations for reasoning about everyday imperative code.
- CSLib connects Lean proofs to practical development by envisioning translations from mainstream languages such as Rust and C++ into Boole.
- The vision targets reliable and secure systems, broader computer-science research, and AI systems trained on high-quality formalization and proof data.
2 Technical Approach
CSLib’s technical approach has two pillars: a unified Lean formalization of computer-science knowledge and infrastructure for verifying everyday imperative code. The framework combines models, algorithms, complexity analysis, and Boole-based verification workflows.
- Pillar 1: Formalizing Computer Science in Lean: CSLib’s first pillar develops a coherent Lean framework covering models of computation, algorithms, data structures, properties, and proofs.The formalizations are intended to integrate related concepts rather than remain isolated modules.
- Models & Logics: A key goal is to unify formalized models and logics spanning deterministic, probabilistic, quantum, functional, online, interactive, decision, and approximate optimization computation.The planned scope includes specification notations such as temporal, Hoare, separation, and linear logic.
- Models & Logics: Transition systems and bisimulations illustrate CSLib’s target formalizations, supporting theoretical and practical reasoning across hardware design, control, and machine learning.The examples include Lean definitions and associated theorems for a classic stateful-system model and a notion of state equivalence.
- Algorithms & Data Structures: Pillar 1 aims to provide a comprehensive repository of formally verified algorithms and data structures, including complexity analysis for algorithms encountered by computer-science graduates.The long-term ambition is broader coverage of computer science, while the medium-term target focuses on standard graduate-level material.
- Algorithms & Data Structures: The proposed TimeM API packages procedure outputs with computational costs, letting composition add costs while separating correctness from complexity analysis.The API uses ret, bind, and tick, with ✓ as notation for tick; Mergesort demonstrates returning a sorted list together with its cost.
- Algorithms & Data Structures: The lightweight complexity API requires manual tick annotations and cannot directly prove lower-bound claims, motivating future RAM- and query-model methods.Despite these limitations, the paper presents it as a starting point for proving interesting complexity theorems.
- Pillar 2: Infrastructure for Reasoning about Everyday Code: The second pillar connects Lean-based reasoning to mainstream imperative code through Boole, Lean specifications, verification-condition generation, and certified implementations.Boole is an intermediate language whose programs can include preconditions, loop invariants, and assertions; the planned library will make certified code freely available.
3 The Role of AI
CSLib is motivated by AI-related software risks and aims to strengthen both formal verification and AI-assisted theorem proving. It expands Lean’s computer-science abstractions while using AI-generated formalizations as training data and applying human review to manage risks.
- CSLib responds to risks from AI-powered vulnerability discovery and AI-generated correctness and security errors in software.The paper frames rigorous software verification and formal methods as part of the response to these risks.
- Expanding CS-relevant abstractions in Lean is intended to enhance AI provers’ capabilities in formal verification settings.
- CSLib formalizations will provide high-quality training data, while AI proof tooling is expected to accelerate CSLib development in a reciprocal flywheel.
- AI-generated formalizations may be buggy or difficult for humans to understand, so CSLib assigns AI an advisory role and requires manual GitHub-based code review.
4 Building a CSLib Community
CSLib seeks a broad user base spanning computer-science research, industry, and education, supported by community activity, development tooling, language translations, and documentation. Its adoption depends especially on reducing verification costs and bridging Lean with mainstream imperative languages.
- CSLib aims to serve researchers, engineers across industries, and universities by reducing formal-verification costs and supporting computer-science education.
- The project follows Mathlib’s community model, using open discussion and a CSLib Lean Zulip channel to support large-scale formalization.
- AI formalization and theorem-proving tools, alongside rigorous code review, are expected to lower the cost of developing and maintaining CSLib.
- Translations from mainstream languages such as Rust and C++ to Boole are especially important because dependently typed languages have had limited adoption outside their traditional ecosystem.
- CSLib plans searchable documentation, including area-specific tutorials and entry-level textbooks.
5 Governance Model
CSLib uses a dual-body governance structure that separates strategic direction from technical execution. The project expects this structure to evolve as the community grows while preserving coherence, expertise, and broad participation.
- A steering committee of academic and industry leaders guides CSLib’s vision and secures financial support, while a maintainer team handles technical execution.
- Maintainers will be invited periodically based on merit, especially contributions and review activity, together with project needs.
- The governance model is intended to combine strategic coherence, technical excellence, and a welcoming environment for contributors.
6 Roadmap
CSLib’s tentative 2026–2027 roadmap moves from initial formalizations and a maturing Boole framework toward broader coverage, unification, and larger verification targets. The project plans both advanced computer-science formalization and end-to-end verification of a substantially sized real-world system.
- The roadmap is explicitly tentative because CSLib is only a few months old and its scope will be refined with community input.
- 2026: The 2026 roadmap targets many undergraduate algorithms and data-structures formalizations and most undergraduate theory-of-computation models and logics.The repository already contains initial formalizations of operational semantics, program equivalences, automata models, linear logic, and elementary sorting and searching algorithms.
- 2026: By the end of 2026, Boole is expected to generate Lean verification conditions, interact with SMT-based hammers, and represent numerous elementary algorithms and data structures.
- 2027: The 2027 Pillar 1 roadmap expands to complexity theory, concurrency, secure compilation, and randomized and quantum algorithms, with a goal of aiding a foundational discovery.
- 2027: By the end of 2027, Pillar 2 is expected to support separation-logic machinery and enable end-to-end verification of at least one substantially sized real-world system.