The "correct by construction" Casper paper + prototype published at DEVCON. Tear it apart

The network is asynchronous, so the messages from stage 0 might not in time for stage 1 (or validators might not send messages and that’s considered fine).

So, the loop might not converge.

An example commitment criterion is implemented in the prototype.

The validators might do whatever, including machine learning, but when they send a message containing an estimate not backed by the justifications, they are considered Byzantine.