Keep it coming
tldr;Runtime Verification audit and verification of deposit contract
Runtime Verification recently completed their audit and formal verification of the eth2 deposit contract bytecode. This is a significant milestone bringing us closer to the eth2 Phase 0 mainnet. Now that this work is complete, I ask for review and comment by the community. If there are gaps or errors in the formal specification, please post an issue on the eth2 specs repo.
The formal semantics specified in the K Framework define the precise behaviors the EVM bytecode should exibit and proves that these behaviors hold. These include input validations, updates to the iterative merkle tree, logs, and more. Take a look here for a (semi)high-level discussion of what is specified, and dig in deeper here for the full formal K specification.
I want to thank Daejun Park (Runtime Verification) for leading the effort, and Martin Lundfall and Carl Beekhuizen for much feedback and review along the way.
Again, if this stuff is your cup of tea, now is the time to provide input and feedback on the formal verification – please take a look.The word of the month is “optimization”
The past month has been all about optimizations.
Although a 10x optimization here and a 100x optimization there doesn’t feel so tangible to the Ethereum community today, this phase of development is just as important as any other in getting us to the finish line.Beacon chain optimizations are critical
(why can’t we just max out our machines with the beacon chain)
The beacon chain – the core of eth2 – is a requisite component for the rest of the sharded system. To sync any shard – whether it be a single shard or many, a client must sync the beacon chain. Thus, to be able to run the beacon chain and a handful of shards on a consumer machine, it is paramount that the beacon chain is relatively low in resource consumption even when high validator participa...