Before an aircraft can depart, its operator must file a flight plan with the Air Traffic Services (ATS) provider, declaring where and when the flight will operate and what equipment the aircraft carries. That plan is not a single static document — it evolves as circumstances change. Delays are reported, routes are modified, flights are cancelled, and departures and arrivals are confirmed. Each of these events is communicated through a standard ICAO message. This example is a full Lean 4 specification of that message-processing system: the data model, the message types, the invariants that bind them together, the state that accumulates flight information, and the operations that update and query it.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.
Background
The standard for flight planning messages is defined by the International Civil Aviation Organisation (ICAO) in the Procedures for Air Navigation Services: Air Traffic Management, published as ICAO Doc 4444 (PANS-ATM). Appendix 3 of PANS-ATM defines a set of messages for communicating flight information between operators and ATS providers. The subset relevant to flight planning consists of six message types.| Message Type | Purpose |
|---|---|
| FPL | File a plan for an intended flight |
| DLA | Report a delay to a previously filed flight |
| CHG | Modify a previously filed flight plan |
| CNL | Cancel a planned flight |
| DEP | Report a flight has departed |
| ARR | Report a flight has arrived |
Example FPL Message
A real FPL message looks like this:WOL H65 RAZZI Q29 LIZZI DCT describes the route the flight will follow through the airspace. The final line carries supplementary information items including the aircraft registration (VHXYZ).
A FPL message is not a free-form document — it is assembled from a defined set of numbered fields, each carrying a specific category of information. The fields present in the example above are:
| Field Number | Content |
|---|---|
| 7 | ABC123 |
| 8 | IS |
| 9 | B738/M |
| 10 | SADE2E3GHIRWZ/LB1 |
| 13 | YSSY0400 |
| 15 | M079F380 DCT WOL H65 RAZZI Q29 LIZZI DCT |
| 16 | YMML0100 |
| 18 | PBN/A1B1C1D1O2S2T1 NAV/RNP2 DOF/230220 REG/VHXYZ SEL/AFPQ CODE/7C6DDF OPR/FLYOU ORGN/YSSYABCO PER/C |
What the Specification Covers
The specification addresses the full lifecycle of flight information processing:- Data elements: Basic types for identifiers, codes, and constrained strings that form the building blocks of all message content.
- Invariants: Consistency constraints between fields within messages and flights. For example, if field 10 indicates that a flight carries performance-based navigation equipment, field 18 must carry the corresponding PBN capability codes.
- State model: A flight store that maps flight identifiers to accumulated flight histories, including the sequence of messages received for each flight in descending timestamp order.
- Message processing: For each message type, a specification of how the state is updated when that message is received — including how the relevant flight is located by matching identifiers, and how invalid or inconsistent messages are handled.
- Maintenance: Operations on the state such as purging flights whose operational period has expired.
- Querying: Functions that interrogate the state to retrieve current flight information.
Module Structure
The specification is divided into five modules. Each layer builds on the previous one: core data types support field definitions, fields are assembled into flight records, flights are packaged into messages, and messages are processed against a state.The flight planning specification depends on three general-purpose support libraries: Util (finite sets and maps, including the
Set A and A ⟹ B types), Geo (geographical positions, aerodromes, and airspace), and Temporal (date-time groups, durations, and intervals). These libraries are used extensively across all five modules.| Module | Purpose |
|---|---|
| Core | The core data elements from which higher-level entities are built |
| Field | The fields from which messages are assembled |
| Flight | Data entity capturing all information on a flight |
| Message | The message types for flight planning |
| State | Message processing against a state of known flights |
Core
Basic data types: identifiers, codes, aircraft designators, route elements, and constrained string types that underpin all higher-level definitions.
Field
Numbered ICAO fields assembling related data items, with worked examples of each field drawn from real ATS messages.
Flight
The flight data entity as the union of all relevant fields, together with flight identification, status, and matching logic.
Message
The six ICAO message types (FPL, DLA, CHG, CNL, DEP, ARR) with their field compositions and cross-field consistency invariants.
State
State definition, message processing (including error handling), maintenance operations, and query functions over the flight store.
Characteristics of This Specification
The flight planning specification is representative of a broad class of real industry systems. Its four defining characteristics are common across ATS systems, air operations centres, and many other stateful information-processing applications. State is held. The system maintains a persistent store of flight information — aFlightStore mapping each FlightId to a FlightHistory. A FlightHistory carries both the current accumulated flight record and the ordered sequence of timestamped messages received for that flight. The invariant that messages are stored in descending timestamp order is encoded directly in the type, not enforced by a separate check.
Messages are received. The system’s interface to the outside world is a stream of incoming messages. Each message is of one of the six ICAO types. All messages are timestamped on receipt for audit purposes. The specification defines, for each message type, exactly what the message contains and what constraints must hold for it to be considered well-formed.
State is updated. The core behavioural specification is the processing function: given a current state and an incoming message, produce a revised state. This involves locating the relevant flight in the store (using the identifier matching logic defined in the Flight module), applying the update described by the message, and recording the message in the flight’s history. Messages that are inconsistent with the current state — for example, a CHG received for an unknown flight — are handled according to specified rules.
State is queried. Beyond processing updates, the specification defines query operations that extract information from the state — for example, retrieving the current record for a flight, listing all flights active during a given time interval, or identifying flights that have not yet reported departure. These operations are specified over the FlightStore type and are fully determined by the state at the time of the query.
Together, these characteristics make the flight planning specification an instructive example of how Lean 4 handles a system that is significantly more complex than a self-contained algorithm. The layered module structure, the use of dependent types to enforce cross-field consistency, and the formal treatment of state transitions all scale naturally to the size and intricacy of a real ICAO-conformant flight data processing system.