Ethereum Dev Roundup: Q1 (Boring Edition)

The Ethereum Foundation believes in transparency, and they practice what they preach. A recent blog post from Vitalik Buterin, “Ethereum Dev Roundup: Q1 (Boring Edition),” gave an inside look into Ethereum developers’ R&D efforts. (If you’re curious as to why it’s called the “Boring Edition,” Buterin also released a farcical April Fools’ version of the Q1 Dev Roundup.)

Buterin starts off the blog by sharing how the last few weeks “have seen great progress for Ethereum research, and we are excited that the protocol is moving closer and closer to the point where it is ready for mainstream adoption.” Their R&D teams have expanded “substantially” and most of their efforts have been focused on privacy, zero knowledge proofs, formal verification, and consensus algorithms. Buterin’s blog serves as a compendium of their recent R&D and the blogs they’ve written about their current work.  See below:

Vitalik’s Casper Algorithm:

Minimal Slashing Conditions

Safety Under Dynamic Validator Sets

Yoichi Hirai Formally Proving Correctness:

Formal methods on some PoS stuff

A mechanized safety proof for PoS with dynamic validators

Fixing safety proof on dynamic validator PoS

Vlad’s Casper:

Formal methods on another Casper

A Casper Contract (And Test):

Ethereum / research / casper4

Karl Floersch’s Work On The Casper daemon:

Karlfloersch / simplecasper

More From Vlad:

Dealing with failure in cryptocurrency

Simple model of an internal PoW attacker

The case for smaller block rewards

ENS Bugs Led To Audits:

Complete Audit – Martin

Complete Audit - Piper

Updates On Formal Proving:

Ethereum Virtual Machine for Coq (v0.0.2)

EVM formal provers can now run state tests

Metropolis Progress:

Core dev meeting notes

Metropolis implementation in Geth

Metropolis implementation in Parity