Under the hood: records in, proof out.

Everything Airmass knows about your aircraft is a record: setup, equipment installations and removals, meter readings, logbook entries, scans, signatures and owner determinations. Records are only ever added. Nothing stored is a status: there is no due-date table to go stale.

Frozen wording, appended corrections

When an entry is signed, its exact text is hashed and the signature covers that hash. The wording can never change after that. A mistake is fixed by a new correction record that points at the old one, so the history always reads back as it was.

Signatures

Every signer confirms with their own passkey: an owner with Face ID or Touch ID on their own iPad, iPhone or Mac, a visiting mechanic on their own iPhone or Android phone by scanning a code on the iPad, or with a security key. A key unique to that signer signs the exact wording. A drawn signature alone is not used, because it shows only appearance. The printed page shows the signer, the signer's certificate and a short verification code. Or sign the printed entry in ink and scan it back in. The design follows the FAA's electronic signature guidance in AC 120-78B: unique to the signer, clear intent, cannot be copied or altered, traceable.

From records to facts

Before the kernel sees anything, each record becomes typed facts, for example "transponder test, passed, 11 Sep 2024, by a repair station". Every fact keeps a pointer to the record and page it came from. That pointer is what lets every answer show its source.

The newest entry governs

For a recurring item, the newest entry of that kind by a person allowed to sign is the one that counts. Two entries on the same day that disagree give "can't tell", never a guess.

Each regulation section that applies to a Part 91 aircraft is one Lean file. Lean is a programming language and proof checker; a rule with any error will not compile. Every paragraph of the regulation sits above the code that encodes it, so a reader can check one against the other.

-- 14 CFR 91.413(a): ATC transponder tests and inspections
-- "No persons may use an ATC transponder ... unless, within the
--  preceding 24 calendar months, the ATC transponder has been
--  tested and inspected and found to comply with appendix F ..."
def r91_413a : Rule := recurring {
  applies   := installed .transponder ∧ uses .transponder
  entry     := .transponderTest
  window    := .calendarMonths 24
  signers   := authorizedBy "91.413(c)"
  supersede := .newestSameKind   -- same-day disagreement: can't tell
}

theorem no_test_never_met (r : Records) (d : Date)
    (h : r.entries .transponderTest = []) :
    eval r91_413a r d ≠ .met := by
  simp [eval, recurring, h]

A shared pattern library

Most rules are one of a dozen shapes: a recurring inspection or test, required equipment, who may sign, inoperative equipment allowed under conditions, a duty triggered by an event, a document that must be aboard. Each shape is written and proved once. A section then states only its own parameters, and any reading that differs from the pattern must be a named exception with its source.

Proofs

The build proves safety properties straight from the regulation text, for example that an aircraft with no transponder test on record can never show the test as met. When a paragraph is amended, the build proves the change touched only that paragraph.

Generated, never hand-edited

The rule pack the app reads, the plain-English reading, the block view and a change summary are all generated from the Lean file. Nothing is edited by hand, so nothing drifts out of step.

Proofs check a rule's structure. The sweep checks its meaning. Before any rule pack ships, it is run against thousands of cases:

• Confirmed cases, whose answers were worked out by hand from the regulation text and FAA guidance.
• Boundary cases: the day before and the day after a due date, the last hour of an hours window, a same-day conflict.
• Random records, generated in bulk and compared between the Lean model and the shipping kernel.
• Mutations: deliberately broken rules that the sweep must catch.

If any answer changes that should not, the pack does not ship. Each confirmed case lists the rulings it depends on, so when a ruling changes, the cases it affects are flagged.

Airtight is a small evaluation engine. It is the only part of Airmass that decides an answer. It takes the facts, the rule packs for the editions in force, and a question date, and returns one of four results for every rule.

Can't tell is never compliance

Missing information never turns into a pass. If the records cannot prove a rule is met, you see what is missing, by name.

Locked and signed

The kernel is locked. It changes only through a signed release, and random-record tests compare it against its Lean model so a property proved in Lean holds for what ships. The same records and the same date always give the same answer.

Every regulation paragraph keeps each edition with the date it took effect. Today the experimental rules reach back to 1 January 1997, and the rest are being extended to the same date. Each edition keeps the Federal Register notice that changed it and the FAA interpretations attached to it. The kernel picks the edition in force on the question date, so a 2019 entry is judged by 2019 rules.

The kernel runs on your device. Your records are stored on your Mac and iPad and, if you choose, in your own private iCloud database. There is no Airmass account and no Airmass copy of your records.

The app looks up your N-number directly in the FAA's public registry and reads airworthiness directives from the Federal Register. Once a day, Airmass publishes the FAA's list of safety bulletins as a file the app downloads and matches on your device. Nothing about you or your aircraft is sent to us.