review request: TLA+ model of Katzenpost/tor dirauth protocol

[David Stainton]

Greetings TLA+ enthusiasts. I'm writing to request feedback or suggestions.

I've been practicing my TLA+ for the past week and here's my first

model of a real protocol, the Tor/Katzenpost dirauth protocol, it's a simple non-BFT voting protocol which is used by the directory authority nodes of an anonymous communication networks, to create a consensus document containing a view of the network that clients can use.

https://github.com/katzenpost/formal_specifications/blob/main/dirauth/dirauth.tla

Thus far I'm able to write this theorem:

THEOREM ConsensusFailureWithBadActor ==
    /\ \E n \in Nat:
        /\ Cardinality(dirauth_nodes) = n
        /\ Cardinality(bad_actors) = n-3
    => <>[] (phase = "Failed Consensus")

Next I'm thinking that I should make it model dirauth node outages (when a node doesn't respond) or perhaps flaky unreliable dirauth node behavior.

If I did that then I'd be able to write theorem about how node failures can cause "Failed Consensus" state.

Cheers,

David Stainton