How To Get Your Verified Dafny Program To Interact With External CodeThis blog explores why getting Dafny code to interact with external code is very useful and how to do it
Formal Verification of Ethereum 2.0 Part 1: Fixing the Array-Out-of-Bound Runtime ErrorFormal Verification of Ethereum 2.0 Part 1 explores how to locate, understand, and fix a subtle array-out-of-bound runtime error within the state transition component.
Measuring The Health Of A Stateless Ethereum EcosystemWith a quantified model in place, part three explores various scenarios to measure the health of a Stateless Ethereum ecosystem.
Building A Stateless Ethereum ModelIn part two of the Stateless Ethereum series, we explore our approach to building a model of such a complex ecosystem.
Defining Stateless Ethereum: A Journey Into The UnknownAs the size of Ethereum state grows ad infinitum, it is worth exploring and modeling the question: Is stateless Ethereum feasible?
How We Proved the Eth2 Deposit Contract Is Free of Runtime ErrorsResearchers 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.