-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES)
-- http://cadp.inria.fr

[Last updated: Fri Mar 27 14:58:48 CET 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:

   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:

   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.

which is available in doc/Esposito-Rossi-Bernardo-et-al-25.pdf. Diverse
versions (named U0, U1, U2, U3, and U4) of this formal model are given in:

   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.

which is available in doc/Garavel-26.pdf. This demo is based on version U4
(the other versions U0 ... U3 being available in the MARS repository of
formal models at https://sourcesup.renater.fr/scm/viewvc.php/marsrepo and
https://mars-workshop.org).

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.