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

The Formal Frontier and Formal-First Research

By Fabrizio Montesi. Created on 2026-10-19. Last updated on 2026-10-19.
See also: CSLib: Library-Grade Computer Science and Europrogramming

Table of Contents (click to show)

The Formal Frontier: Needle projects reach far, Foundation projects extend outwards, Amplification projects strengthen within, and Exploration projects discover nearby. — Working at the Formal Frontier: Needle projects reach far, Foundation projects extend outwards, Amplification projects strengthen within, and Exploration projects discover nearby.

The formal frontier is the current extent of our shared, machine-verified knowledge, as embodied in formal libraries such as CSLib [Barrett et al., 2026; Henson and Montesi, 2026], Mathlib, and Physlib.¹

As these libraries grow, they open new research and innovation opportunities. Results that once required substantial preparatory work may become directly accessible through reusable definitions, theorems, and APIs. Together with increasingly capable tools, particularly AI, this makes formal-first research an increasingly accessible approach to formal sciences (like computer science and mathematics).

By formal-first research, I mean research that is:

Planned with awareness of where the formal frontier stands.
Conducted with the aid of the formal frontier and its tooling.

What changes is not only when we formalise, but also how the existing body of formal knowledge informs the questions we ask and the research we undertake. We start by understanding what we can already build upon, identifying what is missing, and deciding how to advance our knowledge while contributing to shared formal foundations.

This contrasts with some traditional research approaches in which formalisation is treated as a subsequent step, perhaps even a clean-up exercise, if it happens at all. Formal-first research brings formalisation into the process from the earliest stages of conceptualisation.

By this, I do not mean to suggest that we should abandon informal research, or pursue only problems that are easy to formalise. Rather, I am trying to give words to intuitions that are already developing among researchers working with the formal frontier. Making these ideas explicit can help us discuss them, refine them, and put them into practice more effectively. As a starting point, I propose the following taxonomy.

A taxonomy of project traits

Here is a first taxonomy of traits of formal frontier projects, based on how they relate to the existing frontier:

A Needle Project pursues a specific goal far beyond the current frontier, developing a focused path towards it and formalising what is needed along the way.
A Foundation Project extends the scope of the formal frontier by establishing the definitions, abstractions, and results needed to make new areas of knowledge formally accessible.
An Amplification Project increases what can be accomplished with existing formal knowledge, for example by generalising theories, connecting APIs, or developing better automation.
An Exploration Project investigates new research questions made accessible by the existing formal frontier, building upon established foundations to discover new results.

The taxonomy lends itself to a geometric interpretation: Needles reach far, Foundations extend outwards, Amplifications strengthen within, and Explorations discover nearby. The next figure illustrates these four ways of relating to the frontier.

A geometric interpretation of the four formal-first project traits. Green represents the existing formal frontier, while purple represents new development. The traits may coexist within the same project.

Importantly, these four traits describe different ways of relating to the formal frontier, rather than different kinds of scientific achievements. They imply no ranking of ambition, difficulty, or scientific merit. Nor are they mutually exclusive: a project may exhibit several traits simultaneously. Even the terminology matters: the names should evoke different research strategies without suggesting a hierarchy of prestige.²

For example, developing a reusable theory of compiler correctness in CSLib might involve establishing foundations for operational semantics and rule formats, amplifying these foundations through reusable abstractions and automation, and exploring their applicability to concrete compilers. Work on one aspect may reveal new requirements for another.

Projects can also evolve over time. A needle may eventually become a shared foundation, while an exploration may reveal opportunities for amplification. Different researchers within the same team, or across the world, may pursue complementary activities simultaneously.

The formal frontier is continually evolving, and so should our ways of contributing to it. The taxonomy is intended to help us understand, discuss, and plan these possibilities, not constrain them.

This is particularly powerful when we treat formal libraries as collaborative knowledge bases in continuous evolution.

For example, I contributed the initial module for transition systems to CSLib. Other contributors subsequently improved proofs, optimised performance, and suggested additional results to make the API more broadly applicable. What began as an individual contribution gradually developed into richer, shared infrastructure. Later, this infrastructure supported developments in areas such as automata theory and distributed consensus. In terms of our taxonomy, an initial Foundation effort attracted Amplification contributions, eventually enabling new Explorations and Needles.

Shared formal libraries make machine-verified knowledge available for direct reuse. Formal-first projects deliberately build upon it.

AI and the Formal Frontier

As AI systems become more capable, formal-first research offers a promising way to keep humans in the captain's chair of research and innovation.

As formal libraries grow, navigating their contents becomes increasingly challenging. AI can help researchers discover relevant results, understand existing APIs, identify missing abstractions, and recognise opportunities that might otherwise go unnoticed.

It can also help us advance the frontier: constructing proofs, developing new foundations, amplifying existing APIs, pursuing needles, and exploring new research questions.

Researchers can choose the initial scientific questions, design the abstractions, and determine where to direct their efforts. The formal frontier gives humans and AI a shared, explicit foundation on which to build, helping researchers understand the assumptions and dependencies of AI contributions, evaluate their results, and guide subsequent work. Formal verification makes it possible to check the resulting proofs independently of how they were produced. Of course, deciding whether we have formalised the right questions and developed useful abstractions remains a matter of scientific judgement.

Doing science together

The implications of formal-first research extend beyond individual projects.

An awareness of the formal frontier can help individual researchers, developers, research supervisors, groups, and organisations plan their work more consciously. It can help us recognise valuable contributions beyond individual theorems, including the foundations and APIs that enable entire families of future results.

And because these foundations are shared, this way of thinking can extend beyond individual institutions to a global research community.

Formal-first research is not intended to replace other approaches. It is an increasingly accessible way of doing science together, starting from shared, machine-verified knowledge and deliberately contributing to its evolution.

The formal frontier helps us understand where we stand, so that we can deliberately choose where to go next – and help others go further.

¹ Not to be confused with the Formal Frontier project by the Mathlib Initiative, which aims to advance the formalisation of mathematical knowledge. Here, formal frontier refers to the current extent of shared formalised knowledge, rather than a particular formalisation initiative.

² For example, I deliberately use Needle rather than Moonshot. The latter suggests exceptional ambition or importance, whereas distance from the current formal frontier says nothing about a project's scientific merit. Needle emphasises the focused path towards a distant goal, without assigning value to that goal.

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

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