-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr [Last updated: Fri Sep 11 18:07:58 CEST 2026] This directory contains a formal model in LNT of the BBA* consensus protocol originally used in the Algorand blockchain. This protocol was originally proposed in: [0] Jing Chen and Silvio Micali. Algorand: A secure and efficient distributed ledger. Theoretical Computer Science 777, pages 155-183 (2019). A formal model of BBA* was first defined in the following technical report: [1] Andrea Esposito, Francesco Pio Rossi, Marco Bernardo, Francesco Fabris, and Hubert Garavel. Formal Modeling and Verification of the Algorand Consensus Protocol in CADP. arXiv:2508.19452v5 [cs.DC], 29 September 2025. Available in ./doc/Esposito-Rossi-Bernardo-et-al-25.pdf. This early model was progressively refined and diverse versions (named U0, U1, U2, U3, and U4) are given in: [2] Hubert Garavel. Guidelines for Producing Concise LNT Models, Illustrated with Formal Models of the Algorand Consensus Protocol. Proceedings of the 7th Workshop on Models for Formal Analysis of Real Systems (MARS 2026), Turin, Italy, April 2026. Available in ./doc/Garavel-26.pdf. Versions U0 ... U4 are given in the annexes of [2]. The corresponding files available in the MARS repository of formal models (https://mars-workshop.org) or from its SVN server (https://sourcesup.renater.fr/scm/viewvc.php/marsrepo). A variant of this formal model of BBA* is presented in: [3] Andrea Esposito, Francesco Pio Rossi, Marco Bernardo, Francesco Fabris, and Francesco Spegni. A Formal Model of Algorand BBA* Consensus with Its Noninterference Analysis and Probabilistic Verification via CADP. Proceedings of the International Conference on Blockchain Research and Applications (BCRA 2026), Palermo, Italy, July 2026. The present demo example is based on version U4, modified by various changes listed hereafter. Files: ALGORAND.lnt main module CHANNELS.lnt description of the various channels CONSTANTS.lnt description of the various constants COUNTER.lnt description of a counter process NODE.lnt description of a node process TYPES.lnt description of the various types demo.svl SVL verification scenario doc/ publications related to the formal model prop/ auxiliary files for the verified properties The verification scenario is described and commented in the file "demo.svl". It can be run by typing $ svl demo or even simply $ svl After the verification you may type $ svl -clean demo or even simply $ svl -clean to remove all the generated files. ------------------------------------------------------------------------------- Note 1: To change the number H of honest nodes in the Algorand network, it is sufficient to modify the "with H=..." clauses in the demo.svl script and to modify the parameter H passed to properties P7a and P7b. Note 2: To change the total number N of nodes in the Algorand network, it is sufficient to modify, in file TYPES.lnt, the definition of type PID (replacing the constant 4 by another number) and to modify, in file ALGORAND.lnt, the number of branches in the parallel operator. ------------------------------------------------------------------------------- History of changes brought after the U4 version presented in [Garavel-26] ------------------------------------------------------------------------- * March 25, 2026: In files prop/ZERO_ONE.lnt and prob/ZERO_ONE_1.lnt, the MAIN process was simplified by calling the P_H function directly, rather than computing P and P_H. * May 04, 2026: In file COUNTER.lnt, replaced == by = for a BIT-type expression. Both notations are equivalent, but the ALGORAND model uses = rather than ==. * May 09, 2026: In file NODE.lnt (process BROADCAST), the events SELF_PROPAGATE and PROPAGATE are now executed in parallel (which is more general) rather than in sequence. Added comments at various places. * May 10, 2026: In file NODE.lnt (process BROADCAST), malicious nodes may now vote several times. In file COUNTER.lnt, the counter process was modified to refuse multiple votes from the same node. * May 11, 2026: In file NODE.lnt (process BROADCAST), if a committee does not reach quorum, its results are now discarded and a new committee is formed. * May 12, 2026: In file CONSTANT.lnt, the quorum value Q is now set to T instead of 0 to enable the enforcement of quorum. In file demo.svl, the properties P7a and P7b, together with their files prop/ZERO_ONE_1.lnt and prop/ZERO_ONE.lnt, are modified since quorum changes the occurrence of flip-coin operations. The properties P9b and P9c are also modified to replace "inevitable" by "fairly inevitable", since quorum creates new internal cycles. * May 16, 2026: In file COUNTER.lnt, the "only if" condition was removed (since it became a consequence of other checks) and replaced by an "assert" statement. * May 24, 2026: In file CONSTANTS.lnt, taking inspiration from [3], the result of function N must now be greater than 1 (instead of greater than 0). * May 25, 2026: Unified identical channels PROPAGATE and SELF_PROPAGATE into PROPAGATE. Renamed channels PROBABILISTIC and SYNCHRONIZE to PROB and SYNC. Renamed constant functions P_H and P_V to PH and PV, respectively. * May 27, 2026: In files TYPES.lnt and NODE.lnt, renamed the constants of type STEP (0 -> 3, 4, or 7, 1 -> 5, 2 -> 6) to match more closely the step numbers of [Chen-Micali-19] and to assign unique numbers to the various probabilistic choices. The properties P9a, P9b, and P9c have been updated accordingly and completed by two new properties P9d and P9e. * May 28, 2026: In file demo.svl, two new properties P6c and P7c (soundness of probabilistic choices) written in XTL have been added. A new property P9f (absence of certain cycles) was also added. * May 29, 2026: In file prop/SELF_PROPAGATE.lnt, slightly simplified the process PART. In file demo.svl, generalized properties P4a and P5a to check all node IDs rather than node 1 only. Consequently, replaced prop/PROPAGATE_1.lnt and prop/SELF_PROPAGATE_1.lnt by two parameterized variants, respectively prop/PROPAGATE_ID.lnt and prop/SELF_PROPAGATE_ID.lnt. * May 31, 2026: Renamed channel and event SET_BIT to SET_B. * June 1, 2026: In file demo.svl, generalized properties P6a and P7a to check all node IDs rather than node 1 only. Consequently, replaced prop/IN_OUT_1.lnt and prop/ZERO_ONE_1.lnt by two parameterized variants, prop/IN_OUT_ID.lnt and prop/ZERO_ONE_ID.lnt. * June 2, 2026: Taking inspiration from [3], four constant functions PF, 1_PF, 1_PH, and 1_PV have been added; function 1_MINUS was removed and process FLIP_COIN received an extra value parameter. * June 3, 2026: In file NODE.lnt, a S:STEP parameter was added to channel PROB and to the events P_IN, P_OUT, P_ZERO, and P_ONE. The properties P6a, P6b, P6c, P7a, P7b, and P7c have been revised in consequence. * June 4, 2026: Following [3], the four events P_IN, P_OUT, P_ZERO, and P_ONE have been replaced by a unique event PROB. The properties P6a, P6b, and P6c have been merged into properties P7a, P7b, and P7c, respectively, and removed. Both files prop/IN_OUT.lnt and prop/ZERO_ONE.lnt have been replaced by a unique file prob/PROB.lnt. Similarly, both files prop/IN_OUT_ID.lnt and prop/ZERO_ONE_ID.lnt have been replaced by a unique file prob/PROB_ID.lnt. * June 9, 2026: In file demo.svl, a new property P3c was added. * June 10, 2026: In file NODE.lnt, renamed process N to BBA, for clarity and to avoid confusion with the constant N that denotes the number of nodes. * June 19, 2026: In file demo.svl, replaced POSSIBLE() by the new MCL macro IMPOSSIBLE(). * June 24, 2026: In file demo.svl, simplified property P3c by using the macro IMPOSSIBLE(). * July 1st, 2026: Added a 2nd parameter S:STEP to channel PROPAGATE and events PROPAGATE and SELF_PROPAGATE; updated the NODE and COUNTER processes accordingly, as well as the properties P4a, P4b, P5a, P5b and their associated files prop/PROPAGATE.lnt, prop/PROPAGATE_ID.lnt, prop/SELF_PROPAGATE.lnt, and prop/SELF_PROPAGATE_ID.lnt. * July 2, 2026: Added a 2nd parameter S:STEP to channel TALLY and event TALLY; updated the NODE and COUNTER processes accordingly, as well as the properties P3a, P3b, and P3c and the associated file prop/TALLY.lnt. * July 7, 2026: Slightly modified property P7b to take into account rounding errors. * July 8, 2026: Modified the file prop/SYNC.lnt of property P2 to ensure that the property holds when T = 1 and Q >= 1 and when T = 2 and Q >= 3. * July 9, 2026: Modified the file prop/TALLY.lnt of property P3b to ensure that the property holds when T = 1 and Q >= 1 and when T = 2 and Q >= 3. * July 10, 2026: Modified properties P4a, P4b, P5a, P5b, and the files prop/PROPAGATE_ID.lnt, prop/PROPAGATE.lnt, prop/SELF_PROPAGATE_ID.lnt, and prop/SELF_PROPAGATE.lnt to ensure that these properties hold for all values of H, T, and Q. * July 11, 2026: In file CONSTANTS.lnt, the value of C is now derived from the value of T, which is a principal parameter for verification configurations; formerly, the value of T was derived from the value of C. * July 12, 2026: Modified properties P7a and P7b, and the associated files prop/PROB_ID.lnt and prop/PROB.lnt to ensure that these properties hold for all values of H, T, and Q. * July 20, 2026: In file demo.svl, added a new property P6 expressing that events PROPAGATE and SELF_PROPAGATE are closely related. * July 21, 2026: In file demo.svl, merged both properties P8a and P8b into a single property P8, since P8a was somehow a particular case of P8b. * July 22, 2026: In file demo.svl, added the $MODELS variable to increase parameterization. * July 23, 2026: In file demo.svl, extended the LTS names (A40.bcg, A22.bcg, etc.) to fully detailed names (H4-N4-Q2-T2.bcg, H2-N4-Q2-T2.bcg, etc.). Added four GET_*() functions to extract parameter values from model names. Added a GENERATE() function to build a model with a given name. * July 24, 2026: In file demo.svl, added three new properties P10a, P10b, and P10c that check whether the decisions of the BBA* algorithm are deterministic or not. * September 6, 2026: In file demo.svl, added function NO_EVENT that checks whether an Algorand instance has certain events. Many properties (P2, P3b, P4a, P4b, P5a, P5b, P7a, and P7b) have been simplified by using NO_EVENT. Also, the files prop/PROB.lnt, prop/PROB_ID.lnt, prop/PROPAGATE.lnt, prop/PROPAGATE_ID.lnt, prop/SELF_PROPAGATE.lnt, prop/SELF_PROPAGATE_ID.lnt, prop/SYNC.lnt, and prop/TALLY.lnt have been simplified accordingly. * September 7, 2026: In file demo.svl, made the results of properties P4a and P5a more precise. * September 8, 2026: In file NODE.lnt, introduced a process PROB to eliminate all probabilistic transitions carrying probabilities 0.0 and 1.0; this significantly reduces the size of H4-N4-Q2-T2.bcg (78,686 -> 1574 states before minimization, 19,923 -> 1218 states after minimization). Updated properties P7c and P8 by adding prop/ACCEPT.lnt and prop/REJECT.lnt. -------------------------------------------------------------------------------