CSLib: The Lean Computer Science Library

Where it stands today

Fifteen and a half months after the first commit:

leanprover/cslib main at c149a9d (2026-10-01).

What is in it

Governance

CSLib lives in the leanprover GitHub organisation, next to Lean itself. The steering committee guides the vision and secures support:

• Clark Barrett (Stanford, Amazon)

• Swarat Chaudhuri (Google DeepMind, UT Austin)

• Jim Grundy (Amazon)

• Pushmeet Kohli (Google DeepMind)

• Leonardo de Moura (Lean FRO, Amazon)

• Fabrizio Montesi (FORM, University of Southern Denmark)

Maintainers

The maintainers own the codebase and its technical direction. Lead maintainer: Fabrizio Montesi. Technical leads: Alexandre Rademaker (Logic), Sorrachai Yingchareonthawornchai (Algorithms and data structures).

Area maintainers:

• Chris Henson (Drexel): λ-calculus, metaprogramming

• Kim Morrison (Lean FRO): CI/CD with Lean and Mathlib

• Samuel Schlesinger (Google): Complexity, cryptography, learning theory

• Christian Reitwiessner: Complexity

• and the technical leads

New members are invited on project need and merit.

How to contribute

Depend on it first. That is the fastest way to find what is missing:

[[require]]
name = "cslib"
scope = "leanprover"
rev = "<a commit SHA>"   # pin it: `main` moves fast

• Most contributions are pull requests, approved by a relevant maintainer.

• Anything cross-cutting: discuss first, on the #CSLib Zulip channel or an issue.

• Weekly online meetings

• The rules are written down: CONTRIBUTING.md (style, documentation, AI use) and DECISION_MAKING.md (how PRs are reviewed and accepted).

How a pull request gets in

From DECISION_MAKING.md:

• Every PR is reviewed. Anyone may review, and reviewing is a contribution in its own right.

• Acceptance needs one maintainer's approval, and every substantive part reviewed.

• An objection blocks the merge until it is resolved, by technical discussion first. If that fails, the Lead Maintainer decides.

• Reuse over duplication: build on existing definitions, in CSLib or its dependencies, unless an alternative has a clear technical benefit.

The semantic spine

The most reused abstraction in the library: a labelled transition system is just a ternary relation.

A nondeterministic automaton is an LTS with start states:

Nondeterministic Turing machines SingleTapeNTM extends NA, with tape actions (read, write, move) as labels.

CSLib authors: Fabrizio Montesi (@fmontesi), Thomas Waring (@thomaskwaring), Ching-Tsun Chou (@ctchou), Chris Henson (@chenson2018)

A tiny nondeterministic automaton

An NA.FinAcc is an NA (an LTS with start states) plus a set of accepting states. Its instance of Acceptor says when a word is accepted: a multistep transition (MTr) labelled by the word leads from a start state to an accepting state.

language a is the set of words that a accepts.

...in Lean

Words over {a, b} that end in a. On a, state q₀ may stay or move to q₁:

Bisimulation, defined once

Two states are bisimilar, s₁ ~[lts₁, lts₂] s₂, when some bisimulation relates them.

Bisimulation, constructively

Two clocks: one state ticking forever, and two states ticking back and forth. To prove them bisimilar, exhibit a relation, here everything to everything, and check the transfer condition:

Two vending machines

Milner, Communication and Concurrency (1989).

• Good: coin, then you pick tea or coffee. \mathit{Good} \stackrel{\text{def}}{=} \mathit{coin}.(\mathit{tea}.\mathit{Good} + \mathit{coffee}.\mathit{Good})

• Bad: coin, then the machine picks. \mathit{Bad} \stackrel{\text{def}}{=} \mathit{coin}.\mathit{tea}.\mathit{Bad} + \mathit{coin}.\mathit{coffee}.\mathit{Bad}

Their logs are identical: coin tea, coin coffee, ... Same traces. A trace-based test cannot tell them apart.

After the coin, the bad machine may already have chosen coffee, and then the tea button does nothing. A trace records the actions that happened; it never records an action that was refused.

Example: Jesse Alama (@jessealama). CSLib authors: Fabrizio Montesi (@fmontesi).

Traces are too coarse

Trace equivalence ignores which actions are available at each step.

Bisimilarity (slide 14.4): every move of one machine must be matched by a move of the other, and the states reached must again be related, at every step.

Two ways to prove that our machines are not bisimilar:

1. Directly, as CSLib's own vm_ltsD_ltsND_not_bisim does: assume a bisimulation and follow the transitions until it breaks.

2. With a logic: find a formula that one machine satisfies and the other does not.

...in CSLib's CCS

One LTS, machines, with two constants: the good machine is const .good, the bad one const .bad.

...and its semantics

The transitions of a CCS process are an inductive relation, one rule per construct. CSLib declares it as an LTS with @[lts lts]:

Our machines need four rules: pre, choiceL, choiceR, and const, which unfolds a constant through defs.

...as transition graphs

Both have the traces coin tea, coin coffee, ... After coin, Good still offers both drinks; Bad has already committed to one.

...not bisimilar, directly

Assume a bisimulation r. After coin, the good machine has a single successor, so r must relate tea.Good + coffee.Good with tea.Bad. Only the first can do coffee:

Hennessy–Milner logic

A modal logic for labelled transition systems. Its formulas describe which actions a state can perform, and what holds after them:

\begin{aligned} s \models \langle a\rangle\,\varphi &\iff \exists s'.\; s \xrightarrow{a} s' \text{ and } s' \models \varphi && \text{some } a \text{ is possible, then } \varphi \\ s \models [a]\,\varphi &\iff \forall s'.\; s \xrightarrow{a} s' \text{ implies } s' \models \varphi && \text{after every } a,\ \varphi \end{aligned}

plus ⊤, ¬ and ∧.

Hennessy–Milner theorem (1985):

• Bisimilar states satisfy the same formulas.

• For image-finite systems, the converse holds: states that are not bisimilar are always told apart by some formula.

The first direction is the one we use, as CSLib's bisimulation_satisfies:

CSLib authors: Fabrizio Montesi (@fmontesi), Marco Peressotti (@mperessotti), Alexandre Rademaker (@arademaker).

...one formula, in CSLib's HML

In CSLib, formulas are evaluated in a model, an LTS plus a valuation of atomic propositions (Cslib/Logics/HML/Basic.lean):

Our model m is the CCS LTS of both machines with no atomic propositions (Atom := Empty), so only transitions matter. The formula [coin] ⟨tea⟩ ⊤: after every coin, tea is possible.

...which the good machine accepts and the bad machine fails

In obtain ⟨_, ⟨⟩, ⟨⟩⟩, each ⟨⟩ case-splits a hypothesis and substitutes it away: after one coin, the good machine has a single successor, and the goal is now about that successor.

...and a theorem

So a formula true for one machine and false for the other is a certificate that they are not bisimilar.

Three parts of CSLib in 35 lines

• A language: CCS, with its operational semantics.

• A logic: HML, evaluated on that semantics.

• The semantic infrastructure that connects them: transition systems, bisimulation, the Hennessy–Milner theorem.

Languages produce transition systems. Logics consume them. Metatheory is proved once.

Your program is already a specification

To check that a fast program is correct, we need a specification. Often the simplest program that does the job is that specification: obviously correct, but too slow to use.

• Specification: insertion sort, six lines, nothing clever.

• Implementation: CSLib's verified mergeSort, standing in for the optimised version an engineer, or an AI agent, would write.

• Goal: prove they return the same output on every input, and count how many comparisons each one makes.

Both are written in CSLib's time monad TimeM: a program returns its result together with a cost, and each ✓ charges one comparison.

Example: Jesse Alama (@jessealama). CSLib authors: Sorrachai (@sorrachai), Eric Wieser (@eric-wieser), Kim Morrison (@kim-em).

...the obvious sort

...same answer, different bill

...connected to Mathlib

⟪p⟫ drops the cost and keeps the result. Without its cost, our insertion sort is Mathlib's List.insertionSort:

Why Mathlib's definitions: Mathlib already proves that List.insertionSort returns a sorted permutation of its input. One bridge lemma, and we reuse those proofs instead of redoing them.

Mathlib authors: Jeremy Avigad (@avigad), Wrenna Robson (@wrenna-robson).

...equivalent, for every input

Both outputs are sorted permutations of the input, and a list has only one sorted permutation:

• From CSLib: mergeSort_correct, the output of mergeSort is sorted and a permutation of xs.

• From Mathlib: List.sortedLE_insertionSort and List.perm_insertionSort, the same for insertion sort; and List.Perm.eq_of_sortedLE, two sorted lists that are permutations of each other are equal.

...and the cost of insertionSort is n²