Feedback wanted: Modeling Debian's New Member Process

[Arian Ott]

Hi,

I'm a software developer, 3 days into TLA+. As a learning exercise I
modeled Debian's New Member process (Steps 1-7) based on
https://www.debian.org/devel/join/nm-step1 ff.

The shift from "how do I build this" to "what must always be true"
is new to me, so I wanted to try it on a real process I care about.

The spec covers:

- Prerequisite checks (key signing by >= 2 DDs, >= 2 advocates,
DFSG/SC agreement, Salsa account, free time)
- Application submission with guards enforcing all prerequisites
- AM task/skills verification and report
- Front desk review with reject/resubmit loop
- DAM approval or rejection

9 variables, 13 actions, 9 invariants. TLC explores 368 states, all
invariants hold.

One result that surprised me: the DAM reject path is unreachable.
All rejection grounds from the wiki (inadequate identification,
failure to agree to principles, incomplete tasks) are enforced as
guards before submission. So by the time the DAM sees the application,
there's nothing left to reject. I didn't plan for that, however TLC found
it.

Feedback and patches welcome :D

Link to spec:

https://github.com/Arian-Ott/debian-process/blob/master/nmprocess/
nmprocess.tla

Happy Hacking!
--
Arian Ott
aria...@ieee.org

[Andrew Helwer]

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/5119411.GXAFRqVoOG%40office.arianott.com.

[Arian Ott]

Hi Andrew,

thanks for your response!

On Friday, 10 April 2026 20:24:54 British Summer Time Andrew Helwer wrote:
> Very interesting process! TLA+ is an open source project itself, so it is
> neat to see how involved the contributor vetting process can get.

Yeah, open source projects are wonderful. At Debian, we have a strict vetting
process to keep supply chain attacks and malicious contributions to a bare
minimum. Becoming a core developer is a long process which even involves
meeting at least two vetted developer in person to verify IDs :)

Fortunately, you don't have to be a developer to contribute to Debian. In that
case a Debian Developer reviews the code and uploads it for you.

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

Makes sense. Boolean values are more meaningful.

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

+1

I just looked into PlusCal and it is more straightforward than writing plain
TLA+ in that case. From my perspective rewriting the process in PlusCal is
faster than in TLA+.

In the docs there are two flavours (P and C syntax) of PlusCal specified.
Despite the braces, are there meaningful differences?
If there are differences, what is the "recommended" syntax?

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

Thanks for pointing this out :)

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

Good idea. At the moment, I'm rewriting the whole process in PlusCal. After
that I'm gonna take a look and try to implement them. :)

From my perspective TLA+ and PlusCal syntax isn't that hard to learn and the
youtube videos, PDF files etc are great to get started. The hard part is to get
the logic right and think about rules and not about implementations.

> All in all an excellent first spec!

Thanks for your feedback.

[Andrew Helwer]

There are no real differences between P and C PlusCal except for the start/end block syntax. I suspect C syntax is more popular because it is more terse, but P syntax is more similar to the initial spirit of PlusCal as executable pseudocode similar to what you would see in papers.