Hi Arian,
Very interesting process! TLA+ is an open source project itself, so it is neat to see how involved the contributor vetting process can get. I took a look at your spec. It is quite nice and I only have minor feedback:
- TLA+ has built-in boolean values, defined as TRUE and FALSE. The set of both of them (for type invariant purposes) is BOOLEAN. You can probably use booleans for variables like confirmedFreeTime.
- The Debian validation process seems somewhat sequential. As you probably found, it is slightly annoying keeping track of sequential process state in TLA+ (your "applicationState" variable functions as a kind of program counter). For this reason, TLA+ has a variant called PlusCal which enables you to express this sequential flow in an imperative language instead. It transpiles to TLA+, and generates code fairly similar to what you wrote. However, using PlusCal is strictly optional here.
- Your TypeOK is more of a safety property than a type property (although the difference is informal). Probably I would make your TypeOK invariant look more like some conjuncts of expressions like confirmedFreeTime \in BOOLEAN, and then call your current TypeOK invariant something like Safety or just Invariant or Inv.
- For fun, you could try to think of a temporal property for this specification. That would require you to define fairness assumptions on your actions, which is kind of amusing because we are asserting fairness properties on a person's actions instead of a computer's actuals as per usual. A temporal property could be (for example) "every application is eventually accepted, under the assumption that the candidate eventually makes progress on each individual step".
All in all an excellent first spec!
Andrew Helwer