Follow with Edit this page on Go back to the Bliki index

By Fabrizio Montesi. Created on 2026-10-08. Last updated on 2026-10-08.

CSLib is the Lean Computer Science Library, a project we started with the aim of building a shared formal infrastructure for computer science and verified programming [Barrett et al., 2026; Henson and Montesi, 2026].

At the time of this writing, CSLib has recently reached its 1000th pull request (code contribution submission). That feels like a good occasion to reflect on a central question that pervades the library and I as lead maintainer often have to think about: when is a formalisation 'good' for CSLib? The answer is multifaceted. It should be correct, of course. It should be well designed, maintainable, and useful. But none of these quite capture a clear guideline, and we always gotta leave room for realism and allow for incremental improvement – often, making CSLib-quality code requires inventing new things! So we are not talking about hard requirements; we are talking about an aspiration, a vision.

Now, since CSLib aims to be a shared infrastructure for computer science and programming, I think that a better formulation of the question is:

What does it mean to do library-grade computer science?

A central part of the answer is reuse. Not just software reuse in the ordinary sense, but reuse of formalised knowledge: definitions, abstractions, theorems, interfaces, and automation that facilitate future developments. The key idea is that knowledge and tools should compound into powerful infrastructure, rather than merely accumulate.

I find a distinction from the literature on software reuse useful. Prieto-Díaz [1993] distinguishes between:

• vertical reuse, within the same domain or application area; and
• horizontal reuse, where generic components are reused across different applications and domains.

Let's unfold this a bit in the context of formal computer science. As a running example, I'll stick to our recent development of a generic framework for modal logic in CSLib [Girlando and Montesi, 2026].

Vertical Reuse

The goal of vertical reuse is that specialised developments should inherit as much as possible from more general ones.

In the example of modal logic, there is an entire family of logics that use modalities to achieve different things: basic modal logic, temporal logics, Hennessy–Milner Logic, provability logics, epistemic logics, and so on. The surface languages and semantics of these logics have many common ideas, but they formally differ. In the words of Blackburn et al. [2001] in their textbook:

‘Ask three modal logicians what modal logic is, and you are likely to get at least three different answers.’

Patrick Blackburn, Maarten de Rijke, Yde Venema, ‘Modal Logic’.

For CSLib, however, we want to ask the question:

How much of the theory can be formalised once and then reused?

We were not ready to deal with this question right off the bat. Logic has some common abstractions (like inference systems, logical equivalence, and more) that we had to explore through simpler cases first. Recently, we had formalised Hennessy–Milner logic in a way that integrates well with CSLib's abstractions [Montesi et al., 2026] and, likewise, basic modal logic. At this point we could reason about statements like the following, using separate developments.

We then turned our attention to the textbook generic framework for modal languages [Blackburn et al., 2001], in the hope of unifying some developments. This formalisation effort led us to develop generalised properties and a hierarchy of abstractions that allow for deriving more specialised modal interfaces.

Basic modal logic, basic temporal logic, and Hennessy–Milner Logic can be obtained by specialising this common infrastructure, inheriting semantics and shared metatheory. For example, both of the previous axioms about duality are direct consequences of the more general duality axiom for generic modal logic, given next.

I particularly like the example of how Hennessy–Milner logic looks before and after; that is, the ad hoc implementation versus the one derived from the general framework. Factoring out generic parts led to a 67% reduction in logic-specific code, and all useful instances are obtained completely automatically. Not only did we get a leaner codebase, we even got new features: the new implementation inherits the possibility of having atomic propositions.

In general, when a new development belongs to an existing family, it should inherit the knowledge we already have about that family rather than reproduce it.

Horizontal Reuse

In horizontal reuse, the goal is not to derive another member of the same family, but to make an abstraction useful somewhere else: we want to apply it to other developments and domains.

Keeping to modal logic, the area can be seen as a reasoning methodology for relational structure. Once its semantics is connected to ordinary Lean predicates, sets, transition systems, and other structures, the modal library can be used as a reasoning tool outside modal logic itself.

In CSLib, we have shown how these connections enable the application of modal logic to reason about mathematics, programming languages, and concurrency theory. None of these is ‘another modal logic’. Instead, we expose an independently formalised object through an appropriate interface, and an existing body of modal theory becomes applicable to it.

This is where library-grade formalisation becomes especially powerful. A formalised theory stops being only an object of study and becomes a reasoning technology for other theories and applications.

A straightforward example is using Hennessy-Milner Logic to prove that a concurrent process respects a specification, as in the next figure.

Perhaps more surprising is the fact that we can use modal logic to reason about algebraic properties, as shown below. While this is not a new theorem, finding out that modal logic can be used to reason about radicals of ideals in mathematics was a really satisfying development! Particularly because we made a general construction that translates algebraic properties into properties of modal logic models, so the entire approach is reusable.

Making reuse usable

Reuse does not happen automatically just because we have found the right abstractions. We can build something wonderfully general, but we should also strive to make it easy to apply.

A useful principle is:

General underneath, natural at the surface.

Keeping to the example of modal logic, the generic framework supports operators of arbitrary arity through a fairly general representation. But somebody working with basic modal logic should not have to think about that: they should see the familiar operators ◇ and □, with their usual semantics. Somebody working with Hennessy–Milner Logic should see modalities indexed by transition labels.

The same holds for theorems. Having a theorem somewhere in the library is not quite the same as making its knowledge reusable. If every downstream application requires manually rediscovering a chain of five generic lemmas, unfolding representations, and translating between abstraction layers, then using the library becomes cumbersome.

We have found proof automation to be very useful in making generic knowledge easy to activate in specialisations. This is why we treat proof automation as part of the library interface. In modal logic, this is exposed as a grind set called modal, which gives access to a dedicated database of modal results so that routine reasoning can be automatically discharged.

This also gives us useful feedback as library designers. If an elementary fact repeatedly requires bespoke proofs, that may be telling us that the problem is not the proof: perhaps an interface is missing, a theorem is stated in the wrong form, or an abstraction boundary needs to move.

So library-grade computer science has another requirement: the accumulated knowledge should not only be available, but easy to activate.

Conclusion

None of these are hard admission criteria; library development is incremental, and getting to the right abstraction often requires first building some concrete objects. But they describe the direction in which we are going.

I have used modal logic as an example, but CSLib offers many others. This includes, but is not limited to, reusable APIs for semantics, shared infrastructure for automata and computability, and a rich vocabulary for reasoning about relations.

In other words, to conclude:

The question is not only what we have formalised, but what becomes possible to formalise because CSLib exists.

References

Clark W. Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura 0001, Alexandre Rademaker, Sorrachai Yingchareonthawornchai [2026], CSLib: The Lean Computer Science Library. In CoRR abs/2602.04846.
Full view & info | PDF | bibtex | doi.org

@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}
}

Patrick Blackburn, Maarten de Rijke, Yde Venema [2001], ‘Modal Logic’, Cambridge University Press. DOI: 10.1017/CBO9781107050884.

Marianna Girlando, Fabrizio Montesi [2026], Library-Grade Modal Logic. In CoRR abs/2610.04511.
Full view & info | PDF | bibtex | doi.org

@misc{gm26-arxiv,
title={Library-Grade Modal Logic},
author={Marianna Girlando and Fabrizio Montesi},
year={2026},
eprint={2610.04511},
archivePrefix={arXiv},
primaryClass={cs.LO},
url={https://arxiv.org/abs/2610.04511},
}

Christopher Henson, Fabrizio Montesi [2026], Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib). In CoRR abs/2602.15078.
Full view & info | PDF | bibtex | doi.org

@article{DBLP:journals/corr/abs-2602-15078,
  author       = {Christopher Henson and
                  Fabrizio Montesi},
  title        = {Computer Science as Infrastructure: the Spine of the Lean Computer
                  Science Library (CSLib)},
  journal      = {CoRR},
  volume       = {abs/2602.15078},
  year         = {2026},
  url          = {https://doi.org/10.48550/arXiv.2602.15078},
  doi          = {10.48550/ARXIV.2602.15078},
  eprinttype   = {arXiv},
  eprint       = {2602.15078},
  timestamp    = {Sun, 29 Mar 2026 14:38:05 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2602-15078.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker [2026], Hennessy-Milner Logic in CSLib, the Lean Computer Science Library. In CoRR abs/2602.15409.
Full view & info | PDF | bibtex | doi.org

@article{DBLP:journals/corr/abs-2602-15409,
  author       = {Fabrizio Montesi and
                  Marco Peressotti and
                  Alexandre Rademaker},
  title        = {Hennessy-Milner Logic in CSLib, the Lean Computer Science Library},
  journal      = {CoRR},
  volume       = {abs/2602.15409},
  year         = {2026},
  url          = {https://doi.org/10.48550/arXiv.2602.15409},
  doi          = {10.48550/ARXIV.2602.15409},
  eprinttype   = {arXiv},
  eprint       = {2602.15409},
  timestamp    = {Sun, 29 Mar 2026 14:38:07 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2602-15409.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

Rubén Prieto-Díaz [1993], ‘Status Report: Software Reusability’, IEEE Software 10(3), pp. 61–66. DOI: 10.1109/52.210605.