First release of the formal verification of Eth2.0 specs

This release contains the Dafny verified code for a large subset of the Eth2.0 specs' functions.

This project was started by ConsenSys R&D and was also supported by the Ethereum Foundation under grant FY20-285, Q4-2020.

See the README in the master branch for more details.

Experimental branch with GasperFFG proofs.

This branch of the project aims to provide a proof that the computed justified (resp. finalised) check points are indeed justified (resp. finalised).

This branch has diverged from master and is not intended to be merged into master.

This project was started by ConsenSys R&D and was also supported by the Ethereum Foundation under grant FY20-285, Q4-2020.

See the README in this branch for more details.