Proving Inductive Invariants for TLA+ Models

• Proving Inductive Invariants for TLA+ Models
  • Requirements
  • High-Level Description of Algorithm
    • Reliable Broadcast
    • Byzantine Faults and Message Adversaries
    • Algorithm
  • Formal TLA+ Model
  • Model Checking
    • Bounded Model Checking and Proving Inductive Invariants
    • Validity
    • No Double Delivery
    • No Duplication
    • Scaling Up: Symmetry and Abstraction Techniques

In this post, I show how to write a formal model for a reliable broadcast algorithm using TLA+ and prove its safety properties using the model checker Apalache. In particular, I show how inductive invariants can be constructed and proven, and how to scale model checking further using symmetry and abstraction techniques.

The algorithm considered here is called asynchronous Byzantine Reliable Broadcast with a Message Adversary (MBRB for short), and is based on this paper.

Requirements

• Apalache (I have the version 0.44.2)

All models and scripts mentioned in this post can be found in the subdirectory tla-iind.

High-Level Description of Algorithm

Reliable Broadcast

Reliable broadcast is a fundamental communication primitive in distributed systems. It allows a designated sender process to disseminate a message to all other processes with the following guarantees:

• Validity: If a correct process delivers a message from a correct sender, then the sender actually broadcast that message. (No spurious messages can be fabricated by faulty processes and attributed to a correct sender.)
• No duplication: A correct process delivers at most one message per (sender, sequence number) pair.
• No duplicity / Agreement: No two correct processes deliver different messages with the same sender and sequence number. All correct processes agree on the content of each message they deliver.

In short, reliable broadcast ensures that despite failures, all correct recipients either deliver the same message the sender intended (if the sender is correct) or deliver nothing at all, and they never disagree on what was sent.

Byzantine Faults and Message Adversaries

Byzantine faults model the most severe failure mode in distributed systems: a faulty (Byzantine) process can behave arbitrarily: it may crash, send contradictory information to different processes, forge messages, refuse to forward data, or collude with other faulty processes. The classical assumption is that out of $n$ processes, at most $t$ are Byzantine.

The protocol works under the resilience condition $n > 3t$.

The full protocol is also resilient to a message adversary, which can suppress up to $d$ messages at each broadcast. In this case, the resilience condition is $n> 3t + 2d$. For the purpose of this post, we do not consider message adversary ($d=0$).

Algorithm

The MBRB (Message-adversary Byzantine Reliable Broadcast) protocol uses digital signatures and gossip-based dissemination. Each message is identified by a triple $(m, sn, i)$: the content $m$, a sequence number $sn$, and the sender identity $i$.

Broadcast phase. When a correct sender $p_i$ wants to broadcast message $m$ with sequence number $sn$, it signs the message with its own digital signature, stores this signature locally, and sends the bundle $(message, signature\ set)$ to all processes. Due to the message adversary, at most $d$ processes may not receive this initial bundle.

Receive and relay phase. When a correct process $p$ receives a bundle (consisting of a message $(m, sn, i)$ and a set of signatures $s$) it performs the following checks and actions:

1. Check freshness: If $p$ has already delivered a message from sender $i$ with sequence number $sn$, the bundle is ignored.
2. Check sender’s signature: The original sender $i$ must be present in the signature set $s$ (ensuring the sender endorsed this message).
3. Accumulate and forward: $p$ adds all signatures from the received bundle to its own knowledge, appends its own signature, and then forwards the updated bundle to all other processes. (The message adversary may again drop up to $d$ of these forwarded messages.)
4. Delivery decision: If the number of accumulated signatures for this message exceeds $(n + t) / 2$, then $p$ delivers the message.

Byzantine processes can deviate arbitrarily: they may send bundles with arbitrary (possibly incomplete) signature sets to any process, sign messages on their own, or deliver messages to themselves without following the protocol rules.

The critical insight is that the signature threshold $(n+t)/2$ ensures quorum intersection: if two correct processes each collect enough signatures to deliver, their signature sets must intersect in at least one correct process. Since correct processes only sign a message after verifying the sender’s signature, and correct senders never sign two different messages with the same sequence number, this guarantees the no duplicity property — two correct processes can never deliver conflicting messages for the same $(sender, sn)$ pair.

The formal algorithm from the paper is reproduced below. Here, we distinguish application messages which are pairs $(m, sn, i)$ where $m$ is a message content, $sn$ is a sequence number, and $i$ the ID of the sender process. Below, mbrb_deliver and mbrb_broadcast refer to these messages. Implementation messages correspond to low level packets, aka bundles. Typically, several implementation messages are exchanged before delivering an application message.

Formal TLA+ Model

Let us show how to model this protocol in TLA+ with Apalache type annotations. The model has the following constants.

CONSTANT
    \* @type: Int;
    smax,
    \* @type: Int;
    mmax,
    \* @type: Int;
    n, 
    \* @type: Int;
    t

ASSUME 
    0 <= t /\ 0 <= d /\ n > 3*t

For any analysis with model checking tools for TLA+, we need to bound the sizes of all constants. These are defined above:

• smax is the maximal sequence number,
• mmax is the number of different messages,
• n is the number of processes,
• t is the maximal number of Byzantine processes,
• d is the maximal number of adversary message losses.

The ASSUME statement constrains these to satisfy the resilience condition of the algorithm.

The state variables are defined as below.

\* @type: Set(Int);
ID == 1..n
\* @type: Set(Int);
S == 1..smax
\* @type: Set(Int);
M == 1..mmax

\* @type: Set($message);
\* (m, sn, i) where m : message, sn : seq number, and i : sending process id
Messages == [m : M, sn : S, i : ID]

VARIABLES
    \* @type: Int;
    c,
    \* @typeAlias: message = {
    \*      m: Int,
    \*      sn: Int,
    \*      i: Int
    \* };
    \*
    \* @type: Int -> ($message -> Set( Int ));
    \*  sigs[pi][m] is the set ids of those processes that have signed the message m, as known to pi
    sigs,
    \* @type: Int -> Set( $message );
    mbrb_delivered,
    \* @type: Set(<<Int, $message, Set(Int) >>);  
    \*  {(dest_id, message, sigs)} that have not been delivered yet
    packets,
    \* @type: Set($message);
    mbrb_broadcasts

First,

• ID is the set of process identifiers,
• S is the set of sequence numbers,
• M is the set of messages (abstracted here as integers)
• Messages is the set of all tuples (m, sn, i) that can be sent as a bundle.

Moreover, $message is an application message tuple of the form $(m, sn, i)$. This is to be distinguished from M which contains message contents (referred to as m).

The state variables are also explained in comments:

• sigs maps each process ID pi, and message m to a set of processes that have signed m,
• mbrb_delivered maps each process ID to the set of messages it has delivered,
• packets is the set of individual messages (dest\_id, message, sigs) that have not been delivered yet. Here dest\_id is the destination process, message is a triple of the form (m, sn, i), and sigs is the set of signatures for this message.
• mbrb_broadcasts is the set of messages that have been broadcast since the start of the algorithm.

These variables are enough to capture the state of the network at any moment.

We describe the transitions of the protocol by defining a few useful functions.

The simplest is the broadcast_bundle function:

\* @type: (Int, $message, Set(Int)) => Bool;
broadcast_bundle(p, m, s) ==
    packets' = packets \union {<<q, m, s>> : q \in ID }

Because communication is asynchronous, broadcasting a message simply adds packets to be sent to each process in the set packets.

Delivering a message simply consists in putting this message in the set mbrb_delivered:

\* @type: (Int, $message) => Bool;
mbrb_deliver(p, m) == 
    mbrb_delivered' = [mbrb_delivered EXCEPT ![p] = mbrb_delivered[p] \union {m}]

Now, more interesting is the relation defining a mbrb_broadcast:

\* @type: Bool;
mbrb_broadcast ==
    \E msg \in Messages :      
      LET p == msg.i IN
      \* p has not sent another message with the same sn before:
      /\ \A m2 \in M : p \notin sigs[p][ [m |-> m2, i |-> p, sn |-> msg.sn] ]
      \* p signs its own message and stores it
      /\ sigs' = [sigs EXCEPT ![p][msg] = sigs[p][msg] \union {p} ]
      /\ broadcast_bundle(p, msg, sigs'[p][msg])
      /\ mbrb_broadcasts' = mbrb_broadcasts \cup {msg}
      /\ UNCHANGED( <<c, mbrb_delivered>> )

Here, we select a message with the condition that the sender has not used the sequence number before, sign the message for the sender, and broadcast it. In TLA+, when defining a transition relation, one must be very careful defining the next-state of all state variables. Observe how this is the case here.

Next, consider we consider the receive function, where p is a triple (pi, msg, s) where pi is the receiving process, msg is some message triple (m, sn, i), and s is the set of signatures that are sent with the message. The body of the relation follows more or less the bundle_receive function in the algorithm given above. One exception is that we refactored the rebroadcasting of the message into one line (which we do by updating packets). The function is followed by the receive_packet relation which selects a packet from the set packets and calls the bundle_receive function.

\* @type: (<<Int, $message, Set(Int)>>) => Bool;
bundle_receive(p) ==
    \* the process that receives the bundle
    LET pi == p[1] IN
    \* triple (m, sn, pj)
    LET msg == p[2] IN
    \* signatures carried in the packet (these only contain the signatures of (m,sn,pj))
    LET s == p[3] IN
    \* (_, msg.sn, msg.i) has not been already mbrb-delivered /\ s contains the signature of msg.i for this message
    IF \A m1 \in M : [ m |-> m1, i |-> msg.i, sn |-> msg.sn] \notin mbrb_delivered[pi] /\ msg.i \in s
    THEN
      \* save the signatures for this message, and sign it yourself
      sigs' = [sigs EXCEPT ![pi][msg] = sigs[pi][msg] \union s \union {pi}]
      /\ 
      (IF (pi \notin sigs[pi][msg]) \/ Cardinality(sigs[pi][msg]) * 2 > (n+t) THEN
        packets' = (packets \ {p}) \union {<<q, msg, sigs'[pi][msg]>> : q \in ID \ {pi} }
      ELSE
        packets' = (packets \ {p})
      )
      /\
      (IF Cardinality(sigs[pi][msg])*2 > (n+t) THEN
        mbrb_deliver(pi, msg)
      ELSE
        UNCHANGED(mbrb_delivered)
      )
      /\
      UNCHANGED(<<c, mbrb_broadcasts>>)
    ELSE
      UNCHANGED(vars)

receive_packet == 
    /\ packets /= {}
    /\ \E x \in packets : bundle_receive(x)

We also need to model the behavior of Byzantine processes. Below, the Byzantine process p can send a random packet as long as it sends valid signatures; sign a random packet itself; and deliver a random packet.

byzantine(p) ==
    \* Send a random packet (with available signatures) to a random process
    \* (The Byzantine process could also include a subset of these signatures but we omit this case)
    \/ \E msg \in Messages : \E j \in ID :
            /\ packets' = packets \union {<<j, msg, sigs[p][msg]>> }
            /\ UNCHANGED(<<c, sigs, mbrb_delivered111, b_err_mbrb_delivered121, mbrb_broadcast_occurred>>)
    \* Sign a random packet by self
    \/ \E msg \in Messages : 
            /\ sigs' = [sigs EXCEPT ![p][msg] = sigs[p][msg] \union {p}]
            /\ UNCHANGED(<<c, mbrb_delivered111, b_err_mbrb_delivered121, packets, mbrb_broadcast_occurred>>)
    \* Deliver a random packet
    \/ \E msg \in Messages : 
        /\ mbrb_deliver(p, msg)
        /\ UNCHANGED(<<c, sigs, packets, mbrb_broadcast_occurred>>)

The Init, Next and Spec triple is given below.

Init == 
    /\ c \in ID
    /\ c >= n-t
    /\ sigs = [ id \in ID |-> [m \in Messages |-> {}]]
    /\ mbrb_delivered = [ id \in ID |-> {}]
    /\ packets = {}
    /\ mbrb_broadcasts = {}


Next == 
    \/ mbrb_broadcast
    \/ (\E p \in ID : ~Correct(p) /\ byzantine(p))
    \/ receive_packet

Spec == Init /\ [Next]_vars

The full model is given in MBRB.tla. All other files related to this post can be found here.

Model Checking

We are going to prove several safety properties of this model using inductive invariants.

First, we need to instantiate all constants to finite values. The scenarios we consider are given below.

CInit0 == t = 0 /\ n = 2 /\ mmax = 2 /\ smax = 2
CInit1 == t = 0 /\ n = 3 /\ mmax = 1 /\ smax = 2
CInit2 == t = 0 /\ n = 3 /\ mmax = 2 /\ smax = 2
CInit3 == t = 1 /\ n = 4 /\ mmax = 1 /\ smax = 1
CInit4 == t = 1 /\ n = 4 /\ mmax = 2 /\ smax = 1

The first cases are easy to verify but do not have Byzantine processes (recall that the $n>3t$ condition prevents us from having a Byzantine process with n <= 3). But these cases are still very useful for debugging and building the inductive invariant before proving it for larger instances.

Bounded Model Checking and Proving Inductive Invariants

Bounded model checking (BMC) is a verification technique that searches for counterexamples to a property within executions up to a fixed length bound $k$. Instead of exploring the full state space, BMC unrolls the transition relation $k$ times and checks whether a violating state is reachable within $k$ steps using a SAT or SMT solver. While BMC is highly effective at finding bugs, it cannot prove correctness for unbounded executions.

Inductive invariants overcome this limitation. An invariant $I$ is a state predicate that holds in all reachable states of the system. To prove that $I$ is indeed an invariant, one shows:

1. Initiation: $Init \Rightarrow I$. If $I$ holds in all initial states.
2. Consecution (Inductiveness): $I \land Next \Rightarrow I’$. If $I$ holds in a state and a transition is taken, then $I$ holds in the next state.

The challenge lies in finding an $I$ that is inductive. This means that all successors of states in $I$ (including ones that are not reachable from the initial state) lead to $I$ within one step. Often, the desired safety property itself is not inductive, and one must strengthen it with auxiliary invariants until the conjunction becomes inductive.

Apalache-mc only has a bounded model checking engine. This can be used to check for absence of counterexamples of bounded length but also to prove that a property is an inductive invariant, as follows. Assume that we want to prove the property TypeOK. We verify the two premises as follows.

apalache-mc check --cinit=CInit0 --init=Init --inv=TypeOK --length=0 MBRB.tla
apalache-mc check --cinit=CInit0 --init=TypeOK --inv=TypeOK --length=1 MBRB.tla

The first call does not unroll the transition relation at all (length=0) but simply checks if Init implies TypeOK as per the first premise. The second call checks if starting from TypeOK whether the invariant TypeOK holds in 1 step (length=1). Notice that we need to instantiate the constants which is done with the --cinit argument.

The repository contains the script check_inductive.sh which checks both premises:

./check_inductive.sh MBRB.tla CInit0 TypeOK TypeOK

The property TypeOK is a standard one that appears in most TLA+ models, and simply specifies the type and the range of all variables:

TypeOK == 
    /\ c \in ID
    /\ c >= n-t
    /\ (sigs \in [ ID -> [Messages -> SUBSET(ID)]])
    /\ (mbrb_delivered \in [ID -> SUBSET(Messages)])
    /\ (packets \in SUBSET({<<i, m, ids>> : i \in ID, m \in Messages, ids \in SUBSET(ID)}))
    /\ (mbrb_broadcasts \in SUBSET(Messages))

When working with Apalache, most inductive proofs require TypeOK to be assumed in the initial state. Fortunately, once we prove it separately, we can indeed use it as a lemma. We illustrate the use of lemmas below.

Validity

Here is the validity theorem we want to prove:

\* Theorem (MBRB-Validity (no spurious message)): If a correct process p mbrb-delivers an app-message
\*    m from a correct process m.i with sequence number m.sn, then m.i has mbrb-broadcast m with
\*    sequence number m.sn.
Validity == 
    \A p \in ID : \A m \in mbrb_delivered[p] : 
      Correct(p) /\ Correct(m.i) => m \in mbrb_broadcasts

If you attempt to prove the inductive premise directly:

./check_inductive.sh MBRB.tla CInit0 Validity Validity

Apalache will complain about some primed variable being used before being assigned. This is due to the encoding used by Apalache can be avoided by adding TypeOK which defines each variable explicitly with an equality expression.

Define

InitValidity == TypeOK /\ Validity

Now, we can run

./check_inductive.sh MBRB.tla CInit0 InitValidity Validity

Here, we are replacing the inductive check $I \land Next \Rightarrow I’$ by $I \land J \land Next \Rightarrow I’$ where $J$ is a lemma, that is, a property that has been proven to be invariant. Because $J$ is an overapproximation of the reachable states, the check is still sound.

At this point, we are going to check the protocol for 2 processes only. While this is particularly small, it is sufficient to reveal counterexamples and enough for us to build an inductive invariant. We will prove larger instances once we succeed with CInit0.

The check fails with the following counterexample:

(* Initial state [_transition(0)] *)
State0 ==
  c = 2
    /\ mbrb_broadcasts
      = { [i |-> 1, m |-> 1, sn |-> 2],
        [i |-> 2, m |-> 1, sn |-> 1],
        [i |-> 2, m |-> 2, sn |-> 1],
        [i |-> 2, m |-> 2, sn |-> 2] }
    /\ mbrb_delivered
      = SetAsFun({ <<1, {}>>,
        <<
          2, { [i |-> 1, m |-> 1, sn |-> 2],
            [i |-> 2, m |-> 1, sn |-> 1],
            [i |-> 2, m |-> 2, sn |-> 1],
            [i |-> 2, m |-> 2, sn |-> 2] }
        >> })
    /\ mmax = 2
    /\ n = 2
    /\ packets
      = { <<1, [i |-> 1, m |-> 1, sn |-> 2], {1}>>,
        <<1, [i |-> 2, m |-> 1, sn |-> 2], { 1, 2 }>>,
        <<1, [i |-> 2, m |-> 1, sn |-> 2], {2}>>,
        <<1, [i |-> 2, m |-> 1, sn |-> 2], {}>>,
        <<2, [i |-> 2, m |-> 2, sn |-> 2], {}>> }
    /\ sigs
      = SetAsFun({ <<
          1, SetAsFun({ <<[i |-> 1, m |-> 1, sn |-> 1], {}>>,
            <<[i |-> 1, m |-> 1, sn |-> 2], {}>>,
            <<[i |-> 1, m |-> 2, sn |-> 1], {2}>>,
            <<[i |-> 1, m |-> 2, sn |-> 2], {}>>,
            <<[i |-> 2, m |-> 1, sn |-> 1], {}>>,
            <<[i |-> 2, m |-> 1, sn |-> 2], { 1, 2 }>>,
            <<[i |-> 2, m |-> 2, sn |-> 1], {}>>,
            <<[i |-> 2, m |-> 2, sn |-> 2], {}>> })
        >>,
        <<
          2, SetAsFun({ <<[i |-> 1, m |-> 1, sn |-> 1], {1}>>,
            <<[i |-> 1, m |-> 1, sn |-> 2], { 1, 2 }>>,
            <<[i |-> 1, m |-> 2, sn |-> 1], {1}>>,
            <<[i |-> 1, m |-> 2, sn |-> 2], {1}>>,
            <<[i |-> 2, m |-> 1, sn |-> 1], {1}>>,
            <<[i |-> 2, m |-> 1, sn |-> 2], {1}>>,
            <<[i |-> 2, m |-> 2, sn |-> 1], {1}>>,
            <<[i |-> 2, m |-> 2, sn |-> 2], {1}>> })
        >> })
    /\ smax = 2
    /\ t = 0

(* State1 [_transition(6)] *)
State1 ==
  c = 2
    /\ mbrb_broadcasts
      = { [i |-> 1, m |-> 1, sn |-> 2],
        [i |-> 2, m |-> 1, sn |-> 1],
        [i |-> 2, m |-> 2, sn |-> 1],
        [i |-> 2, m |-> 2, sn |-> 2] }
    /\ mbrb_delivered
      = SetAsFun({ <<1, {[i |-> 2, m |-> 1, sn |-> 2]}>>,
        <<
          2, { [i |-> 1, m |-> 1, sn |-> 2],
            [i |-> 2, m |-> 1, sn |-> 1],
            [i |-> 2, m |-> 2, sn |-> 1],
            [i |-> 2, m |-> 2, sn |-> 2] }
        >> })
    /\ mmax = 2
    /\ n = 2
    /\ packets
      = { <<1, [i |-> 1, m |-> 1, sn |-> 2], {1}>>,
        <<1, [i |-> 2, m |-> 1, sn |-> 2], {2}>>,
        <<1, [i |-> 2, m |-> 1, sn |-> 2], {}>>,
        <<2, [i |-> 2, m |-> 1, sn |-> 2], { 1, 2 }>>,
        <<2, [i |-> 2, m |-> 2, sn |-> 2], {}>> }
    /\ sigs
      = SetAsFun({ <<
          1, SetAsFun({ <<[i |-> 1, m |-> 1, sn |-> 1], {}>>,
            <<[i |-> 1, m |-> 1, sn |-> 2], {}>>,
            <<[i |-> 1, m |-> 2, sn |-> 1], {2}>>,
            <<[i |-> 1, m |-> 2, sn |-> 2], {}>>,
            <<[i |-> 2, m |-> 1, sn |-> 1], {}>>,
            <<[i |-> 2, m |-> 1, sn |-> 2], { 1, 2 }>>,
            <<[i |-> 2, m |-> 2, sn |-> 1], {}>>,
            <<[i |-> 2, m |-> 2, sn |-> 2], {}>> })
        >>,
        <<
          2, SetAsFun({ <<[i |-> 1, m |-> 1, sn |-> 1], {1}>>,
            <<[i |-> 1, m |-> 1, sn |-> 2], { 1, 2 }>>,
            <<[i |-> 1, m |-> 2, sn |-> 1], {1}>>,
            <<[i |-> 1, m |-> 2, sn |-> 2], {1}>>,
            <<[i |-> 2, m |-> 1, sn |-> 1], {1}>>,
            <<[i |-> 2, m |-> 1, sn |-> 2], {1}>>,
            <<[i |-> 2, m |-> 2, sn |-> 1], {1}>>,
            <<[i |-> 2, m |-> 2, sn |-> 2], {1}>> })
        >> })
    /\ smax = 2
    /\ t = 0

While this is quite hard to read, State0 and State1 are the full descriptions of two states such that State0 satisfies InitValidity but State1 violates Validity. This is a counterexample to induction (CTI).

You can use a diff tool to visualize what happens between the two states. Basically, the following tuple belongs to the set packets in State0:

<<2, [i |-> 2, m |-> 1, sn |-> 2], { 1, 2 }>>,

and gets mbrb_delivered in State1, while it does not belong to mbrb_broadcasts.

Thus, satisfying validity in one step does not necessarily imply being valid in the next step.

Intuitively, the State0 should not be reachable. In fact, the above message has been signed by the sender 2 but it does not appear in the list of broadcasts. This cannot be. Let us write this property as a lemma:

\* Lemma: If a message m originating from a correct process has been signed, then m has been mbrb-broadcast.
MsgOriginateFromBR ==
  \A m \in Messages : Correct(m.i) /\ m.i \in sigs[m.i][m] => m \in mbrb_broadcasts
InitMsgOriginateFromBR == TypeOK /\ MsgOriginateFromBR  

We can attempt to prove this lemma:

./check_inductive.sh MBRB.tla CInit0 InitMsgOriginateFromBR MsgOriginateFromBR

But this fails with the following CTI.

• State0:
  • We have packets = {<<2, [i |-> 2, m |-> 2, sn |-> 2], { 1, 2 }>>}
  • this message does not appear in mbrb_broadcasts
  • there is no signature for this packet by process 2

But this packet is received by process 2 in the next step which adds the signature it sees in sigs. Because mbrb_broadcasts still does not contain this message, the invariant fails.

But this should again not be possible in our protocol. We need another lemma excluding the above situation. Basically, if a signature of a message m appears somewhere, then the signing process already has the signature.

\* Lemma: 
\*  1. If q has the signature of m by p, then so does p.
\*  2. all processes p whose signatures for m appear in s in a packet have indeed signed m.
\* Proof: Inductive invariant assuming TypeOK
PacketsValid == 
    \A dest \in ID : \A m \in Messages : \A s \in SUBSET(ID) : 
    \A p \in ID : Correct(p) =>
        \* If p knows the signature of q for message m, then p also knows its own signature for m
        /\ \A q \in ID : p \in sigs[q][m] => p \in sigs[p][m]
        \* all processes p whose signature appear in s have signed this message        
        /\ <<dest, m, s>> \in packets /\ p \in s => p \in sigs[p][m]
InitPacketsValid == TypeOK /\ PacketsValid

In practice, bulding the previous lemma requires a few more counterexample analysis steps.

We can now prove this lemma alone:

./check_inductive.sh MBRB.tla CInit0 InitPacketsValid PacketsValid

Then prove the lemma MsgoriginateFromBR by strengthening it with the PacketsValid lemma:

InitMsgOriginateFromBR == TypeOK /\ PacketsValid /\ MsgOriginateFromBR  

./check_inductive.sh MBRB.tla CInit0 InitMsgOriginateFromBR MsgOriginateFromBR

At last, we can prove that Validity is inductive relative to previous lemmas (relative to means that we are strengthening the first step by known lemmas):

InitValidity == TypeOK /\ PacketsValid /\ MsgOriginateFromBR /\ Validity

./check_inductive.sh MBRB.tla CInit0 InitValidity Validity

We have established validity for CInit0. Can we go further? We succeeded proving up to CInit2 in 11m. To go further, we suggest here using abstraction techniques which will be detailed below.

Let us first mention the no-double-delivery property:

No Double Delivery

No-double-delivery can be expressed as follows.

\* Theorem: MBRB-No-double-delivery. A correct process pi mbrb-delivers at most one app-message m
\*    from a process pj with sequence number sn.
Nodouble_deliver == 
  \A pi \in ID : \A msg \in Messages : \A s \in SUBSET(ID) :
    \* The If-condition of bundle_receive
    ( /\ \A m1 \in M : [ m |-> m1, i |-> msg.i, sn |-> msg.sn] \notin mbrb_delivered[pi] 
      /\ msg.i \in s
      \* The inner if-condition for mbrb_deliver
      /\ Cardinality(sigs[pi][msg])*2 > (n+t))
    => msg \notin mbrb_delivered[pi]
InitNodouble_deliver == TypeOK /\ PacketsValid /\ Nodouble_deliver

Here, rather than introducing an auxiliary variable to track double delivery, we express that if the if-conditions of bundle_receive leading to mbrb_delivery pass, then the message to be delivered is not already in the set mbrb_delivered[pi] for process pi.

This can be proven thanks to the lemma PacketsValid already proven above, with the initial condition:

InitNodouble_deliver == TypeOK /\ PacketsValid /\ Nodouble_deliver

You can run

./check_inductive.sh MBRB.tla CInit0 InitNodouble_deliver Nodouble_deliver

This succeeded on my machine for CInit2 in 5 minutes, for CInit3 in 6 minutes, and CInit4 in 28 minutes.

No Duplication

The third property we prove states that no two different correct processes mbrb-deliver different app-messages from a process pi with the same sequence number sn.

\* Theorem: MBRB-No-duplicity.
Noduplicity == \A p \in ID : \A q \in ID : \A msg \in Messages : \A other_m \in M :
  msg \in mbrb_delivered[p] /\ [ m |-> other_m, i |-> msg.i, sn |-> msg.sn] \in mbrb_delivered[q]
  => msg.m = other_m

It is easy to check that this property is not inductive, even with respect to PacketsValid. We will prove this property in the next section using abstraction techniques.

Scaling Up: Symmetry and Abstraction Techniques

We still would like to verify validity for at least the condition CInit3 ($n=4, t=1$) i.e. with the presence of a Byzantine process, and the no-duplication property for CInit4 (with the presence of a Byzantine process and two different messages).

We will achieve this thanks to symmetry reduction and abstraction techniques detailed below.

As a rule of thumb, reducing the number of variables, or their domains often lead to performance gains. To check validity, we suggest a simple abstraction which consists in tracking only the broadcast and delivery of packet $(1,1,1)$. Because message contents, process IDs, and sequence numbers are symmetric (their precise values do not matter), it is sufficient to prove validity for this specific message.

The changes in the model are the following. We remove the variable mbrb_broadcasts and replace it with the Boolean variable

  \* @type: Bool;
  mbrb_broadcast_occurred

storing whether $(1,1,1)$ has been broadcast.

Accordingly, the mbrb_broadcast relation now contains the conjunct

  /\ (mbrb_broadcast_occurred' = (mbrb_broadcast_occurred \/ (msg.i = 1 /\ msg.sn = 1 /\ msg.m = 1)))

Other changes are straightforward. The validity theorem becomes:

Validity == 
    \A p \in ID : \A m \in mbrb_delivered[p] : 
      Correct(p) /\ Correct(m.i) /\ m.i = 1 /\ m.sn = 1 /\ m.m = 1 => mbrb_broadcast_occurred

The whole modified model can be found in MBRB_sym.tla.

I could prove the validity for CInit3 in 14 minutes:

./check_validity.sh MBRB_sym.tla CInit3

To prove the no-duplication property, we can go even further and define a more aggressive abstraction. In this abstraction, we will check whether it is possible to mbrb_deliver $(1,1,1)$ first, and then mbrb_deliver $(1,2,1)$. As above, the sender process ID and the sequence number are irrelevant. What matters is that we are checking whether two messages ($1$ and $2$) can be delivered with the same sender process ID and the same sequence number.

The variables now contain the following:

    \* @type: Set(Int);
    \* The set of processes that have delivered the message <<1, 1, 1>>
    mbrb_delivered111,
    \* Observer: Whether some process has mbrb-delivered <<1,2,1>> while <<1,1,1>> was already mbrb-delivered?
    \* @type: Bool;
    b_err_mbrb_delivered121,

Here, mbrb_delivered111 replaces the map mbrb_delivered and now only tracks this particular message. The Boolean flag b_err_mbrb_delivered121 tracks whether $(1,2,1)$ was delivered after $(1,1,1)$ has been delivered.

Accordingly, the mbrb_deliver function is changed as follows.

\* @type: (Int, $message) => Bool;
mbrb_deliver(p, m) == 
    /\ mbrb_delivered111' = 
        IF m.i = 1 /\ m.m = 1 /\ m.sn = 1 THEN 
            mbrb_delivered111 \cup {p} 
        ELSE 
            mbrb_delivered111
    /\ b_err_mbrb_delivered121' = 
        \/ b_err_mbrb_delivered121 
        \/ /\ Correct(p) 
           /\ m.i = 1 /\ m.m = 2 /\ m.sn = 1
           /\ mbrb_delivered111 \cap 1..c /= {}

The no-duplicity theorem is now very simple to state:

Noduplicity == ~b_err_mbrb_delivered121

This abstract model can be found in MBRB_abs_12.tla.

The proof requires once again several intermediate lemmas which we comment now.

First, we need PacketsValid lemma which was central in all properties we have proven. The version below is just the instantiation for the messages of the form $(1,\cdot,1)$ since we only deal with these.

\* Lemma: this is a restriction of the PacketsValid lemma to messages of the form <<1, _, 1>>.
\* (This version is sufficient to prove no-duplicity and lower execution time)
PacketsValid11 == 
    \A dest \in ID : \A s \in SUBSET(ID) : \A mcontent \in M : 
    LET m == [ i|-> 1, m |-> mcontent, sn |-> 1] IN
    \A p \in ID : Correct(p) =>
        \* If p knows the signature of q for message m, then p also knows its own signature for m
        /\ \A q \in ID : p \in sigs[q][m] => 
            /\ p \in sigs[p][m]
            /\ Correct(m.i) => m.i \in sigs[m.i][m]
        \* all processes p whose signature appear in s have signed this message        
        /\ <<dest, m, s>> \in packets /\ p \in s => p \in sigs[p][m]
InitPacketsValid11 == TypeOK /\ PacketsValid11

The following lemma states that a correct process does not sign two different messages with the same sender and sequence numbers.

\* Lemma: A correct process does not emit two packets with the same sn and different message contents
\* symmetry reduction: we only prove this for m.i = 1, and m.m = 1, while 2 represents a different message content
NoduplicitySig ==
    \A sn \in S : 
        LET m  == [i |-> 1, m |-> 1, sn |-> sn] IN
        LET m2 == [i |-> 1, m |-> 2, sn |-> sn] IN
        Correct(m.i) /\ m.i \in sigs[m.i][m] =>
        m.i \notin sigs[m.i][m2]
InitNoduplicitySig == TypeOK /\ PacketsValid11 /\ NoduplicitySig

It can be proven thanks to the lemma PacketsValid11.

The following lemma is a simple property stating that any process delivering the message $(1,1,1)$ must have signed it before.

\* Lemma: If some process p has mbrb_delivered111, then it owns the signature of <<1,1,1>>
Delivered111MeansSigned ==
    \A p \in ID : 
        Correct(p) /\ p \in mbrb_delivered111 =>
        p \in sigs[p][[i |-> 1, m |-> 1, sn |-> 1]]
InitDelivered111MeansSigned == TypeOK /\ PacketsValid11 /\ Delivered111MeansSigned

At last, these lemmas allow us to prove the no-duplicity theorem.

\* Theorem: MBRB-No-duplicity. No two different correct processes mbrb-deliver different app-messages
\* from a process pi with the same sequence number sn.
Noduplicity == ~b_err_mbrb_delivered121
InitNoduplicity == TypeOK /\ PacketsValid11 /\ NoduplicitySig /\ Delivered111MeansSigned /\ Noduplicity

All these steps are automatized in the ./check_nodup.sh script which checks the model MBRB_abs_12.tla with the instantiation CInit4. This succeeded in 25 minutes.

Furthermore, this abstraction also allowed us to prove validity for CInit4 in 44 minutes.

./check_validity.sh MBRB_abs_12.tla CInit4