EF project for model-checking Accountable Safety on the 3SF protocol proposal by D'Amato, Saltini, Tran, and Zanolini.
Spec 1. spec1-2/ffg_recursive.tla. The result of a manual mechanical translation of the original executable specification in Python, which can be found in ffg.py.
Spec 2. spec1-2/ffg.tla. A manual adaptation of Spec 1, using folds instead of recursion and introducing a memorization optimization.
Spec 3. spec3/ffg.tla. A manual abstraction of Spec 2 that is further optimized for constraint solving, especially with Apalache.
Our translation rules from executable Python specifications to TLA+ can be found in Translation.md.
Experimental results are reported in EXPERIMENTS.md.