Verified Air

Guided tour · 5 steps

A tour of the model in 5 steps

The business rules for airline offers and orders are written in Lean, a language that checks proofs. This tour shows how much the model holds, how its parts depend on each other, and where it needs a decision from the business. Each step links to the page where you can look further.

Step 1 of 5

The cards in the model, by status

The model is a set of cards: definitions and rules written in Lean, guarantees about those rules, and candidate rules found in IATA's public ONE Order material. The dependency graph has 432 cards in 12 areas, and the build gives each one a status.

357 cards are in Lean. 204 guarantees are proven: Lean checked a proof that holds for every input. 60 are open questions, and 67 candidate rules need a business decision before they can be written.

93
modelled
204
proven
60
open question
67
needs a decision
7
ready to build
1
waiting

See every rule and guarantee on the progress page

Step 2 of 5

How the areas build on each other

The cards fall into 12 areas, the sections of the blueprint. The foundations sit at the top, and each layer builds on the ones above it. An arrow runs from an area to an area that builds on it, thicker for more dependencies. Click an area to read its summary.

12 areas in 5 layers, with an arrow from each area to the areas that build on it.Order creation and information builds on Change and cancellation: 5 dependenciesOrder creation and information builds on Payment: 5 dependenciesChange and cancellation builds on Delivery and fulfilment: 5 dependenciesDelivery and fulfilment builds on Payments and refunds: 5 dependenciesOffers, prices and conditions builds on Order structure and status: 6 dependenciesOffers, prices and conditions builds on Payment: 6 dependenciesOffers, prices and conditions builds on Change and cancellation: 6 dependenciesAncillaries, seats and bundles builds on Core concepts: 6 dependenciesCommission, accounting and settlement builds on Order structure and status: 6 dependenciesOffers and orders builds on Core concepts: 7 dependenciesAncillaries, seats and bundles builds on Offers and orders: 7 dependenciesAncillaries, seats and bundles builds on Change and cancellation: 7 dependenciesAirline-initiated change builds on Order structure and status: 7 dependenciesDelivery and fulfilment builds on Change and cancellation: 7 dependenciesPayment builds on Delivery and fulfilment: 7 dependenciesPayment builds on Core concepts: 7 dependenciesPayment builds on Order structure and status: 7 dependenciesCommission, accounting and settlement builds on Delivery and fulfilment: 7 dependenciesAirline-initiated change builds on Delivery and fulfilment: 8 dependenciesOrder creation and information builds on Core concepts: 10 dependenciesChange and cancellation builds on Core concepts: 11 dependenciesDelivery and fulfilment builds on Order structure and status: 11 dependenciesPayment builds on Payments and refunds: 11 dependenciesChange and cancellation builds on Payments and refunds: 12 dependenciesAirline-initiated change builds on Change and cancellation: 12 dependenciesAncillaries, seats and bundles builds on Order structure and status: 13 dependenciesCommission, accounting and settlement builds on Payments and refunds: 13 dependenciesOffers, prices and conditions builds on Core concepts: 15 dependenciesOrder creation and information builds on Offers and orders: 20 dependenciesOrder creation and information builds on Order structure and status: 20 dependenciesChange and cancellation builds on Order structure and status: 22 dependenciesOffers, prices and conditions builds on Offers and orders: 23 dependencies810111111121213131520202223Core concepts8 cardsModelled: 7Proven: 1Pilot offers and orders12 cardsModelled: 9Proven: 3Pilot payments and refunds5 cards · 1 openModelled: 4Open question: 1Order structure21 cards · 2 openModelled: 6Proven: 12Open question: 2Ready to build: 1Payment43 cards · 3 open, 10 to decideModelled: 8Proven: 22Open question: 3Needs a decision: 10Change and cancellation44 cards · 6 open, 13 to decideModelled: 7Proven: 16Open question: 6Needs a decision: 13Ready to build: 1Waiting: 1Delivery36 cards · 2 open, 8 to decideModelled: 10Proven: 16Open question: 2Needs a decision: 8Offers and prices53 cards · 7 open, 6 to decideModelled: 8Proven: 28Open question: 7Needs a decision: 6Ready to build: 4Order creation50 cards · 9 open, 11 to decideModelled: 8Proven: 22Open question: 9Needs a decision: 11Ancillaries53 cards · 11 open, 10 to decideModelled: 8Proven: 24Open question: 11Needs a decision: 10Airline change39 cards · 9 open, 3 to decideModelled: 8Proven: 19Open question: 9Needs a decision: 3Accounting68 cards · 10 open, 6 to decideModelled: 10Proven: 41Open question: 10Needs a decision: 6Ready to build: 1
Arrows stand for five or more dependencies. A dashed arrow points back to an area that comes earlier in the layers.

Open the area map · count the dependencies in the matrix

Step 3 of 5

The decisions that reach the most cards

60 open questions and 67 candidate rules wait for the business. Some sit under many other cards, so an answer to them reaches further. These five have the most cards depending on them, directly or through other cards.

  1. Committing to pay nothing
    C-12Needs a decisionPayment
    51 cards in 7 areas: Payment, Change and cancellation, Delivery, Offers and prices, Order creation, Ancillaries, Accounting
  2. Stored value stays in its order
    C-20Needs a decisionChange and cancellation
    22 cards in 6 areas: Payment, Change and cancellation, Delivery, Order creation, Ancillaries, Airline change
  3. Requesting a clearance
    C-160Needs a decisionCommission, accounting and settlement
    22 cards in 1 area: Accounting
  4. Transferred services keep the order balanced
    C-19Needs a decisionChange and cancellation
    16 cards in 5 areas: Change and cancellation, Delivery, Order creation, Ancillaries, Airline change
  5. Refunds never exceed payments
    Open questionPayments and refunds
    15 cards in 3 areas: Payment, Change and cancellation, Accounting

See the top ten on the progress page

Step 4 of 5

Refunds never exceed payments

If every refund was accepted against one of the order's payments, the total refunded does not exceed the total paid. This guarantee is open: the rule as written does not meet it. An example shows the rule breaking it.

The 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.

Then each refund is accepted, and together they return 120.00 USD, more than was paid. This is the counterexample for refunds_le_payments.

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.

Open point: 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?

Read Accepting a refund in the review document, where you can try the rule

Step 5 of 5

The cards that depend on this question

15 cards build on this guarantee, directly or through other cards, in 3 areas: Payment, Change and cancellation, Accounting. Whatever the business decides reaches each of them, which puts it at number 5 in the ranking. The cards it uses directly are to the left; the cards that build on it are to the right, nearest first.

Depends on directlyThis cardBuilds on it directly2 steps on3 steps onPaymentChange and cancellationAccountingPaymentChange and cancellationAccountingChange and cancellationAccountingAccepting a refundAccepting a refundModelledTotals paid and refundedTotals paid and refundedModelledRefunds never exceed paymentsRefunds never exceed paymentsOpen questionRefund as a negative paymentRefund as a negative paymentC-138 · Needs a decisionRefundable payment surchargesRefundable payment surchargesC-137 · Needs a decisionRefunds across payment methodsRefunds across payment methodsC-17 · Needs a decisionPaid or partly paid orders need an offerPaid or partly paid orders n…C-87 · ModelledMoney balance of an orderMoney balance of an orderC-146 · Open questionAllocating a payment across itemsAllocating a payment across…C-133 · Needs a decisionPaying with a voucherPaying with a voucherC-141 · Needs a decisionCancellation offers stay within paymentsCancellation offers stay wit…Open questionChanges made without an offerChanges made without an offerC-97 · Needs a decisionSettling money the airline owesSettling money the airline o…C-90 · Needs a decisionStored value belongs to payerStored value belongs to payerC-99 · Needs a decisionMoney balance when cancellation amounts are checkedMoney balance when cancellat…ProvenRefunds within paymentsRefunds within paymentsOpen questionStored value is used onceStored value is used onceC-92 · Needs a decisionRefunds within payments when cancellation amounts are checkedRefunds within payments when…Proven

For some open questions, Lean already proves the guarantee under one reading of the sources. The card then shows that reading under If we decide this, on the Explore page and on its area's summary. 24 of the 60 open guarantees have one.

Open its neighbourhood on the Explore page

Other pages