Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt

Use this file to discover all available pages before exploring further.

Formal program specification is the practice of expressing precisely and unambiguously what a software system must achieve — independent of how it is implemented. Unlike prose requirements or UML diagrams, a formal specification carries mathematical semantics: there is no room for misinterpretation, because the meaning is determined by the logic of the underlying language. Lean-Spec is a tutorial demonstrating how Lean 4, a dependently typed functional programming language, can serve as an expressive and practical specification language for real software. Crucially, you do not need to write proofs to benefit from formal specifications — the specification itself, expressed as a Lean type, is already a rigorous, machine-checkable statement of intent.

​
Why Formal Specification?

In a typical industrial software development process, requirements are captured as shall clauses written in natural language, supplemented by UML diagrams and descriptive text. Despite significant effort to use precise language, these artefacts remain open to interpretation.
Experience shows that, despite significant effort being expended on using precise language, specifications and designs are open to interpretation. A designer may misinterpret the intent of a requirement, a software developer the intent of a requirement or design clause, a tester the intent of a requirement.
The core problems with natural language specifications are:
  • Vagueness — natural language words carry contextual ambiguity that formal symbols do not.
  • Missing context — informal presentations may omit dependencies that are obvious to the author but not to the reader.
  • Inconsistent interpretation — different stakeholders (designers, developers, testers) may draw different conclusions from the same clause.
Formal specifications resolve these problems through the semantics of the underlying formal language. Mathematical notation, refined over centuries, allows concise expression. Everything a specification depends on must be made explicit — the formal syntax enforces it. The result is a specification that is complete, unambiguous, and amenable to automated checking. Importantly, specification without proof is still highly valuable in software development. Theorems without proof have limited value in mathematics, but a formal specification without a full correctness proof is already far more useful than an informal one: it can be reviewed, debated, and used as a reference to settle functional questions with precision.

​
Why Lean?

Lean is a dependently typed functional programming language that incorporates the Curry–Howard correspondence between propositions and types (and between proofs and programs). This makes it uniquely positioned as a software specification tool. The README identifies three concrete benefits:
  1. Specification language — Lean can be used to specify the functionality of software that may be implemented in Lean or in other languages. The specification lives independently of any implementation.
  2. Verification — Lean software can be verified in Lean itself, using the same logic employed for mathematical proof. When you are ready to go beyond specification, the framework is already there.
  3. Proof yields program — When a Lean specification is viewed as a theorem in the Lean logic, a proof of that theorem yields a program that satisfies the specification by construction. This means type correctness = program correctness when dependent types are used to their full capacity.
The key ingredient is the dependent type. In a non-dependent type system, the type of a value cannot depend on the value of another term. Dependent types break this restriction, enabling types that carry logical propositions about their inhabitants. A subtype { a : A // P a } is the canonical example: its elements are exactly those a : A for which the proposition P a holds. This means a function returning { m : Nat // m = 2 * n } is not merely a function — it is a function together with a proof that its output is twice its input. Lean also integrates a comprehensive functional programming language (in the style of Haskell) and a large body of formalised mathematics via mathlib4. In the case of Lean, the specification language, programming language, and proof framework are one and the same language — there is no impedance mismatch between the layers.

​
About This Tutorial

This tutorial is focused exclusively on specification — expressing what a function must achieve, not how it achieves it. Proof and verification are not covered here. Readers wanting to go deeper into those areas should consult the following resources: The tutorial walks through a series of progressively richer specification examples, from simple arithmetic properties to real-world aviation industry scheduling and flight planning problems.

​
Tutorial Modules

Introduction

Introduction to Lean as a specification language. Covers propositions, types, subtypes, and the Double specification example.

Quotient & Remainder

Specifying quotient and remainder on division — a clean example of using subtypes to capture arithmetic invariants.

Sort

Specifying a sort function: expressing that the output is a permutation of the input and that it is ordered.

Knapsack

Knapsack optimisation — specifying an NP-hard combinatorial optimisation problem in a few lines of Lean.

Graph

Graph searching — specifying reachability and path properties over graph structures using dependent types.

TMI

A scheduling example drawn from the aviation industry, demonstrating specification of complex temporal constraints.

Flight Planning

Flight planning message processing: a full industry example from aviation, showcasing the expressiveness of Lean for real specifications.
Bottom-up definition order. This tutorial has been developed as a Lean script that can be loaded into a Lean IDE such as Visual Studio Code. Lean requires that any value be defined before it is used, which imposes a strict constraint on how a specification is presented. While it is often preferable to present specifications top-down — starting with higher-level concepts and decomposing them — the Lean definition-before-use requirement means that all specifications in this tutorial are presented bottom-up.

​
The Core Idea: Types as Specifications

The central insight of Lean-Spec is that a type is a specification. Consider doubling a natural number. One might first try to express this as a proposition: 
def DoubleProp := ∀n : Nat, ∃m : Nat, m = 2 * n
This is a valid Lean proposition, but propositions have no computational content in Lean — they are either provable or not, and you would need to define the function separately and prove it satisfies the proposition. That is verification, not specification-as-type. Types, by contrast, have data and computational content. Using Lean’s dependent types, we can build a type whose elements are the functions satisfying the property. The key mechanism is the subtype { a : A // P a }, which combines a type A with a proposition P. Its elements are pairs: a value a : A together with evidence that P a holds. Applying this to the doubling example: 
-- A type: functions that take n and return m together with evidence that m = 2 * n
def Double₂ := (n : Nat) → { m : Nat // m = 2 * n }
Moving the universally quantified variable to the left of := (the idiomatic form used throughout this tutorial): 
def Double₃ (n : Nat) := { m : Nat // m = 2 * n }
Double₃ is the specification. An implementation satisfying it must provide both the value and the evidence: 
def double (n : Nat) : { m : Nat // m = 2 * n } :=
  {val := 2 * n, property := rfl}
The field val is the computed number; property is the evidence (rfl — reflexivity — is enough here because 2 * n = 2 * n is trivially true). We can verify the implementation meets the specification: 
variable (n : Nat)
#check (double n : Double₃ n)  -- double n : Double₃ n  ✓
And Lean evaluates only the computational content: 
#eval double 4  -- 8
Lean outputs 8, not the full subtype structure {val := 8, property := rfl}, because non-computational content is erased at evaluation time. This is a practical demonstration that formal specifications do not impose runtime overhead.

Build docs developers (and LLMs) love

Get started for freeTalk to us