New to the model
Take the guided tour
Five steps: what the model holds, how its areas build on each other, and where it needs a decision.
Formally verifying airline booking rules
When you book a flight, the airline makes you an offer, and accepting it creates an order: something that is paid for, changed, refunded and finally used. IATA, the airlines' trade association, describes how offers and orders should work in its ONE Order standard. The standard is written in prose, and prose leaves gaps that two systems can fill differently.
This project uses formal verification: each rule is written as code in Lean, a language that checks proofs. A guarantee that Lean proves holds in every possible case. Where the rules as written cannot meet a guarantee, the gap becomes a question for the business, with an example that shows it.
A proof of concept built from IATA's public material, not affiliated with IATA. This page is generated from the model on every build.
Refunds never exceed payments Open question
One guarantee from the model, worked through. It is still open: an example shows the rule as written breaking it, so the business has to decide what the rule should say.
The rule
When a refund is requested against a payment, the system shall accept it only if the refund amount does not exceed that payment's amount.
The guarantee we want
If every refund was accepted against one of the order's payments, the total refunded does not exceed the total paid.
An example
Given one payment of 100.00 USD against order ORD-1.
When two refunds of 60.00 USD each are requested against that payment.
What the rule gives
- First accepted
- yes
- Second accepted
- yes
- Total refunded
- 120.00 USD
Lean computes this result from the rule on every build.
The question for the business
Does the limit apply per refund, cumulatively per payment, or cumulatively per order, and is a refund above the amount paid ever allowed, for example as a goodwill credit?
Take the five-step tour Read “Accepting a refund” in the review document
Where to start
Each page shows the same model from a different side. Pick the one that fits what you do.
You decide business rules
Questions for the business
The open questions and decisions, ranked by how much of the model each answer reaches.
You build airline systems
Requirements and their checks
A chapter per requirement, with its acceptance criteria and the Lean that checks each one.
You want a traveler's view
Verified Airline
A fictional airline's policies, written from the model, with every fee and refund computed by it.
The model's status today
The model is a set of cards: rules written in Lean, guarantees about those rules, and candidate rules taken from IATA's public material. A proven guarantee holds for every input, and an open question is a guarantee the rules as written do not meet. A candidate rule needs a business decision, is ready to build, or waits on other rules.
73
rules in the model
203
guarantees proven
60
open questions
67
need a business decision
7
ready to build
1
waiting on other rules
Decide these first
The three open questions and decisions with the most cards depending on them, so an answer reaches furthest.
- 51 cards in 7 areas: Payment, Change and cancellation, Delivery, Offers and prices, Order creation, Ancillaries, Accounting
- 22 cards in 6 areas: Payment, Change and cancellation, Delivery, Order creation, Ancillaries, Airline change
- 22 cards in 1 area: Accounting
See the top ten on the progress page
Every part of the site
The bar at the top links them all.
Guided tour
Start here if the model is new to you. The tour shows how much the model holds, how its areas build on each other, the decisions that reach the most cards, and one open question with the example that breaks it.
Progress
Every rule, guarantee and candidate rule with its status, grouped by area: 336 cards in Lean and 75 candidates from the ONE Order survey. Of these, 60 are open questions, and 67 candidates need a business decision.
Decide these first Open questions In the model today Candidates
Review document
The rules in plain words, a chapter per requirement: 55 requirements with 253 acceptance criteria, 184 of them proven. Each criterion shows the Lean that checks it, and try-it panels run some of the rules in your browser.
Explore
How the rules depend on each other: 432 cards in 12 areas, counting the definitions the rules rest on, with 973 dependencies between them. Click a card to see what it uses and what builds on it.
Verified Airline
A fictional airline's site, written from the model in a traveler's words. Every fee and refund on its policy pages is computed from the model, and a button shows the requirement behind each answer. The site has its own repository and reads the model's files from /airline-data/.
Specs and data
The requirements as specs in Kiro's format, with acceptance criteria in EARS, and the same criteria as a spreadsheet. The blueprint and the survey of ONE Order are where the candidate rules come from.