praveen-supraoracles
released this
13 Jan 05:08
·
187 commits
to master
since this release
This is the formal proof of consistency of the SupraBFT consensus protocol: if any two honest nodes commit blocks to their chains at the same height, then the two blocks are equal. The formal proof is carried out using Ivy version 1.8. The full safety condition is at the last line of the file classic_safety.ivy. The shell script check_all.sh will run all the commands necessary to check everything.
This formally proves the safety of a version of the consensus protocol that was used for the pen and paper safety proof. Some changes have since been made to the protocol for liveness, which are not accounted for in this release.