Mathlib provides a centralised library of formalised mathematics in Lean, but Lean has had no comparable unified library for computer science. Such a library needs shared abstractions for operational semantics and must stay compatible with Mathlib.

CSLib bundles reduction systems and labelled transition systems as Lean structures. From these it derives standard notions such as multistep reduction, reachability, and confluence, and it provides notation attributes that work with the calc tactic. Proof automation built on Lean's grind tactic is treated as a design constraint on interfaces. The library reuses Mathlib's linters and CI and adds stricter namespacing linters and weekly expensive checks.

Developments include bisimilarity, similarity, and trace equivalence with up-to techniques, CCS, NFA-to-DFA subset construction, and lambda-calculi with polymorphism and subtyping. Declarations that adopted grind after their initial commit saved an average of 7.1 LoC per theorem, with 15 to 39 LoC saved on bisimilarity proofs. The System F formalization is about 45% smaller than the Rocq development it was modelled on.