How We Proved the Eth2 Deposit Contract Is Free of Runtime Errors
Date:
Researchers at ConsenSys designed a machine-checkable correctness (and termination) proof for the Eth2 deposit contract, ensuring that the deposit contract is correct and free of runtime errors.