Docstrings use Verso markup (doc.verso = true for the whole package). Code spans carry roles: {name} for model declarations (a rename breaks the docstring), and {lit} or {lean} for literals and terms. Status/Main.lean turns the option off, since its comments are for developers.

Generated Verso modules. The plan names one Generated.lean. Each Verso chapter is its own module, so the script writes three: Review/Review/Generated/Guarantees.lean, Examples.lean and Ears.lean. They are gitignored and regenerated on every build, as are blueprint/src/*.generated.tex. (Decision 29 later replaced the Guarantees and Examples chapters with one chapter per requirement.)

Verso layout. The Review library has srcDir = "Review", so its chapters sit in Review/Review/. The review-doc executable's root is Review/Main.lean. Verso writes build/review/html-multi/, and that directory becomes the site root.

Statement in the Guarantees chapter. Each guarantee shows its Lean statement twice: in the {docstring} box, which renders the full signature, and in a checked ```lean block (#check @name). (Decision 28 later removed the #check block.)

leanblueprint new answers: checkdecls yes; doc-gen4 no (the Verso document takes the place of API docs); Jekyll home page no; CI yes. The generated blueprint.yml and the template's other three workflows were then folded into ci.yml.

Graph colors. Proven theorems get \leanok on both the statement and the proof, so they fill dark green. The open theorem gets neither. By default leanblueprint would fill it light blue ("ready to prove"); \graphcolor{can_prove}{}{No} in macros/web.tex leaves it unfilled. Its blue border still says the statement is ready.

Blueprint to Verso links. leanblueprint links each \lean{} name to {dochome}/find/#doc/<name>. \dochome{../docs} points that link at pages/docs/find/index.html, a small redirect into Verso's own find/?name=<name> page, which jumps to the declaration's section.

CI step order. render_status.py runs before the Verso build, because it writes chapters the build imports. leanblueprint web runs before checkdecls, because web writes the lean_decls file that checkdecls reads.

TeX in CI. CI installs TinyTeX instead of texlive-full, matching the local setup, which also uses TinyTeX. It is far smaller, and its default package set built the PDF with no additions. CI runs tlmgr update --self first, because the installer's tlmgr refused to install packages until it was updated. CI's TinyTeX has fewer packages than the local one, so CI installs every package the local PDF build loads, read from print.fls. CI also caches the compiled Verso packages, keyed on lake-manifest.json.

Pages deploys from main only. Pull requests build and upload the site but do not deploy it.

The repository is public. The plan asked for a private repository. GitHub refused Pages for it on this account's plan ("Your current plan does not support GitHub Pages for this repository"), so the repository was made public with Sam's approval, and Pages was enabled with GitHub Actions as the source. The deploy job still checks the repository variable PAGES_ENABLED (set to true), so a fork or a copy without Pages keeps a green build.

EARS outputs. The status executable writes build/ears.csv along with ears.md. "Proven by" lists every theorem whose statement mentions the rule, so OO-001 lists both accept theorems.

Branch protection is not turned on for the POC. CODEOWNERS names @samdengler on every path.

Acceptance demos. The demos (fixing the refund rule, changing a #guard, renaming accept) were run locally on a branch or as uncommitted edits, then discarded, as the plan says.

Requirement specs and acceptance criteria (added after the plan, at Sam's request). The requirement specs are Markdown in the layout Kiro reads, so they can be used with Kiro's spec-driven flow; ears.csv stays as an extra export. They were first called Kiro specs; the name changed so that it does not suggest Kiro is required. Decisions:

• One spec folder per Lean module that holds rules, named from the namespace and the module's title, for example offer-order-accepting-an-offer. The module docstring becomes the introduction.
• Criterion IDs extend the rule's ID (OO-001.1) and are written by hand in the docstring, like the rule IDs, so they never renumber.
• The EARS text stays in standard form in the docstrings ("When X, the system shall Y"). The spec files print it in Kiro's notation (WHEN X THE SYSTEM SHALL Y, IF X THEN THE SYSTEM SHALL Y).
• A criterion's status is computed from what checks it, but whether a theorem's statement covers the criterion's wording is a review question: the @[checks] tag is authored.
• An example that checks an open criterion is labelled a counterexample.
• Four criteria (OO-002.2, OO-002.3, OO-002.5, OO-003.1) have no theorem or example yet and are shown as not checked. Adding theorems for them would change the proven count the acceptance criteria fix at three. (Decision 29's transitionTable example later checks the first three.)
• Only requirements.md is generated; design.md and tasks.md belong to the team using the spec.

Implementation checks (added after the plan, at Sam's request). The target teams use Java, so options 1 and 2 are shown on a Java implementation; option 3 needs Rust because Aeneas translates Rust.

• The oracle runs the model in Lean's interpreter, loading Oracle.Handle from its .olean files like lake exe status does. Compiling the rules into the executable would link Mathlib's native code.
• The JSON shapes are the ones Lean derives for the model's types, so the oracle adds no mapping of its own. The Java tests do the mapping.
• Lean's amounts are natural numbers; Java uses long. The generators produce only non-negative amounts below 50,000, so the two agree on every generated input.
• Inputs are generated close together (instants around expiry, three shared payment IDs) so that boundaries and repeated refunds come up often.
• The open theorem's property uses jqwik's @ExpectFailure, the Java counterpart of @[open_question].

Aeneas and the move to Lean v4.35.0. The proofs about the Rust code need the model and Aeneas's Lean library in one build, and that library is pinned to Lean and Mathlib v4.35.0. The repository moved from v4.36.0-rc1 to the v4.35.0 release, which Verso also tags. The status counts, the review document and the conformance vectors came out the same.

• The Aeneas binary and its Lean library are pinned to the same release, nightly-2026.10.26-da2b22e. Aeneas publishes nightly releases only.
• The Rust code uses numbers for references, because Aeneas handles integers and not strings. The refund theorem therefore takes any one-to-one naming of numbers as strings.
• accept has no Rust version, because it joins strings to make order references.
• The generated Lean in Verify/Rust/ is committed, like the requirement specs, and CI checks that it matches a fresh translation.

A progress page at the site root. The blueprint's layout is fixed by leanblueprint and reads like a mathematics paper, so business readers get their own page. scripts/render_progress.py generates it from the same data as the blueprint, so it adds nothing that can drift. The review document moved from the site root to /review/, and its links to the blueprint and the CSV files now go up one level.

• Cards are grouped by blueprint section, and the graph colors become words: modelled, proven, open question, needs a decision, ready to build, waiting.
• The open refund theorem's blueprint text was split into a counterexample and an open point, the labels the page and the candidate nodes share.
• The dependency map is drawn top to bottom without area boxes. With the boxes, Graphviz routed long edges across the areas.
• The review document has the same look. Review/review.css overrides Verso's theme variables and is read by lake exe review-doc when it runs, so a change to the stylesheet needs no Lean rebuild. A small Verso role, {status "proven"}[Proven], gives the generated chapters the same status labels as the progress page.
• Each docstring is shown as a card: a plain label (object, rule, calculation, guarantee, example), the description, the fields or values as a list, and the Lean form in a small footer. Guarantees are titled with their blueprint titles and examples with their names in words, and the sidebar lists sections without every Lean name. The Guarantees chapter no longer repeats each statement in a #check block, since the docstring card already fails the build if the name is wrong.

The review document is organized by requirement (added at Sam's request, with the readable examples, the state diagram and the try-it panels). Business readers think one rule at a time, so each requirement gets a chapter: the rule, a table of how each acceptance criterion is checked and its status, the guarantees, the examples and any open question. Objects and the EARS table follow as reference chapters.

• scripts/render_status.py writes the chapters as Review/Review/Generated/OO00n.lean and fails if Review/Review.lean does not include one of them.
• Examples state Given, When and Then in their docstrings. Their results are parsed from the value Lean prints and shown in business terms: amounts as 245.00 USD, instants as UTC times, lists of records as tables. A result that does not parse is shown as Lean printed it. The two examples that returned tuples now return records whose field names label each part.
• A new example, transitionTable, runs every delivery state and event through step. Its #guards fix the three allowed moves and the count of 12, and the review document draws the state diagram from its value. It also checks OO-002.2, OO-002.3 and OO-002.5, which no example checked before.
• The try-it panels call step and accept_refund from impl/rust, compiled to WebAssembly through a wrapper crate, impl/wasm. The proofs in Verify/RustRules.lean are about those two functions; the wrapper and the page's script are not proved, and the panels say so. The refund panel adds up the accepted refunds itself to show the open question.
• The review document's front page shows a card per requirement, with its user story and the computed status of its criteria, then the reference chapters as a list. scripts/render_status.py writes the cards into Review/Review/Generated/Front.lean. Verso's own chapter list is hidden there, since the sidebar shows it.
• Every page has the same bar at the top: the site name and links to the progress page, the review document, the dependency graph and GitHub. scripts/site_nav.py defines it. The progress page uses it directly, scripts/assemble-site.sh runs it on the blueprint's pages to replace their header (keeping the blueprint's contents button), and Review/review.js builds the same bar inside Verso's header, which keeps Verso's search box.
• The dependency graph has its own page, /graph/, drawn by scripts/render_graph.py in the style of the progress page. The script places the nodes in rows below the nodes they use, at most 14 to a row; the page draws flat cards with a status line and light connectors. Every status has its own color, used the same way on every page: In Lean magenta, Proven green, Open question red, Needs a decision amber, Ready to build blue, Waiting grey and dashed. Finished states get a lighter rim than the ones that need attention. The colors were checked against each other for color-blind readers, and every status also carries its label. A reader can move and zoom, and clicking a card dims the rest and opens a panel with its statement, open point, source, Lean names, and what it depends on and what uses it. leanblueprint's graph stays at /blueprint/dep_graph_document.html for the blueprint's own legend.
• Every card and map box on the progress page is a link, resolved through Verso's own lookup (review/find/?…) so a moved chapter keeps working: a rule opens its requirement chapter at the top, a guarantee opens its section heading in that chapter (tagged guarantee-<name> by scripts/render_status.py), and a candidate opens its node in the dependency graph. A graph address ending in # and a node's label, such as graph/#def%3Ac06-item-status, opens with that node selected; selecting a node updates the address, so a selection can be shared.
• The blueprint follows the reader's dark-mode setting too, through blueprint/src/extra_styles.css. In the dependency graph only the black edges and text change, and blue borders lighten; the green fills keep the meaning the legend gives them.

Renamed from business-rules-verified to airline-order-verified. The new name says what the rules are about without using IATA's name, which could suggest the project is IATA's or endorsed by it. The site moved with the repository to samdengler.github.io/airline-order-verified/. GitHub redirects the old repository URLs; GitHub Pages does not redirect a renamed project's site. The site is called Airline Order in its top bar, page titles and document titles, with a plane as its mark and tab icon (PLANE_PATH in scripts/site_nav.py, repeated in Review/review.js).

The review-doc program loads the document when it runs. CI spent most of its time compiling about 2,800 Mathlib modules to native code so that review-doc could link the document, whose rules import Mathlib.Tactic. Review/Main.lean now imports only Verso and Review.Status (the document's own extensions, which Verso must have compiled in), and loads the compiled Review modules with importModules, as lake exe status and lake exe oracle already do. The program builds in 471 jobs instead of 6,767, and the HTML it writes is byte for byte the same.

A starting-small branch, milestones and a graph history. The starting-small branch and tag snapshot/starting-small keep the version to propose for an internal pilot, while main grows toward as much of ONE Order as the public material allows. Each milestone gets an annotated tag milestone/<name> and a snapshot of the graph in history/, written by scripts/graph_history.py, which also computes one layout for every node that has appeared so nodes keep their place across snapshots. The first three milestones were recorded after the fact from the blueprint's history. The site publishes the current graph at /graph/graph.json. docs/motion-brief.md describes how the snapshots can drive a motion piece about the graph's growth.

ONE Order as published, in its own namespace. Rules.OneOrder models the standard as IATA's public guide describes it: services with a service status and a delivery status, order items and orders, accepting an offer for several passengers and segments, and the item and order status rules (ONE-001 to ONE-003). The pilot rules in Rules.OfferOrder and their Java and Rust checks stay as they are; a later theorem can relate the two. The guide says which of five delivery statuses hold value and is silent on the other eight, so the model takes the answer as a parameter (ValueReading). A guarantee about value is proven only when it holds for every reading the guide allows; where a reading breaks it, the guarantee is open and an example shows the case. Open guarantees outside the pilot get a generated chapter, Questions from the ONE Order rules. Chapters find their guarantees and examples by criterion ID in any namespace, and section tags carry the namespace when a name repeats.

A second survey round, C-24 to C-161. Eight surveys, one per area, read each area's public pages in full and returned 160 candidates; 22 duplicates across areas were merged. Every candidate is a blueprint node with its rule, a case to check where the sources suggest one, the open point for vague and silent rules, and links to its pages. docs/one-order-survey.md lists them and docs/one-order-coverage.md maps them to capabilities: every capability with high rule content now has candidates. With 200 nodes, Graphviz laid the dependency graph out in one row many thousands of pixels wide, so scripts/render_graph.py now places cards itself, in rows of at most 14 below the cards they use, ordered to keep connectors short. The progress page links to the graph instead of drawing its own map.

Lenses on the dependency graph. The whole graph shows how much there is; a reader needs a smaller view to follow it. The graph page lays out the cards in the browser, with the same row layout, so it can redraw a subset: one area with the cards it builds on (faded), or one card with everything it depends on and the cards that use it. The lens is kept in the address (?area=Payment, ?focus=<label>), so a view can be shared. Areas are the blueprint sections. A lens by IATA capability code would need the codes on the blueprint nodes; they are in the survey data only.

The ONE Order areas, written in parallel. After the foundations, each area of the coverage map got its own folder, sub-namespace and range of requirement IDs (CLAUDE.md lists them), so several could be written at once. Each was written by an agent in its own git worktree, from a shared brief, and merged onto main by rebase after review and a full site build, with a milestone tag per area. Two were sent back before merging because they proved a guarantee by choosing a reading the sources leave open: creating one order from several offers, and the balance of an order's accounts. The rule for that is now in CLAUDE.md: the undecided part is a parameter, a guarantee is proven only under every reading, and a proven version for one reading is named with _of_ and checks no criterion. The progress cards link to the dependency graph for anything the review document has no page for, using the review's cross-reference index, and the Objects chapter has the ONE Order foundation objects.

A history page. /history/ plays the milestones on the dependency graph: cards appear as surveys find them and change color as areas are written in Lean, with the camera easing out as the graph grows. It is in the top bar, reads the same history/ files as the motion piece (scripts/render_history.py), and keeps the milestone in the address (?m=13). Card titles in the shared layout come from the latest snapshot that has the card.

An Explore page in place of the dependency graph and history pages. With 429 cards the full graph shows how much there is and little else. Most of its dependencies stay inside one area, so the ones between areas reduce to a graph a reader can follow. The top bar's Dependency graph and History links become one link, Explore, which stays at /graph/ so older links keep working. It has five views, kept in the address as ?view=area-map, matrix, all-cards, history and card, with a selected card in the hash as before.

• The area map is the first view: one box per blueprint section, with its status bar and counts, in layers from the foundations down, and an arrow to each area that builds on it, as thick as the number of dependencies. A box opens the area's summary page. Arrows for fewer than five dependencies are left out; the matrix counts them all.
• The layers are set by hand in AREA_LAYERS in scripts/graph_model.py, since no ordering of the areas has every dependency pointing one way. A new blueprint section stops the build until it is placed there. A dependency on an area listed later points back: dashed on the map, and outlined in the matrix, where it sits above the diagonal.
• The dependency matrix counts the dependencies between each pair of areas. Clicking a cell lists the cards behind the count.
• All cards is the earlier graph page, with its area lens, and a lens by IATA capability.
• History is the earlier /history/ page drawn as clusters of dots: a box per area and a dot per card, which appear and change color by milestone. /history/ sends readers to this view and keeps ?m=.
• A card's neighbourhood replaces the focus lens: the card in the middle, what it depends on to the left by distance, and what builds on it to the right, grouped by area, with the side panel's text beside it. Any card link (graph/#<label>) and the search box open it. The neighbourhood shows the cards that build on it directly, and all of them on request.
• The area map, the matrix and the clusters are drawn by the build (scripts/area_views.py); the page's script (scripts/explore.js) draws the full graph and the neighbourhood, and is written into the page with scripts/explore.css.

Decide these first. The progress page ranks the ten open questions and decisions with the most cards depending on them, directly or through other cards, above the open question cards. Ties go to the one whose dependent cards span more areas. Each links to its neighbourhood.

A summary page per area. /area/<slug>/ shows an area's cards by status, the areas it builds on and the areas that build on it, its open questions and decisions with the number of cards depending on each, its requirements with links to their chapters, and its IATA capabilities. Requirements are found through the Lean names on the area's blueprint nodes.

If we decide this. Many open guarantees have a version proven for one reading of the sources, named <open name>_of_<reading> and tagged with no criterion. The build pairs them by name only, and shows the proven theorem's docstring beside the open question, on the card's panel and on its area page, as a choice the business can make. When this was written, 18 of the 58 open guarantees had a pair; python3 scripts/render_areas.py --unpaired lists the others. Three proven _of_ theorems name no open theorem (history_rebuilds_of_oldestFirst, createOrder_guaranteed_of_reprice, recordOutcome_final_of_reading), so their open guarantees show no pair until one of the names changes.

IATA capability codes on the blueprint nodes. Decision 35 noted that a lens by capability needed the codes on the nodes. Each candidate node now ends with a paragraph such as "Capabilities: ORDCAN, ORDCA2.", which scripts/render_progress.py reads like "Source:". The codes for C-24 to C-161 come from the survey data; those for C-01 to C-23 come from the coverage map's "In the model or blueprint" column, leaving out the two rows that say a capability is only close to a node. The names come from docs/one-order-coverage.md, and the build fails on a code it does not list. The All cards view filters by capability, and the area pages list their codes.

A guided tour. /tour/ takes a business reader through the model in five static steps: the cards by status, the area map, the decisions that reach the most cards, the refund question with the example that breaks it, and the cards that depend on that question. The progress page links to it. The build stops if the refund guarantee is no longer open, since the tour's text would then be wrong.

A motion piece rendered with Remotion. docs/motion-brief.md left the tool open. Remotion renders a React composition frame by frame in headless Chrome, so the piece is code that reads the history files. motion/ imports the snapshots, history/layout.json and build/frames/frames.json, checks them against each other, and draws the cards, connectors and counters from them, so no count or status is typed by hand. It follows the storyboard; the brief lists where it departs. Rendering needs Node and a headless Chrome and takes about a minute, so CI does not do it: scripts/render-motion.sh writes motion/out/history.mp4 (1920 by 1080, H.264, about 9 MB) and its poster, both are committed, and scripts/assemble-site.sh copies them to /motion/. They are rendered again after each milestone. The History tab of the Explore page shows the film above the step control. It never starts by itself, so a reader who asks for reduced motion sees the poster until they press play. Remotion is free for individuals, for-profit companies of up to three employees and non-profits, and a larger company needs a company licence (motion/README.md links the terms).

A fictional airline's policy pages. /airline/ shows the model as a traveler would meet it: Verified Airline's policies in plain words, with the Lean model hidden until a reader asks for it. The pages are static HTML with every popover already in the page, so they need no data fetching and read with scripts off. The fares are values of the model's existing Restriction type, evaluated by the model's own functions, so the fare table and worked examples could not be written without the model changing. The model's readings stay open: lake exe airline-facts evaluates every reading and fails if two disagree, and the fares are written so they do not (no expiration dates, no refund that is both full and fixed). The fares are invented. The six rows of the fare table extend the design mockup's four with changes after a missed flight and cancellations after the first flight. The page sources are in airline-site/ because airline/ and the Lean directory Airline/ are one directory on macOS's default file system. A "still being decided" item names its open criterion, and the build stops when that criterion is proven, so the pages never keep a stale caveat.

A home page, with the progress page at /progress/. Decision 28 put the progress page at the site root. By the time the model had 58 open questions and over 400 cards, the page was about 100 screens long, and the open questions alone took 15, each in full and again as a card further down. The root is now a home page: the introduction and status tiles, a card for each part of the site with counts from the build, and the top three of "Decide these first". The progress page keeps every card. Its open questions are one line each, grouped by area, with the example and open point behind a click, and a table of contents beside the page (across its top on a phone) links every section. A script on the home page sends links to the old sections, such as /#found, to the same section of /progress/. On a phone the site bar keeps the plane, which leads home, and drops the site name.

Fixes from the independent critique. A review on 30 October compared every criterion with its theorems and the areas with each other, and found 30 problems. The fixes for the modelling errors:

• Five rules outside Delivery set a service's delivery status directly, so a DELIVERED service could become REMOVED. Every rule that ends a service now goes through Delivery.endWith, which applies the event through the delivery status table and leaves the service as it was when the table refuses the move. delivery_moves_follow_table in Rules/OneOrder/Consistency.lean proves, for every rule that changes a delivery status, that it moves only along the table (ONE-105).
• A cancellation is priced from the items that still hold a live service, so an item a change replaced is not refunded twice (ONE-203.5). The balance of an order still counts value, so an item whose services are all REMOVED HOLD VALUE counts there and not in a cancellation; which of the two a refund follows is open.
• A payment with no payment method is FAILED, and is never accepted (ONE-301.4, ONE-304.7).
• The reading of what an unpaid item becomes at its time limit is now the event that ends its services: REMOVED, REMOVED HOLD VALUE or EXPIRED, with the services cancelled.
• Five criteria written for one reading were removed (ONE-101.5, 703.3, 803.5, 804.6, 805.6); their theorems are _of_ versions with no criterion.

Going through the table made two gaps visible, which are now open questions: the table has no way to cancel a REQUESTED or UNABLE TO DELIVER service, so an unpaid order with one is not closed by cancelling it (ONE-203.2), and a flight the airline cancels can leave a REQUESTED or IN PROGRESS service live (ONE-704.6). The graph snapshot critique-before-fixes records the model as the critique found it, and the milestone critique-fixes the model after the fixes.

The film plays one step at a time, and the build stops when it is stale. The film was rendered before the critique's first snapshot was recorded, and nothing noticed. Its storyboard treated every milestone after the second survey as an area being written, so it could not even be rendered again. It now has a step for the review and one for the fixes. scripts/render-motion.sh records the milestones and a hash of motion/src/ in motion/out/history-film.json, and scripts/render_graph.py stops the site build when they no longer match. The History tab plays the film in the nine steps of STEPS in motion/src/story.ts, listed under it with their start times: a step plays and stops on its last frame, and buttons go to the previous or next step, replay one, or play to the end. The story checks that nothing moves in the half second before each pause, so the page stops on a still frame with its caption in full. motion/README.md shows the film's last frame, linked to the History tab, with the same list of steps. A GIF of the film for GitHub was tried and left out: at a size where captions stay readable it was 8 MB, and the site plays the MP4.

Renamed to Verified Air. The site is called Verified Air, from "rarefied air", and the repository is verified-air, so the site moves to samdengler.github.io/verified-air/. As with decision 30, GitHub redirects the old repository URLs and GitHub Pages does not redirect the old site. The plane stays as the mark. The home page's heading names the subject, rules for airline offers and orders, since the site's name no longer does. The fictional airline of /airline/, called Parliament Air until then with a serif P as its mark, is now Verified Airline with the site's plane in its own indigo. The Lake package keeps the name airline-order-verified, which nothing outside the build shows.

Verified Airline has its own repository. The airline's pages moved from /airline/ to samdengler/verified-airline, served at https://samdengler.github.io/verified-airline/, so the airline can grow a booking flow and a customer support widget. Those need a JavaScript toolchain, and the widget a server, which do not belong in this repository's CI. The fares stay in Airline/Fares.lean, since they are values of the model's types and need Lean to evaluate. This repository publishes what the pages read under /airline-data/: facts.json, and model.json from scripts/export_airline.py, with every requirement's statuses and absolute links into the review document. The airline's repository commits a copy, so its version of the model is pinned and each update shows as a diff. Decision 45's check still stops a stale caveat: scripts/check-airline.sh renders the airline's current wording against each build here and fails if it calls a proven criterion still being decided, so the wording changes there before the proof is pushed here. The old addresses under /airline/ send readers to the same pages on the new site.

A home page for a reader with no context. The home page opened with Lean and proofs, then six count tiles, so a reader new to the project met the method and the numbers before the problem. It now says what the project is in plain words: an airline's offers and orders, IATA's ONE Order standard written in prose, and Lean checking rules written as code. One open guarantee follows, worked through from the model: the rule's EARS statement, the guarantee from its blueprint card, the example's Given and When, what Lean computes for it, and the open point. It is the same guarantee as the tour's step 4 (QUESTION in scripts/render_tour.py), so the build stops for both pages when it is proven. Four links by kind of reader come next, then the status tiles with a sentence on what each status means. The not-affiliated line moved under the introduction.

Verified Airline is served at air.dengler.io. The airline's site moved from GitHub Pages to https://air.dengler.io/, an Angular app on AWS whose design is recorded in the airline's own README. The top bar, the home page card, the review document's bar and the old /airline/ addresses here now lead there. The files the site reads stay at /airline-data/, and scripts/check-airline.sh still renders the airline's wording against each build.

Each fare fact has a theorem. Verified Airline's support chat answers fare questions through an Automated Reasoning check whose rules come from facts.json, and shows the facts an answer rests on. A fact was a value Lean evaluated for one journey at one instant, and no theorem named it. Airline/Theorems.lean now states each change and cancellation fact for every journey and instant in its stage after the fare terms start, every item or change request, and every reading of the guide, since the chat's rules say "returns the full price paid" for any price. A theorem about the evaluated journey alone would be an example. Each proof unfolds the rule in force with simp. /airline-data/theorems.json lists each fact's theorem with a link to its line; facts.json keeps its shape. Lean checks the facts; whether an answer's words state them is still the Automated Reasoning check. The chat's general rules (the fare difference, the amount due on a change, the refund limit) rest on theorems in Rules whose statements are not yet matched to the chat's wording, so the file does not list them.

The support chat's policy is written here, and every rule has a theorem. Verified Airline's support chat checks answers with an Automated Reasoning policy generated from the model's files. Its exporter moved from the airline's repository to scripts/export_airline_policy.py, which writes ar-policy.json, ar-rules.json and ar-checks.json under /airline-data/ beside the files they come from. The policy is now one of the model's files, built and checked with the theorems it cites. Each rule in ar-rules.json names the theorems that prove it, and the export stops if one has none. The general rules got theorems in Airline/Theorems.lean, stated for every rule list: the fare difference of an allowed change, the amount due on one, and the two halves of acceptRefund's limit, with theorems for what the chat takes as given (money is never negative, every fare's price is positive). lake exe airline-facts --theorems lists them under general and checks them as it checks the facts' theorems. Matching them to the chat's wording found one gap: the amount due was the fee plus the fare difference whenever the new flight costs more, but under the reading that waives a fee above the refundable value, that holds only when the price paid covers the fee. The rule now says so. Every Verified Airline fare in the worked examples costs more than its fee, and the policy's 40 tests in Bedrock still pass.

Every rule names its sources, and a confirmation goes out of date when the rule changes. A model written from documents can be wrong where a document is wrong or where it was read wrong, and a proof does not catch a rule and its guarantee mistranslated the same way. So each rule records where it came from and whether anyone outside the model has confirmed it. @[source "<key> ..."] names the sources by key, and Rules/Core/Sources.lean lists each key once with its kind, title and link. The kinds run from a published standard to the airline's own policy, a rules engine, code, tests, production data and a subject matter expert, plus the modeller for a rule no source states. The attribute rejects an unknown key where it is written, and lake exe status fails on a rule with none. The first keys come from the blueprint's Source: paragraphs: a rule names the pages cited on the nodes for it and for the theorems that check its criteria. The three pilot rules name only pilot-slice, since they were simplified and invented for the proof of concept, and ONE-105 also names model-consistency, the critique's fix in decision 47. @[confirmed sme "2026-11-03" "<who>" "<what was confirmed>" "<fingerprint>"] records a confirmation by a subject matter expert, production data (data) or a second independent source (crosscheck). The fingerprint is a hash of the rule's docstring, type and definition at the time, copied from build/status.json. When the rule changes, the fingerprints differ, the rule shows as confirmed but out of date, and lake exe status warns until someone confirms it again or the tag is removed. A Lean or Mathlib upgrade that elaborates a rule differently changes its fingerprint too. Each requirement chapter and each spec now lists the rule's sources and says whether it is confirmed, the specs index counts the rules by provenance, and provenance.csv has a row per rule. No rule carries a confirmation, because none has happened.