EF project for model-checking Accountable Safety on the 3SF protocol proposal by D'Amato, Saltini, Tran, and Zanolini.
Spec 1.: This is the specification spec1-2/ffg_recursive.tla. It is the result of a manual mechanical translation of the original executable specification in Python, which can be found in ffg.py. This specification is using mutually recursive operators, which are not supported by Apalache. As a result, we are not checking this specification.
Spec 2. This is the specification spec1-2/ffg. It is a manual adaptation of Spec 1. The main difference between Spec 2 and Spec 1 is that Spec 2 uses "folds" (also known as "reduce") instead of recursion. Check the model checking instance in spec1-2/MC_ffg.
Spec 3. This is the further abstraction of Spec 2 that uses the concept of a state machine, instead of a purely sequential specification (such as the Python code). Check spec3/ffg and the model checking instance in spec3/MC_ffg.
Spec 3b. This is a specification in SMT using the theory of finite sets and cardinalities. In combination with the solver CVC5, this specification allows us to push verification of accountable safety even further. Check the description.
Spec 3c. This is a specification in Alloy. With this specification, we manage to check all small configurations that cover the base case and one inductive step of the definitions. Check the description.
Spec 4. This is an extension of Spec 3 that contains an inductive invariant in spec4/ffg_inductive.tla. See the model checking instances in MC_ffg_b3_ffg5_v12 and MC_ffg_b3_ffg5_v12.
Spec 4b. This spec contains further abstractions and decomposition of configurations. This is the first TLA+ specification that allowed us to show accountable safety for models of very small size. Check ffg, MC_ffg_b3_ffg5_v12, and MC_ffg_b5_ffg10_v20.
Our translation rules from executable Python specifications to TLA+ can be found in Translation.md.
Experimental results are reported in EXPERIMENTS.md.